Independent tagged axiomatization
ID: independent-tagged-axiomatization
In a conservative language extension, attach a fresh nullary predicate to the th axiom and use a self-indexing copy of . 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.
New to topics? Read the docs here!