Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:complete_recursive_axiomatizations [2008/04/06 16:43] vkuncak |
sav08:complete_recursive_axiomatizations [2009/05/16 10:47] (current) vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Complete Recursive Axiomatizations ====== | ====== Complete Recursive Axiomatizations ====== | ||
- | ---- | + | **Theorem:** Let a set of first-order sentences $Ax$ be a recursively enumerable axiomatization for a [[First-Order Theories|complete and consistent theory]], that is: |
- | **Theorem:** Let a set of formulas $Ax$ be a recursive axiomatization for a [[First-Order Theories|complete and consistent theory]], that is: | + | * $Ax$ is recursively enumerable: there exists an enumerateion $A_1,A_2,\ldots$ of the set $Ax$ and there exists an algorithm that given $i$ computes $A_i$; |
- | * $Ax$ is recursive: there exists a an algorithm for checking, given $F$, whether $F \in Ax$ | + | * $Conseq(Ax)$ is complete: for each FOL sentence $F$, either $F \in Conseq(Ax)$ or $(\lnot F) \in Conseq(Ax)$; |
- | * $Conseq(Ax)$ is complete: for each FOL sentence $F$, either $F \in Conseq(Ax)$ or $(\lnot F) \in Conseq(Ax)$ | + | |
Then there exists an algorithm for checking, given $F$, whether $F \in Conseq(Ax)$. | Then there exists an algorithm for checking, given $F$, whether $F \in Conseq(Ax)$. | ||
- | ---- | + | **Proof.**++++| |
+ | 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 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)$. | ||
+ | * 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 $(\lnot F)$ is proved, then by soundness of theorem prover $(\lnot F) \in Conseq(Ax)$. Because $Ax$ is consistent, there is a model $I$ for $Ax$. Then $(\lnot F)$ is true in $I$, so $F$ is false in $I$. Because there is a model where $F$ does not hold, we have $F \notin Conseq(Ax)$. | ||
- | In other words, if a complete theory has a recursive axiomatization, then this theory is decidable. | ||
- | (Note: a finite axiomatization is recursive. Typical axiomatizations that use "axiom schemas" are also recursive.) | + | **End of Proof.** |
+ | ++++ | ||
+ | |||
+ | In short: if a complete theory has a recursively enumerable axiomatization, then this theory is decidable. | ||
Conversely: if a theory is undecidable (there is no algorithm for deciding whether a sentence is true or false), then the theory does not have a recursive axiomatization. | Conversely: if a theory is undecidable (there is no algorithm for deciding whether a sentence is true or false), then the theory does not have a recursive axiomatization. | ||
- | **Proof.** | + | Note: |
- | Suppose $Ax$ is a complete recursive axiomatization. There are two cases, depending on whether $Ax$ is consistent. | + | * a finite axiomatization is recursively enumerable |
+ | * typical axiomatizations that use "axiom schemas" are also recursively enumerable | ||
+ | * if $Ax$ is an axiomatization for for some interpretation $I$, that is $Conseq(Ax) = \{ F \mid e_F(F)(I) \}$, then $Ax$ is an axiomatization of a complete theory | ||
- | **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. | + | **Corrollary:** Let $I$ be an interpretation. Then exactly one of the following is true: |
- | + | * there exists an algorithm for checking $e_F(F)(I)$ | |
- | **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. We show that this is an algorithm that decides $F \in Conseq(Ax)$. | + | * there is no enumerable set of axioms $Ax$ such that $Conseq(Ax) = \{ F \mid e_F(I) \}$. |
- | * 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 $(\lnot F)$ is proved, then by soundness of theorem prover $(\lnot F) \in Conseq(Ax)$. Because $Ax$ is consistent, there is a model $I$ for $Ax$. Then $(\lnot F)$ is true in $I$, so $F$ is false in $I$. Because there is a model where $F$ does not hold, we have $F \notin Conseq(Ax)$. | + | |
- | + | ||
- | **End of Proof.** | + | |
Example: the theory of integers with multiplication and quantifiers is undecidable | Example: the theory of integers with multiplication and quantifiers is undecidable |