LARA

This is an old revision of the document!

Complete Recursive Axiomatizations

Theorem: Let a set of first-order sentences $Ax$ be a recursively enumerable axiomatization for a 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$;
  • $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)$.

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.

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 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)$.

End of Proof.

Example: the theory of integers with multiplication and quantifiers is undecidable

  • consequently, there are no complete axiomatizations for it, no decidable set of axioms from which the truth value of facts about natural numbers follows
  • this result is one part of Goedel's incompleteness theorem

References