In mathematical logic, Craig's theorem states that any recursively enumerable set of well-formed formulas of a first-order language is (primitively) recursively axiomatizable. This result is not related to the well-known Craig interpolation theorem, although both results are named after the same mathematician, William Craig.
Contents
Recursive axiomatization
Let
for each positive integer i. The deductive closures of T* and T are thus equivalent; the proof will show that T* is a decidable set. A decision procedure for T* lends itself according to the following informal reasoning. Each member of T* is either
Since each formula has finite length, it is checkable whether or not it is
Primitive recursive axiomatizations
The proof above shows that for each recursively enumerable set of axioms there is a recursive set of axioms with the same deductive closure. A set of axioms is primitive recursive if there is a primitive recursive function that decides membership in the set. To obtain a primitive recursive aximatization, instead of replacing a formula
one instead replaces it with
where f(x) is a function that, given i, returns a computation history showing that