Craig's Theorem - Recursive Axiomatization

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.