Circumscription

Origin. John McCarthy introduced circumscription (1980) as a formalization of the closed-world assumption and non-monotonic reasoning. "Minimize the extension of abnormality predicates." A form of default reasoning via model-theoretic minimization. Influential in AI knowledge representation alongside default logic and autoepistemic logic.

Models. Reasoning with minimal models. Classical logic can't express "typically" or "unless otherwise stated." Circumscription adds a preference for models where certain predicates have minimal extensions. "Birds fly unless abnormal; assume minimal abnormality." Conclusions hold in all minimal models, not all models.

Formalism.

Basic idea: Given theory T and predicate P to minimize, prefer models where P's extension is smallest (⊆-minimal).

Circumscription of P in T: CIRC[T; P] = T + "P has minimal extension consistent with T"

Second-order formulation: CIRC[T; P] ≡ T(P) ∧ ¬∃P'[T(P') ∧ P' ⊂ P]

"T holds, and there's no smaller P' that also satisfies T."

Prioritized circumscription: Minimize P₁ first, then P₂ among P₁-minimal models, etc. CIRC[T; P₁ > P₂ > ... > Pₙ]

Variable predicates: Some predicates minimized, some fixed, some allowed to vary. CIRC[T; P₁,...,Pₙ; Z₁,...,Zₘ] Minimize P's, allow Z's to vary, fix others.

Example — Birds fly:

Bird(x) ∧ ¬Ab(x) → Flies(x)
Bird(Tweety)
Bird(Opus) ∧ Penguin(Opus)
Penguin(x) → Ab(x)

Circumscribe Ab: minimal abnormality. Result: Ab(Opus), ¬Ab(Tweety), Flies(Tweety), ¬Flies(Opus).

Pointwise circumscription: For each individual separately, assume normality unless forced otherwise.

Formula circumscription: Minimize formulas, not just predicates.

Symbols.

Symbol	Unicode	Name	Meaning
CIRC	—	Circumscription	Minimization operator
Ab	—	Abnormality	Predicate to minimize
⊂	U+2282	Proper subset	Strictly smaller extension
⊆	U+2286	Subset	Smaller or equal extension
¬	U+00AC	Negation	No smaller extension exists
∧	U+2227	Conjunction	Joins the theory to the minimality condition
∨	U+2228	Disjunction	Disjunctive abnormality, from which nothing is minimized
→	U+2192	Material conditional	Object-language implication in the examples
≡	U+2261	Definitional equivalence	Defines the CIRC schema
∃	U+2203	Existential quantifier	Second-order, ranging over predicates
>	—	Priority	Minimize first
T	—	Theory	Axioms being circumscribed
P'	—	Predicate variable	Competing extension for the minimized predicate
Z	—	Variable predicate	Allowed to change while P is minimized
min	—	Minimal	Minimal extension

Metatheory. CIRC[T; P] is the second-order sentence T(P) ∧ ¬∃P'[T(P') ∧ P' ⊂ P], and its models are exactly the models of T that are minimal in the ordering comparing the extension of P with everything else held fixed; consequence from CIRC[T; P] is therefore truth in every P-minimal model of T, and this equivalence is the soundness and completeness statement for the schema. Eiter and Gottlob (1993) settled the propositional case: circumscriptive inference is Π₂ᵖ-complete, and the associated model-checking question — is this particular model minimal? — is co-NP-complete. In first order the consequence relation is not recursively enumerable, so no finitary complete calculus exists. Lifschitz (1985) gave conditions under which the second-order quantifier can be eliminated, so that CIRC[T; P] is equivalent to a first-order sentence for separable theories. For a set of definite Horn clauses, circumscribing all predicates yields exactly the least Herbrand model. Prioritized circumscription unfolds into nested parallel circumscriptions, and parallel, prioritized and pointwise policies are not equivalent.

Applies to. Commonsense reasoning. Default reasoning. Diagnosis (minimize faults). Planning (minimize changes, frame problem). Legal reasoning (exceptions are minimized). Knowledge representation with closed-world assumptions.

Limitations. CIRC[T; P] can be inconsistent while T is consistent: if the models of T admit an infinite strictly descending chain of P-extensions, no model is minimal, the circumscription has no models, and everything follows. Minimality is inclusion, only a partial order, so incomparable minimal models stand on equal footing and disjunctive abnormality yields nothing — from Ab(a) ∨ Ab(b) circumscription concludes neither disjunct. There is no proof theory in the usual sense: the second-order quantifier is eliminable only for restricted classes of theories, and first-order circumscriptive consequence is not recursively enumerable, so completeness is unavailable in principle rather than merely unachieved. The formalism supplies no principle for deciding which predicates are minimized, which vary and which stay fixed, yet the conclusions turn on that choice, and the parallel, prioritized and pointwise policies disagree. Defaults are encoded through abnormality predicates rather than represented, so exceptions to exceptions require further predicates and further priorities.