Craig's theorem
= Craig's theorem
{c}
{wiki}
<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.