This is an old revision of the document!
Complete Recursive Axiomatizations
Theorem: Let a set of first-order sentences 
be a recursively enumerable axiomatization for a complete and consistent theory, that is:
- is recursively enumerable: there exists an enumerateion
of the set and there exists an algorithm that given 
computes 
; 
is complete: for each FOL sentence 
, either 
or 
;
Then there exists an algorithm for checking, given , whether .
Proof.
; 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 
is proved, then by soundness of theorem prover 
for 
.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.
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