@prefix owl: . owl:sameAs . @prefix foaf: . foaf:page . @prefix rdfs: . rdfs:label "Craig's theorem"@en . @prefix dbpprop: . dbpprop:abstract "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 <math>A_1,A_2,\\dots</math> be an enumeration of the axioms of a recursively enumerable set T of first-order formulas. Construct another set T* consisting of <math>\\underbrace{A_i\\land\\dots\\land A_i}_i</math> 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 <math>A_1</math> or of the form <math>\\underbrace{B_j\\land\\dots\\land B_j}_j. </math> Since each formula has finite length, it is checkable whether or not it is <math>A_1</math> 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 <math>A_j</math>; otherwise it is not in T*. Again, it is checkable whether it is in fact <math>A_n</math> by going through the enumeration of the axioms of T and then checking symbol-for-symbol whether the expressions are identical."@en ; rdfs:comment "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 <math>A_1,A_2,\\dots</math> be an enumeration of the axioms of a recursively enumerable set T of first-order formulas."@en . @prefix skos: . @prefix ns5: . skos:subject ns5:Recursion_theory , ns5:Mathematical_theorems , ns5:Mathematical_logic ; dbpprop:hasPhotoCollection . @prefix dbpedia: . dbpedia:Craig_theorem dbpprop:redirect .