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 be an enumeration of the axioms of a recursively enumerable set T of first-order formulas. Construct another set T
* consisting of
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 or of the form
Since each formula has finite length, it is checkable whether or not it is or of the said form. If it is of the said form and consists of ''j'' conjuncts, it is in T
* if it is the expression ; otherwise it is not in T
*. Again, it is checkable whether it is in fact by going through the enumeration of the axioms of T and then checking symbol-for-symbol whether the expressions are identical.
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』