Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
sav08:complete_recursive_axiomatizations [2008/04/06 16:52] vkuncak |
sav08:complete_recursive_axiomatizations [2008/04/06 16:59] 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 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$; | ||
Line 19: | Line 18: | ||
++++ | ++++ | ||
- | In other words, if a complete theory has a recursively enumerable axiomatization, then this theory is decidable. | + | In short: 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. | 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. | ||
+ | Note: | ||
+ | * 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 | ||
+ | |||
+ | **Corrollary:** Let $I$ be an interpretation. Then exactly one of the following is true: | ||
+ | * there exists an algorithm for checking $e_F(F)(I)$ | ||
+ | * there is no enumerable set of axioms $Ax$ such that $Conseq(Ax) = \{ F \mid e_F(I) \}$. | ||
Example: the theory of integers with multiplication and quantifiers is undecidable | Example: the theory of integers with multiplication and quantifiers is undecidable |