Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:complete_recursive_axiomatizations [2008/04/06 16:52] vkuncak |
sav08:complete_recursive_axiomatizations [2008/04/06 16:52] vkuncak |
||
|---|---|---|---|
| Line 9: | Line 9: | ||
| **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 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 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. | ||
| * If $F$ is proved, then by soundness of theorem prover, $F \in Conseq(Ax)$. | * If $F$ is proved, then by soundness of theorem prover, $F \in Conseq(Ax)$. | ||