Past exam of the mathematics course of the University of Cambridge / 2010 / iii / Paper 20 / 4 / a / Solution

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.