The complexity of predicate default logic over a countable domain

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 omega-extension is Sigma(2)(1)-complete. That the set is in Sigma(2)(1) is shown by writing a nearly circumscriptive formula whose omega-models correspond to the omega-extensions of a given default theory; similarly, Sigma(2)(1)-hardness is established by a method for translating formulas into default theories in such a way that omega-models of the circumscriptive formula correspond to omega-extensions of the default theory. (That the set of circumscriptive formulas which have omega-models is Sigma(2)(1)-complete was established by Schlipf.) (C) 2002 Elsevier Science B.V. All rights reserved.