Complexity of First Order ID-Logic
John Stewart Schlipf, Marc Denecker · 2008
First Order ID-Logic interprets general first order, nonmonotone, inductive definability by generalizing the wellfounded semantics for logic programs. We show that, for general (thus perhaps infinite) structures, inference in First Order ID-Logic is complete Π 1 2 over the natural numbers. We also prove a Skolem Theorem for the logic: every consistent formula of First Order ID-Logic has a countable model.