In mathematical logic, Craig's theorem (also known as Craig's trick) states that any recursively enumerable set of well-formed formulas of a first-order language is recursively axiomatizable, and even primitively recursively axiomatizable, and even decidable in 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.

Let ${\displaystyle A_{1},A_{2},\dots }$ be an enumeration of the axioms of a recursively enumerable set ${\displaystyle T}$ of first-order formulas. Construct another set ${\displaystyle T^{*}}$ consisting of

for each positive integer ${\displaystyle i}$. That is,

The deductive closures of ${\displaystyle T^{*}}$ and ${\displaystyle T}$ are thus equivalent; the proof will show that ${\displaystyle T^{*}}$ is a recursive/decidable set.

Given any formula ${\displaystyle X}$, let its length be ${\displaystyle |X|}$. Then to decide ${\displaystyle X\in T^{*}}$, it suffices to first run the enumeration algorithm until all ${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$ are ouputted, then check if ${\displaystyle X}$ is equal to one of $${\displaystyle A_{1},A_{2}\land A_{2},\dots ,\underbrace {A_{|X|}\land \dots \land A_{|X|}} _{|X|}.}$$

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 ${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$ are ouputted", the enumeration algorithm may take a very long time to output all ${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$.

For primitive recursion, all 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.