# Differences

This shows you the differences between two versions of the page.

 sav08:complete_recursive_axiomatizations [2008/04/06 16:59]vkuncak sav08:complete_recursive_axiomatizations [2009/05/16 10:47] (current)vkuncak Both sides previous revision Previous revision 2009/05/16 10:47 vkuncak 2008/04/06 16:59 vkuncak 2008/04/06 16:58 vkuncak 2008/04/06 16:52 vkuncak 2008/04/06 16:52 vkuncak 2008/04/06 16:51 vkuncak 2008/04/06 16:50 vkuncak 2008/04/06 16:49 vkuncak 2008/04/06 16:49 vkuncak 2008/04/06 16:48 vkuncak 2008/04/06 16:48 vkuncak 2008/04/06 16:43 vkuncak 2008/04/06 16:27 vkuncak 2008/04/06 16:27 vkuncak 2008/04/06 16:26 vkuncak 2008/04/06 16:25 vkuncak 2008/04/03 16:05 vkuncak 2008/04/03 14:07 vkuncak 2008/04/03 13:52 vkuncak created 2009/05/16 10:47 vkuncak 2008/04/06 16:59 vkuncak 2008/04/06 16:58 vkuncak 2008/04/06 16:52 vkuncak 2008/04/06 16:52 vkuncak 2008/04/06 16:51 vkuncak 2008/04/06 16:50 vkuncak 2008/04/06 16:49 vkuncak 2008/04/06 16:49 vkuncak 2008/04/06 16:48 vkuncak 2008/04/06 16:48 vkuncak 2008/04/06 16:43 vkuncak 2008/04/06 16:27 vkuncak 2008/04/06 16:27 vkuncak 2008/04/06 16:26 vkuncak 2008/04/06 16:25 vkuncak 2008/04/03 16:05 vkuncak 2008/04/03 14:07 vkuncak 2008/04/03 13:52 vkuncak created Line 8: Line 8: **Proof.**++++| **Proof.**++++| Suppose $Ax$ is a complete recursive axiomatization. ​ There are two cases, depending on whether $Ax$ is consistent. Suppose $Ax$ is a complete recursive axiomatization. ​ There are two cases, depending on whether $Ax$ is consistent. - * **Case 1):** The set $Ax$ is inconsistent,​ that is, there are not models for $Ax$.  Then $Conseq(Ax)$ is the set of all first-order sentences and there is a trivial algorithm for checking whether $F \in Conseq(Ax)$:​ always return true. + * **Case 1):** The set $Ax$ is inconsistent,​ that is, there are no models for $Ax$.  Then $Conseq(Ax)$ is the set of all first-order sentences and there is a trivial algorithm for checking whether $F \in Conseq(Ax)$:​ always return true. * **Case 2):** The set $Ax$ is consistent. ​ Given $F$, to check whether $F \in Conseq(Ax)$ we run in parallel two complete theorem provers (which exist by [[lecture10|Herbrand theorem]]), the first one trying to prove the formula $F$, the second one trying to prove the formula $\lnot F$; the procedure terminates if any of these theorem provers succeed (the theorem provers simultaneously searches for longer and longer proofs from a larger and larger finite subsets of $Ax$). We show that this is an algorithm that decides $F \in Conseq(Ax)$. * **Case 2):** The set $Ax$ is consistent. ​ Given $F$, to check whether $F \in Conseq(Ax)$ we run in parallel two complete theorem provers (which exist by [[lecture10|Herbrand theorem]]), the first one trying to prove the formula $F$, the second one trying to prove the formula $\lnot F$; the procedure terminates if any of these theorem provers succeed (the theorem provers simultaneously searches for longer and longer proofs from a larger and larger finite subsets of $Ax$). We show that this is an algorithm that decides $F \in Conseq(Ax)$. * Because either $F \in Conseq(Ax)$ or $(\lnot F) \in Conseq(Ax)$,​ and theorem provers are complete, one of these theorem provers will eventually halt.  The procedure is therefore an algorithm. * Because either $F \in Conseq(Ax)$ or $(\lnot F) \in Conseq(Ax)$,​ and theorem provers are complete, one of these theorem provers will eventually halt.  The procedure is therefore an algorithm.