Complexity of First Order ID-Logic
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 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.