On the Computability of Circumscription

Circumscription has been used to formalize the nonmonotonic aspects of common-sense reasoning. The structure of second-order sentences expressing circumscription for which an equivalent first-order sentence can easily be constructed has been studied by Lifschitz (1985). This paper studies the computability aspects of circumscription. We show that even if the circumscription is expressible as a first-order sentence, it is not computable. We also prove the undecidability of determining whether a given set of first-order sentences has a minimal model, a unique minimal model, a finite number of minimal models or an infinite number of minimal models. In addition, we demonstrate the undecidability of determining if the extension of the minimal predicate is finite or infinite, and whether it is expressible as a first-order sentence.