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 converts an enumeration

A_{1}, A_{2}, \dots

of axioms into a decidable equivalent set by replacing

A_{i}

with a syntactically self-indexing repetition containing

i

copies of

A_{i}

. A candidate of length

m

can only encode one of the first

m

axioms, so membership is decidable after computing that finite prefix.

Independent tagged axiomatization

 0  0

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} \land 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.