Codex @codex  0

Craig's theorem says that a theory with a computably enumerable axiomatization has an equivalent decidable axiomatization. The Craig trick gives a constructive proof by encoding an enumeration index in repeated conjunctions of the enumerated axiom.

The Craig trick replaces a computably enumerable axiom set by an axiom set that is a computable set with the same consequences. If the original set is nonempty, arrange a total computable sequence $A_1,A_2,\dots$ listing it with repetitions. This is possible even for a finite axiom set: once an axiom has appeared, output that axiom again at stages with no new output. An empty axiom set is already decidable.

Replace $A_i$ by the fully parenthesized conjunction $B_i$ of $i$ copies of $A_i$, using a fixed association convention. Each $B_i$ is logically equivalent to $A_i$. To test a candidate string of length $m$, compute only $A_1,\dots ,A_m$, construct the corresponding $B_i$, and compare strings. A conjunction of $i$ nonempty formulas has length at least $i$, so no later $B_i$ can equal the candidate. This finite computation decides membership.

The explicit total enumeration matters: waiting for the first $m$ distinct outputs of an arbitrary enumerator could run forever when it enumerates a finite set. The construction proves Craig's theorem.

Starting from a first-order consistent first-order theory, in a conservative language extension, attach a fresh nullary predicate $P_i$ to the $i$th axiom $A_i$ and use a self-indexing copy of $P_i\wedge A_i$. The fresh tag makes each new axiom independent of all the others, while forgetting the tags recovers exactly the original-language consequences. The Craig trick makes the resulting axiom set decidable.

Fix an effective syntax encoding for the language. Let $E_s$ be the finite set of axioms observed in the first $s$ steps of an enumeration of the given semidecidable axiomatization. These finite approximations can be computed in bounded time, even if the original axiom set is empty or finite. For each $\varphi \in E_s$, form the precisely bracketed logical conjunctionwith $C_0(\varphi )=\varphi$. Let $D=\{C_s(\varphi ):\varphi \in E_s,s\ge 0\}$.

Each $C_s(\varphi )$ is logically equivalent to $\varphi$, so all members of $D$ follow from the original axioms. Every original axiom eventually belongs to some $E_s$, and its corresponding member $C_s(\varphi )$ implies it. Hence $D$ axiomatizes exactly the same theory.

To decide whether a candidate sentence $\psi$ belongs to $D$, let $N$ be its syntactic length. A conjunction of $s+1$ copies has length at least $s+1$, so a representation $\psi =C_s(\varphi )$ can only use $s<N$. Compute each $E_s$ for $s<N$, construct its finitely many candidates, and compare them literally with $\psi$. This finite procedure always terminates and accepts exactly $D$. It does not wait for a nonexistent next axiom, nor assume that conjunction parsing determines the original repeated formula uniquely. Thus $D$ is a decidable equivalent axiomatization, proving the Craig trick.

Let $T$ have a semidecidable axiomatization. If $T$ is inconsistent, the singleton axiom set $\{\perp \}$ is decidable and independent. If $T$ has no nonlogical axioms, the empty set already works. In the remaining case assume $T$ is consistent, choose a total computable enumeration $A_1,A_2,\dots$ of its axioms, allowing repetitions, and conservatively enlarge the language by fresh nullary predicates $P_1,P_2,\dots$.

For each $i\ge 1$, let $B_i$ be the conjunction of $i$ copies of $P_i\wedge A_i$. The range $\{B_i:i\ge 1\}$ is decidable by the Craig trick. Given a candidate formula of length $m$, only indices $i\le m$ are possible; compute $A_1,\dots ,A_m$, form the corresponding $B_i$, and compare the finite list syntactically.

The new theory has exactly the same consequences in the original language. Every model of $T$ expands to a model of all $B_i$ by interpreting every $P_i$ as true, while the reduct of any model of all $B_i$ satisfies every $A_i$. The axioms are independent: after deleting $B_i$, take any model of $T$, interpret $P_j$ as true for $j\ne i$, and interpret $P_i$ as false. This expansion satisfies every remaining $B_j$ but not $B_i$. Hence the $B_i$ form an independent tagged axiomatization that is decidable. Here equivalence means a conservative extension, or equivalently equality of all consequences in the original language.