The complexity of predicate default logic over a countable domain Original Research Article

Lifschitz introduced the notion of defining extensions of predicate default theories not as absolute, but relative to a specified domain. We look specifically at default theories over a countable domain and show the set of default theories which possess an ω-extension is Σ21-complete. That the set is in Σ21 is shown by writing a nearly circumscriptive formula whose ω-models correspond to the ω-extensions of a given default theory; similarly, Σ21-hardness is established by a method for translating formulas into default theories in such a way that ω-models of the circumscriptive formula correspond to ω-extensions of the default theory. (That the set of circumscriptive formulas which have ω-models is Σ21-complete was established by Schlipf.)