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
sav08:complete_recursive_axiomatizations [2008/04/06 16:49]
vkuncak
sav08:complete_recursive_axiomatizations [2009/05/16 10:47]
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 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 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