Craig's theorem

From Wikipedia, the free encyclopedia

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. Distinguish this result from the more well-known Craig interpolation theorem.

Proof. Let 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

\underbrace{A_i\land\dots\land A_i}_i

for each positive integer i. Clearly the deductive closures of T* and T are equivalent. A decision procedure for T* lends itself according to the following informal reasoning. Each member of T* is either A1 or of the form

\underbrace{B_j\land\dots\land B_j}_j.

Since each formula has finite length, it is checkable whether or not it is A1 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 Aj; otherwise it is not in T*. Again, it is checkable whether it is in fact An by going through the enumeration of the axioms of T and then checking symbol-for-symbol whether the expressions are identical.

[edit] References

  • William Craig. On Axiomatizability Within a System, The Journal of Symbolic Logic, Vol. 18, No. 1 (1953), pp. 30-32.