LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Last revision Both sides next revision
sav08:complete_recursive_axiomatizations [2008/04/06 16:49]
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 7: Line 6:
 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 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)$. 
 +    * 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 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.)+**End of Proof.** 
 +++++ 
 + 
 +In shortif 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 casesdepending 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 $Ibe 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 (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)$. +  * there is no enumerable set of axioms ​$Ax$ such that $Conseq(Ax\F \mid e_F(I) \}$.
-  * Because either $\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