# Craig's theorem

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.

## Recursive axiomatization

Let ${\displaystyle A_{1},A_{2},\dots }$ be an enumeration of the axioms of a recursively enumerable set T of first-order formulas. Construct another set T* consisting of

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{i}}$

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 ${\displaystyle A_{1}}$ or of the form

${\displaystyle \underbrace {B_{j}\land \dots \land B_{j}} _{j}.}$

Since each formula has finite length, it is checkable whether or not it is ${\displaystyle A_{1}}$ or of the said form. If it is of the said form and consists of j conjuncts, it is in T* if the (reoccurring) conjunct is ${\displaystyle A_{j}}$; otherwise it is not in T*. Again, it is checkable whether the conjunct is in fact ${\displaystyle A_{n}}$ by going through the enumeration of the axioms of T and then checking symbol-for-symbol whether the expressions are identical.

## 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 ${\displaystyle A_{i}}$ with

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{i}}$

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{f(i)}}$ (*)
where f(x) is a function that, given i, returns a computation history showing that ${\displaystyle A_{i}}$ is in the original recursively enumerable set of axioms. It is possible for a primitive recursive function to parse an expression of form (*) to obtain ${\displaystyle A_{i}}$ and j. Then, because Kleene's T predicate is primitive recursive, it is possible for a primitive recursive function to verify that j is indeed a computation history as required.