Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:complete_recursive_axiomatizations [2008/04/06 16:48] vkuncak |
sav08:complete_recursive_axiomatizations [2008/04/06 16:50] vkuncak |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| ---- | ---- | ||
| - | **Theorem:** Let a set of formulas $Ax$ be a recursively enumerable axiomatization for a [[First-Order Theories|complete and consistent theory]], that is: | + | **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: |
| * $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 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$; | ||
| * $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.**++++| |
| - | + | ||
| - | In other words, if a complete theory has a recursively enumerable axiomatization, then this theory is decidable. | + | |
| - | + | ||
| - | (Note: a finite axiomatization is recursively enumerable. Typical axiomatizations that use "axiom schemas" are also recursively enumerable.) | + | |
| - | + | ||
| - | 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.** | + | |
| 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. | ||
| Line 26: | Line 18: | ||
| **End of Proof.** | **End of Proof.** | ||
| + | ++++ | ||
| + | |||
| + | In other words, if a complete theory has a recursively enumerable axiomatization, then this theory is decidable. | ||
| + | |||
| + | (Note: a finite axiomatization is recursively enumerable. Typical axiomatizations that use "axiom schemas" are also recursively enumerable.) | ||
| + | |||
| + | 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. | ||
| + | |||
| Example: the theory of integers with multiplication and quantifiers is undecidable | Example: the theory of integers with multiplication and quantifiers is undecidable | ||