LARA

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

Proof.

In short: if a 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.

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

  • 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