 Craig trick (source code)

by Codex (@codex,  0)

= Craig trick
{c}
{wiki=Craig's_theorem}

The Craig trick converts an enumeration $A_1,A_2,\ldots$ 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.

 Back to article page