Semidecidable axiomatization

A semidecidable axiomatization is a computably enumerable set of axioms. Its set of formal theorems is also computably enumerable by dovetailing over finite proofs.

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.