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.
Articles by others on the same topic
Craig's theorem is a result in the field of mathematical logic, particularly in model theory. It is named after William Craig, who formulated it in the context of first-order logic. The theorem states that if a set of first-order statements (a theory) has a model, then it has a countable model.