In [[mathematical logic]], '''Craig's theorem''' (also known as '''Craig's trick''') states that any [[recursively enumerable set]] of [[well-formed formula]]s of a [[first-order language]] is recursively [[axiomatization|axiomatizable]], and even primitively recursively axiomatizable, and even decidable in [[Time complexity|polynomial time]].

This result is not related to the well-known [[Craig interpolation]] theorem, although both results are named after the same logician, [[William Craig (philosopher)|William Craig]].

== Recursive axiomatization ==

Let <math>A_1,A_2,\dots</math> be an enumeration of the axioms of a recursively enumerable set <math>T</math> of first-order formulas. Construct another set <math>T^*</math> consisting of

:<math>\underbrace{A_i\land\dots\land A_i}_i</math>

for each positive integer <math>i</math>. That is,

:<math>T^* = \{ A_1, A_2 \land A_2, A_3 \land A_3 \land A_3, \ldots \}</math>

The [[deductive closure]]s of <math>T^*</math> and <math>T</math> are thus equivalent; the proof will show that <math>T^*</math> is a recursive/decidable set.

Given any formula <math>X</math>, let its length be <math>|X|</math>. Then to decide <math>X \in T^*</math>, it suffices to first run the enumeration algorithm until all <math>A_1, A_2, \dots, A_{|X|}</math> are ouputted, then check if <math>X</math> is equal to one of <math display="block">A_1, A_2 \and A_2, \dots, \underbrace{A_{|X|}\and\dots\and A_{|X|}}_{|X|}. </math>

== Primitive recursive axiomatization ==

A set of axioms is [[primitive recursive]] if there is a primitive recursive function that decides membership in the set. The algorithm given above is recursive, but not necessarily primitive recursive. The main issue is that, at the part where we "run the enumeration algorithm until all <math>A_1, A_2, \dots, A_{|X|}</math> are ouputted", the enumeration algorithm may take a very long time to output all <math>A_1, A_2, \dots, A_{|X|}</math>.

For primitive recursion, all [[Loop (statement)|loops]] must be bounded by a pre-computed upper bound. Consequently, we are not allowed to say "run the enumeration algorithm until...". However, we can say "run the enumeration algorithm for up to ''k'' steps", provided that we know what ''k'' should be.

Now, instead of replacing a formula <math>A_i</math> with

:<math>\underbrace{A_i\land\dots\land A_i}_i</math>

one replaces it with

:<math>\underbrace{A_i\land\dots\land A_i}_{f(i)}</math> (*)

where <math>f</math> is a function that, given <math>i</math>, returns the number of steps the enumeration Turing machine takes in order to output <math>A_i </math>. In fact, this construction gives a decision algorithm that runs in [[polynomial time]], which is a particularly well-behaved class of primitively recursive functions.

== Applications == The theorem has been used in proofs of [[Gödel's incompleteness theorems]]. One would first prove the theorems for all theories that with a set of axioms that is primitive recursive, then apply Craig's theorem to immediately conclude that the theorems hold for all theories with a set of axioms that is recursively enumerable.<ref name="SmithDef">{{Cite book |last=Smith |first=Peter |url=https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf |title=An introduction to Gödel's theorems |publisher=Logic Matters |year=2013 |isbn=979-8-6738-6213-1 |edition=2 |location=England |chapter=26. Broadening the scope}}</ref>

== Philosophical implications == If <math>T</math> is a recursively axiomatizable theory and we divide its predicate symbols into two [[disjoint sets]] <math>V_A</math> and <math>V_B</math>, then those theorems of <math>T</math> that are in the vocabulary <math>V_A</math> are recursively enumerable, and hence, based on Craig's theorem, axiomatizable. [[Carl Gustav Hempel|Carl G. Hempel]] argued based on this that since all science's predictions are in the vocabulary of observation terms, the theoretical vocabulary of science is in principle eliminable. He himself raised two objections to this argument: 1) the new axioms of science are practically unmanageable, and 2) science uses [[inductive reasoning]] and eliminating theoretical terms may alter the inductive relations between observational sentences. [[Hilary Putnam]] argues that this argument is based on a misconception that the sole aim of science is successful prediction. He proposes that the main reason we need theoretical terms is that we wish to talk about theoretical entities (such as viruses, radio stars, and elementary particles).

== References == {{Reflist}}

* {{cite book |last=Hempel |first=C. G. |chapter=Implications of Carnap's Work for the Philosophy of Science |date=1963 |publisher=Open Court |editor-last=Schilpp |editor-first=P. A. |location=La Salle, Illinois |pages=685–709 |title=The Philosophy of Rudolf Carnap}}

* {{cite journal |last=Craig |first=William |date=1953 |title=On Axiomatizability Within a System |journal=The Journal of Symbolic Logic |volume=18 |issue=1 |pages=30–32 |doi=10.2307/2266324}}

* {{cite journal |last=Putnam |first=Hilary |date=1965 |title=Craig's Theorem |journal=The Journal of Philosophy |volume=62 |issue=10 |pages=251–260 |doi=10.2307/2023298}}

[[Category:Computability theory]] [[Category:Theorems in the foundations of mathematics]]