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.

PropertyValue
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.
dbpprop:hasPhotoCollection
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.
rdfs:label
  • Craig's theorem
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of