LARA

This is an old revision of the document!

Complete Recursive Axiomatizations

Theorem: Let a set of formulas $Ax$ be a recursive axiomatization for a complete theory, that is:

  • there exists a an algorithm for checking, given $F$, whether $F \in Ax$,
  • 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 recursive axiomatization, then this theory is decidable.

(Note: a finite axiomatization is recursive. Typical axiomatizations that use “axiom schemas” are also recursive.)

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

  • 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