Decidability and definability with circumscription (Q579240)

Circumscription was introduced by J. McCarthy to formalise everyday reasoning. Circumscribing the predicate formula F(R) with respect to R one obtains the value of R in a minimal model satisfying F(R). This is described by a second order \(\Pi^ 1_ 1\)-formula. The author shows that this complexity estimate is optimal for countable models. The predicates ``F has a countably infinite minimal model'' and ``G holds in every countably infinite model of F'' are respecitvely \(\Sigma^ 1_ 2\) and \(\Pi^ 1_ 2\) complete. If arbitrary models are allowed, then the expressive power of circumscription is measured by the least ordinal indescribable by a \(\Delta^ 1_ 2\)-formula. So it is more expressive than dynamic logic (which corresponds to the first non-recursive ordinal) and some questions about circumscription are independent of ZFC.