
In mathematical logic, Craig's theorem states that any recursively enumerable set of wellformed formulas of a firstorder language is (primitively) recursively axiomatizable. This result is not related to the wellknown Craig interpolation theorem, although both results are named after the same mathematician, William Craig. == Recursive axiomatization == Let $A\_1,A\_2,\backslash dots$ be an enumeration of the axioms of a recursively enumerable set T of firstorder formulas. Construct another set T * consisting of :$\backslash underbrace\_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 $A\_1$ or of the form :$\backslash underbrace\_j.$ Since each formula has finite length, it is checkable whether or not it is $A\_1$ 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 $A\_j$; otherwise it is not in T *. Again, it is checkable whether it is in fact $A\_n$ by going through the enumeration of the axioms of T and then checking symbolforsymbol whether the expressions are identical. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Craig's theorem」の詳細全文を読む スポンサード リンク
