= Craig trick
{c}
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,\ldots$ 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,\ldots,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>.
Back to article page
