Circumscription

Witold Łukaszewicz: Nonmonotonic reasoning: Formalization of Common-Sense Reasoning, Ellis Horwood, 1990.

Second-order logic

Alphabet:

1. A denumerable set of n-ary (for each n≥0) function variables: {ϕ_{1}^{n}, ϕ_{2}^{n}, …}; 0-ary function variables are called individual variables, and we denote them by x_{1}, x_{2}, . . ..

2. A denumerable set of n-ary (for each n≥0) predicate variables: {Φ_{1}^{n}, Φ_{2}^{n}, …}.

3. Truth constants: T rue and F alse.

4. Standard sentential connectives and quantifiers.

5. A countable set P of predicate constants.

6. A distinguished 2-ary predicate constant: “=”.

7. A countable set F of function constants.

Terms

(1) Each individual variable is a term.

(2) Each individual constant is a term.

(3) If f is an n-ary (n>0) function constant and α_{1}, … α_{n} are terms, then f(α_{1}, … α_{n}) is a term.

(4) If ϕ is an n-ary (n>0) function variable and α_{1}, … α_{n} are terms, then ϕ(α_{1}, … α_{n}) is a term.

Examples of terms:

x, f(a, y), ϕ(x, ϕ(b, z)).

Atomic formulas

(1) T rue, F alse and all proposition constants are atomic formulas.

(2) If P is an n-ary (n>0) predicate constant and α_{1}, … α_{n} are terms, then P (α_{1}, … α_{n}) is an atomic formula.

(3) If α and β are terms, then (α = β) is an atomic formula.

(4) Each proposition variable is an atomic formula.

(5) If Φ is an n-ary (n>0) predicate variable and α_{1}, … α_{n} are terms, then Φ(α_{1}, … α_{n}) is an atomic formula.

Examples of atomic formulas:

P (ϕ(a), a), Φ(b, x, ϕ(x)), (b = ϕ(y)).

Formulas

(1) Each atomic formula is a formula.

(2) If A is a formula, then so is (¬A).

(3) If A and B are formulas, then (A ⊃ B), (A ∧ B), (A ∨ B) and (A ≡ B) are formulas.

(4) If A is a formula and X is any variable, then (∀X(A)) and (∃X(A)) are formulas.

Examples of formulas:

(∀xΦ(x)), (∀x∃Ψ(¬Ψ(x) ∨ Φ(x)))

Semantics

Definition A frame for a second-order language L_{AL} is a pair M=⟨D,m⟩, where D is a non-empty set, the domain of M, and m is a function which assigns to each n-ary (n≥0) predicate constant in AL, different from “=”, an n-ary relation on D, to the constant “=”, the identity relation on D, and to each n-ary (n≥0) function constant in AL, an n-ary function from D^{n} into D.

Given a frame M=⟨D,m⟩, we write |M| to denote the domain of M; M|K| stands for m(K), where K is any function or predicate constant in AL.

Definition An assignment over M is any function which assigns to every n-ary (n≥0) function variable an n-ary function from |M|^{n} into |M|, and to each n-ary (n≥0) predicate variable an n-ary relation on M.

The set of all assignments over M will be denoted by As(M).

If a∈As(M) and X is any variable, then we write [a]_{X} to denote the set of those assignments over M which differs from “a” at most on X.

Definition The value V_{a}^{M}(α) of a term α in a frame M with respect to a∈As(M) is an element of |M| defined as follows:

(1) V_{a}^{M}(x) = a(x);

(2) V_{a}^{M}(a) = M|a|;

(3) V_{a}^{M}(f(α_{1}, … α_{n})) = = M|f|[V_{a}^{M}(α_{1}), …, V_{a}^{M}(α_{n})];

(4) V_{a}^{M}(ϕ(α_{1}, … α_{n})) = = a(ϕ)[V_{a}^{M}(α_{1}), …, V_{a}^{M}(α_{n})]; Definition The value V_{a}^{M}(A) of an atomic formula A in M with respect to a∈As(M) is an element of {0, 1} defined as follows:

(1) V_{a}^{M}(T rue) = 1; V_{a}^{M}(F alse) = 0;

(2) V_{a}^{M}(p) = M|p|;

(3) V_{a}^{M}(P (α_{1}, … α_{n})) = = M|P |[V_{a}^{M}(α_{1}), …, V_{a}^{M}(α_{n})];

(4) V_{a}^{M}(α = β) = 1 iff V_{a}^{M}(α) = V_{a}^{M}(β);

(5) V_{a}^{M}(Φ^{0}) = a(Φ^{0});

(6) V_{a}^{M}(Φ(α_{1}, … α_{n})) = = a(Φ)[V_{a}^{M}(α_{1}), …, V_{a}^{M}(α_{n})].

Definition The value V_{a}^{M}(A) of a non-atomic formula A in M with respect to a∈As(M) is an element of {0, 1} defined as follows:

(1) VM a(¬B) = 1 − VM a(B);

(2) VM a(B ⊃ C) = 1 iff VM a(B) = 0 or VM a(C) = 1;

(3) VM a(B ∨ C) = 1 iff VM a(B) = 1 or VM a(C) = 1;

(4) VM a(B ∧ C) = 1 iff VM a(B) = 1 and VM a(C) = 1;

(5) VM a(B ≡ C) = 1 iff VM a(A) = VM a(B);

(6) VM a(∀X B) = 1 iff V{M \atop a’}(B) = 1, for every a’ ∈ [a]_{X};

(7) VM a(∃X B) = 1 iff V{M \atop a’}(B) = 1, for some a’ ∈ [a]_{X}.

A formula A is said to be satisfied in M by an assignment a∈ As(M) iff V_{a}^{M}(A) = 1.

A is satisfiable iff V_{a}^{M}(A) = 1, for some M and some a∈ As(M).

A is true in M iff V_{a}^{M}(A) = 1, for any a∈ As(M). In this case we say that M is a model of A.

A is valid iff A is true in every frame.

Theorem The validity problem for second-order logic is undecidable. The problem is even not semi-decidable.

A second-order theory is a computable set of formulas. The formulas from a theory T are called the axioms (premisses) of T.

A frame in which all the axioms of a theory T are true is called a model of T.

A theory T is called satisfiable iff it has a model.

A formula A is entailed by a theory T, written T ⊧ A, iff A is true in every model of T.

Theories T and T ’ are said to be equivalent, written T ⇔ T ’, iff they have the same models.

Theorem If T = {A_{1}, …, A_{n}}, then

T ⇔ {A_{1} ∧ ⋯ ∧ A_{n}}.

THEOREM (Gödel) There is no complete deduction system for second-order logic.

Predicate and function expressions

Definition An n-ary predicate expression U is any expression of the form

λx_{1} … x_{n} A(x_{1}, …, x_{n}) (n ≥ 0)

where x_{1}, …, x_{n} are individual variables and A(x_{1}, …, x_{n}) is a formula of first- or second-order logic.

U = λx_{1} … x_{n} A(x_{1}, …, x_{n})

An occurrence of X is said to be free in U iff X ∉ {x_{1}, …, x_{n}} and X is free in A(x_{1}, …, x_{n}).

Any individual variable which is free in U is called a parameter in U.

If no parameters occur in U, then U is called a predicate expression without parameters. Otherwise U is called a predicate expression with parameters.

λx P (x); λxy [Φ(x) ∨ Q(y)]; λx Q(x, y)

Definition Let U be a predicate expression of the form λx_{1} … x_{n} A(x_{1}, …, x_{n}). The extension E_{a}^{M}(U) of U in a frame M with respect to a∈As(M) is an n-ary relation R on |M| given by

⟨d_{1}, …, d_{n}⟩ ∈ R iff

V_{a(x_{1}/d_{1},...x_{n}/d_{n})}^{M}(A) = 1

where a(x_{1}/d_{1}, … x_{n}/d_{n}) is the assignment on M which is like “a”, except perhaps on the variables x_{1}, …, x_{n}; here it assigns d_{1}, …, d_{n}, respectively.

Note:

(1) For each n-ary predicate constant P: E_{a}^{M}[λx_{1} … x_{n} P (x_{1}, …, x_{n})] = M|P |.

(2) For each n-ary predicate variable Φ: E_{a}^{M}[λx_{1} … x_{n} Φ(x_{1}, …, x_{n})] = a(Φ).

λx A(x) stands for λx_{1} … x_{n} A(x_{1}, …, x_{n}).

Let U = λx A(x), where x = (x_{1}, …, x_{n}), and let α = (α_{1}, …, α_{n}) be an n-tuple of terms. The application of U to α, written U(α), is the formula A(α).

The application is correct iff each α_{i} is free for x_{i} in A(x).

Examples

(1) If U = λxy P (x, y) and α = (z, f(b)), then U(α) = P (z, f(b)). This is correct application.

(2) If U = λxy ∃z P (x, y, z) and α = (z, f(a)), then U(α) = ∃z P (z, f(a), z). This is incorect application.

A substitution of predicate expressions for predicate variables is a set

{Φ_{1} ← U_{1}, …, Φ_{n} ← U_{n}} (n ≥ 0)

where Φ_{1}, …, Φ_{n} are distinct predicate variables, U_{1}, …, U_{n} are predicate expressions and the corresponding Φ_{i} and U_{i} have the same arities.

Definition The application of a substitution θ = {Φ_{1} ← U_{1}, …, Φ_{n} ← U_{n}} to a formula A, written Aθ, is the formula obtained from A by the following construction:

(1) Replace each free occurrence of Φ_{i} in A by ⌊U_{i}⌋.

(2) In the expression resulted from (1), which in general is not a formula, successively replace each part of the form ⌊U_{i}⌋(α) by the application of U_{i} to α.

The application of θ to A is proper iff

(i) All the applications (of predicate expressions to terms) performed in (2) are correct. (ii) No free occurrence of any variable in any of U_{1}, …, U_{n} becomes bound in Aθ.

Example Let A = ∀xΦ(x) ⊃ ∀xΦ(b); θ = {Φ ← λyP (x, y)}. Applying θ to A, we first get

∀x ⌊λy P (x, y)⌋(x) ⊃ ∀x ⌊λy P (x, y)⌋(b) and then

∀x P (x, x) ⊃ ∀x P (x, b).

Example Let

A = ∀xΦ(x)⊃Φ(y); θ = {Φ ← λx∃yQ(x, y)}.

Applying θ to A, we first get

∀x ⌊λx ∃y Q(x, y)⌋(x) ⊃ ⌊λx ∃y Q(x, y)⌋(y)

and then

∀x ∃y Q(x, y) ⊃ ∃y Q(y, y).

This is an improper application because the application of λx ∃y Q(x, y) to y is not correct (y is not free for x in ∃y Q(x, y)).

Example Let A = ∀xy(Φ(x, y) ∨ Ψ(x, y)) θ = {Φ ← λxyP (x, y), Ψ ← λuvQ(u, v)}.

Applying θ to A we first obtain ∀xy(⌊λxyP (x, y)⌋(x, y) ∨ ⌊λuvQ(u, v)⌋(x, y)) and then

∀xy(P (x, y) ∨ Q(x, y)).

This is a proper application.

Theorem For any formula A and any substitution θ = {Φ_{1} ← U_{1}, …, Φ_{n} ← U_{n}}, the formula

(∀Φ_{1} … Φ_{n}A) ⊃ Aθ

is valid, provided that the application of θ to A is proper.

Corollary For any sentence of the form ∀Φ_{1} … Φ_{n}A and any substitution θ = {Φ_{1} ← U_{1}, …, Φ_{n} ← U_{n}},

∀Φ_{1} … Φ_{n}A ⊧ Aθ

provided that the application of θ to A is proper.

Definition An n-ary function expression F is any expression of the form

λx_{1} … x_{n} α(x_{1}, …, x_{n}) (n ≥ 0)

where x_{1}, …, x_{n} are individual variables and α(x_{1}, …, x_{n}) is a term.

The following are function expressions:

λxf(x); λxy f(g(x), y); λxϕ(x, y).

An n-ary function expression is meant to represent an n-ary function.

Circumscription

We distinguish between:

• a predicate, thought of as a particular relation specified over a particular domain, and

• predicate expressions, including predicate constants and predicate variables, which can be used to denote this relation.

Recall:

• An n-ary predicate constant P can be identified with the predicate expression λx_{1} … x_{n} P (x_{1} … x_{n}).

• An n-ary predicate variable Φ can be identified with the predicate expression λx_{1} … x_{n} Φ(x_{1} … x_{n}).

• The predicate denoted by a predicate expression U is called the extension of U.

General idea of circumscription

The objects (tuples of objects) that can be shown to satisfy a certain predicate are the only objects (tuples of objects) enjoying it.

More specifically: Given a theory T and an n-ary predicate constant P, to circumscribe P in T is to assume that the extension of P is minimal in the sense that it cannot be made smaller without contradicting T.

Circumscription is thus a form of minimization: to circumscribe a predicate constant is to minimize its extension.

Let T consist of

Red(a) ∧ On(a, b).

Circumscribing Red in T, we expect to infer

∀x Red(x) ⊃ x = a.

Circumscribing On in T, we expect to derive

∀xy. On(x, y) ⊃ x = a ∧ y = b.

Circumscription can be also used to minimize extensions of several predicates.

All versions of circumscription share the following common characteristics:

• Unlike other non-monotonic formalisms, circumscription allows us to formalize non-monotonic reasoning directly in the language of classical first-order logic.

• It is always the task of the user to specify predicates which are to be minimized. Circumscription provides a general method which can be applied to arbitrarily chosen predicates.

• Circumscription is based on syntactic manipulations. Given a theory T and a list of predicate constants P_{1}, … P_{n}, circumscription of P_{1}, … P_{n} in T amounts to implicitly adding a special second-order sentence (a set of first-order formulas, in some versions of circumscription) capturing the desired minimization.

Abnormality formalism

(1) How the common-sense knowledge, including non-monotonic rules, is to be represented in the framework of circumscription?

(2) Which predicates are to be minimized to assure intuitively acceptable conclusions?

Ab − abnormal

∀x. Bird(x) ∧ ¬Ab(x) ⊃ F lies(x)

(1) Bird(T weety)

(2) ∀x. Bird(x) ∧ ¬Ab(x) ⊃ F lies(x).

Conclusions: ∀x¬Ab(x) ∀x. Bird(x) ⊃ F lies(x) F lies(T weety).

(3) Bird(Clyde) ∧ ¬F lies(Clyde)

Conclusions: ∀x. x ≠ Clyde ⊃ ¬Ab(x) ∀x. Bird(x) ∧ x ≠ Clyde ⊃ F lies(x).

(1) Bird(T weety)

(2) ∀x. Bird(x) ∧ ¬Ab(x) ⊃ F lies(x)

(3) P enguin(Joe)

(4) ∀x. P enguin(x) ⊃ Bird(x).

Conclusion:

F lies(Joe).

How to block this conclusion?

∀x. P enguin(x) ⊃ ¬F lies(x).

∀x. P enguin(x) ⊃ Ab(x).

∀x. P enguin(x) ∧ ¬Ab(x) ⊃ ¬F lies(x). This is incorrect representation.

∀x. P enguin(x) ∧ ¬Ab_{1}(x) ⊃ ¬F lies(x). Ab and Ab_{1} should be jointly minimized. Unfortunately, there is a conflict. Minimization _{1}: ¬Ab(Joe) and F lies(Joe) Minimization _{2}: ¬Ab_{1}(Joe) and ¬F lies(Joe).

∀x. P enguin(x) ⊃ Ab(x).

There are nm rules requiring many-place abnormality predicates:

“In the absence of evidence to the contrary, assume that x gives y a gift, provided that y has a birthday and x is a friend of y”.

∀xy. Birthday(y) ∧ F riend(x, y) ∧ ¬Ab(x, y) ⊃

⊃ Gives − Gift(x, y).

Here Ab(x, y) should be read: “x behaves abnormally with respect to y in the situation where y has a birthday and x is a friend of y”.

Predicate circumscription (McCarthy 1980)

L - a fixed first-order language with equality.

The objects under consideration are finite sets of sentences from L, referred to as theories.

Recall that every such a theory can be identified with a single sentence, namely with the conjunction of all its members.

We write T (P_{1}, … P_{n}) to indicate that some (but not necessarily all) of predicate constants occurring in T are among P_{1}, … P_{n}.

L_{2} - a second-order language whose alphabet is that of L, together with an infinite set of n-place (n≥0) predicate variables.

Let U and V be n-ary predicate expressions. We write

U ≤ V for ∀x. U(x) ⊃ V (x)

where x = (x_{1}, … x_{n}) is a new n-tuple of individual variables and ∀x stands for ∀x_{1} ⋯ ∀x_{n}.

Note: U ≤ V states that the extension of U is a subset (not necessarily proper) of the extension of V.

Let U and V, where U = (U_{1}, …, U_{n}) and V = (V_{1}, …, V_{n}), be similar tuples of predicate expressions, i.e. U_{i} and V_{i} have the same arities, for each 1 ≤ i ≤ n. We write U ≤ V to denote the sentence

n ; ⋀ ; i=1 [U_{i} ≤ V_{i}] i.e. n ; ⋀ ; i=1 [∀x. U_{i}(x) ⊃ V_{i}(x)].

U ≤ V states that the extension of each member of U is a subset (not necessarily proper) of the extension of the corresponding member of V.

Let T (P_{1}, …, P_{n}) be a theory. How to express the fact that the extensions of P_{1}, …, P_{n} are minimal with respect to T, i.e. none of them can be made smaller without contradicting T?

∀Φ_{1} … Φ_{n}.

[T (Φ_{1}, …, Φ_{n}) ∧ n ; ⋀ ; i=1 (Φ_{i} ≤ P_{i})] ⊃ n ; ⋀ ; i=1 (P_{i} ≤ Φ_{i}).

Here Φ_{1}, …, Φ_{n} are predicate variables with the same arities as P_{1}, …, P_{n}, respectively. T (Φ_{1}, …, Φ_{n}) is the sentence obtained from T (P_{1}, …, P_{n}) by replacing all occurrences of P_{1}, …, P_{n} by Φ_{1}, …, Φ_{n}, respectively.

Notice: The presence of T (Φ_{1}, …, Φ_{n}) in the above formula assures that the extensions of P_{1}, …, P_{n} are minimized relative to T.

Definition The circumscription schema of P_{1}, …, P_{n} in T, denoted by CS (T; P_{1}, …, P_{n}), is the second-order formula

[T (Φ_{1}, …, Φ_{n}) ∧ n ; ⋀ ; i=1 [Φ_{i} ≤ P_{i}]] ⊃ n ; ⋀ ; i=1 [P_{i} ≤ Φ_{i}]

or, equivalently

[T (Φ_{1}, …, Φ_{n}) ∧ n ; ⋀ ; i=1 [∀x. Φ_{i}(x) ⊃ P_{i}(x)]] ⊃

⊃ n ; ⋀ ; i=1 [∀x. P_{i}(x) ⊃ Φ_{i}(x)]

where Φ_{1}, …, Φ_{n} and T (Φ_{1}, …, Φ_{n}) are defined as before.

Example Let T = {Red(a) ∧ On(a, b)}.

CS(T; Red) =

[Φ(a) ∧ On(a, b) ∧ [∀x. Φ(x) ⊃ Red(x)]] ⊃

⊃ [∀x. Red(x) ⊃ Φ(x)].

Definition Let T (P_{1}, …, P_{n}) be a theory and let CS (T; P_{1}, …, P_{n}) be the set of all formulas obtainable from CS (T; P_{1}, …, P_{n}) by proper substitutions of first-order predicate expressions for Φ_{1}, …, Φ_{n}. The predicate circumscription of P = (P_{1}, …, P_{n}) in T, written CIRC_{PR}(T; P), is T ∪ CS (T; P_{1}, …, P_{n}).

The set of theorems derivable by circumscribing P = (P_{1}, …, P_{n}) in T is identified with the set of theorems classically derivable from CIRC_{PR}(T; P).

Example Let T = {Red(a) ∧ On(a, b)}. CS(T; Red) = [Φ(a)∧On(a, b)∧[∀x. Φ(x) ⊃ Red(x)]] ⊃ [∀x. Red(x) ⊃ Φ(x)].

We show that CIRC_{PR}(T; Red) ⊧ ∀x. Red(x) ⊃ x = a (1)

Substituting λx x = a for Φ, we get [a = a ∧ On(a, b) ∧ [∀x. x = a ⊃ Red(x)]] ⊃

⊃ [∀x. Red(x) ⊃ x = a].

From this, we immediately conclude (1).

Example We circumscribe “=” in T = {P (a)}. CS(T; =) = [P (a) ∧ [∀xy. Φ(x, y) ⊃ x = y]] ⊃ [∀xy. x = y ⊃ Φ(x, y)].

Putting {Φ ← λxy F alse}, we get [P (a) ∧ [∀xy. F alse ⊃ x = y]] ⊃ [∀xy. x = y ⊃ F alse] which is equivalent to

P (a) ⊃ ∀xy. x ≠ y.

Since T ⊢ P (a), we finally conclude that CIRC_{PR}(T; =) is inconsistent.

Semantics for predicate circumscription

Definition Let T (P_{1}, …, P_{n}) be a theory, some of whose predicate constants are among P = (P_{1}, …, P_{n}). A model M of T is a P -submodel of a model N of T, written M≤^{P} N, iff

(1) |M| = |N|;

(2) M|P | ⊆ N|P |, for every predicate constant P in P;

(3) M|K| = N|K|, where K is any function constant or any predicate constant not in P.

M is a P -minimal model of T iff every model of T which is a P -submodel of M is identical with M.

Theorem If CIRC_{PR}(T; P) ⊢ A, then A is true in every P -minimal model of T.

Example Let T consist of:

Bird(T weety)
∀x. Bird(x) ∧ ¬Ab(x) ⊃ F lies(x).

Consider the frame M, where:

|M|={TWEETY}; M|F lies|={};
M|Bird|=M|Ab|={TWEETY}.

M is an Ab-minimal model of T (we cannot make M|Ab| smaller without contradicting T). Thus, since F lies(T weety) is false in M, this formula cannot be derived by circumscribing Ab in T.

This example illustrates a more general phenomenon:

THEOREM: Neither positive nor negative new ground instances of uncircumscribed predicates can be derived by predicate circumscription.

In view of the above theorem, predicate circumscription is generally incapable to deal with non-monotonic rules!

Reason: While minimizing the extensions of circumscribed predicates, predicate circumscription keeps the extensions of all other predicates fixed.

Second-order circumscription (McCarthy, Lifschitz)

Second-order circumscription extends predicate circumscription in three ways:

1. The process of minimization is expressed by a special circumscription axiom, being a single second-order sentence rather than a set of first-order formulas.

2. The extensions of arbitrarily chosen predicate constants, also of those not minimized, may be varied during the minimization.

3. The extensions of arbitrarily chosen function constants may be also allowed to vary in the process of minimization.

Recall:

(1) If U and V are predicate expressions of the same arity, then U ≤ V stands for ∀x. U(x) ⊃ V (x).

(2) If U = (U_{1}, …, U_{n}) and V = (V_{1}, …, V_{n}) are similar tuples of predicate expressions, then U ≤ V stands for

n ; ⋀ ; i=1 [U_{i} ≤ V_{i}] i.e. n ; ⋀ ; i=1 [∀x. U_{i}(x) ⊃ V_{i}(x)].

(3) We write U = V for (U ≤ V) ∧ (V ≤ U), and U < V for (U ≤ V) ∧ ¬(V ≤ U).

Definition Let P be a tuple of distinct predicate constants, let S be a tuple of distinct function and/or predicate constants disjoint with P, and suppose that T (P , S) is a first- or second-order theory. The second-order circumscription of P in T with variable S, written CIRC_{SO} (T; P; S), is the sentence

T (P , S) ∧ ∀Φ Ψ ¬[T (Φ , Ψ ) ∧ Φ < P]

where Φ and Ψ are tuples of variables similar to P and S, respectively.

A formula A is said to be a consequence of second-order circumscription of P in T with variable S iff CIRC_{SO} (T; P; S) ⊧ A.

CIRC_{SO} (T; P; S) can be rewritten as

T (P , S) ∧ ∀Φ Ψ (T (Φ , Ψ ) ∧ (Φ ≤ P) ⊃ (P ≤ Φ )) which, in turn, is an abbreviation for T (P , S) ∧ ∀Φ Ψ

[(T (Φ , Ψ ) ∧ n ; ⋀ ; i=1 [∀x. Φ_{i}(x) ⊃ P_{i}(x)]) ⊃

⊃ n ; ⋀ ; i=1 [∀x. P_{i}(x) ⊃ Φ_{i}(x)]] .

Example Let T = {Bird(T weety)∧

∧ [∀x. Bird(x) ∧ ¬Ab(x) ⊃ F lies(x)]}.

We take P = (Ab) and S = (F lies).

CIRC_{SO} (T; P; S) = T (P , S) ∧ ∀ΦΨ

(Bird(T weety) ∧ [∀x. Bird(x) ∧ ¬Φ(x) ⊃ Ψ(x)]∧

∧ [∀x. Φ(x) ⊃ Ab(x)]) ⊃ ∀x. Ab(x) ⊃ Φ(x).

Taking {Φ←λxF alse; Ψ←λxBird(x)}, we get:

CIRC_{SO} (T; P; S) ⊧ ∀x. Ab(x) ⊃ F alse

CIRC_{SO} (T; P; S) ⊧ ∀x. ¬Ab(x)

CIRC_{SO} (T; P; S) ⊧ ∀x. Bird(x) ⊃ F lies(x)

CIRC_{SO} (T; P; S) ⊧ F lies(T weety).

Semantics for second-order circumscription

Theorem Let P, S and T (P , S) be as before. Let M and N be models of T. M is a (P; S)-submodel of N, written M≤^{(P;S)} N, iff

(1) |M| = |N|;

(2) M|P | ⊆ N|P |, for every predicate constant P in P;

(3) M|K| = N|K|, for any function or predicate constant K not in P , S.

We write M<^{(P;S)} N iff M≤^{(P;S)} N but not N≤^{(P;S)} M. A model M of T is (P; S)-minimal iff T has no model N such that N<^{(P;S)} M.

MOD ^{(P;S)} (T) - the class of all (P; S)- minimal models of T. MOD(T) - the class of all models of T.

Theorem For any T, P and S, MOD(CIRC_{SO} (T; P; S) )=MOD ^{(P;S)} (T).

Satisfiability of second-order circumscription

Theorem Second-order circumscription need not preserve satisfiability.

Definition A theory T is well-founded with respect to (P; S) iff, for every M∈MOD(T), there is N∈ MOD ^{(P;S)} (T) such that N≤^{(P;S)} M.

Theorem If T is satisfiable and well-founded with respect to (P; S), then CIRC_{SO} (T; P; S) is satisfiable.

Well-foundedness is not necessary for satisfiability of secondorder circumscription.

A sentence is said to be universal iff its prenex normal form contains no existential quantifiers. A theory is said to be universal iff all of its axioms are universal.

Theorem If T is universal, then T is well-founded with respect to any (P; ()).

Corollary For any tuple of predicate constants P and any satisfiable universal theory T, CIRC_{SO} (T; P; ()) is satisfiable.

Theorem Second-order circumscription need not preserve satisfiability for universal theories if function constants are allowed to vary.

The situation is different if varying constants are restricted to predicate constants:

Theorem For any disjoint tuples P and S of predicate constants, every universal theory is well-founded with respect to (P; S).

Corollary For any disjoint tuples P and S of predicate constants and any satisfiable universal theory T, CIRC_{SO} (T; P; S) is satisfiable.

Expressive power of second-order circumscription

Theorem If T (P , S) is well-founded with respect to (P; S), P ∈ P is an n-ary predicate constant, S is a tuple of predicate constants disjoint with P, and α is an n-tuple of ground terms, then

CIRC_{SO} (T; P; S) ⊧ P (α) iff T ⊧ P (α).

Theorem If T (P , S) is well-founded with respect to (P; S), P and S are disjoint tuples of predicate constants, R is an n-ary predicate constant not in P , S, and α is an n-tuple of ground terms, then

(i) CIRC_{SO} (T; P; S) ⊧ R(α) iff T ⊧ R(α) (ii) CIRC_{SO} (T; P; S) ⊧ ¬R(α) iff T ⊧ ¬R(α).

Note: The only ground literals that may be obtained from well-founded theories by using second-order circumscription (without varying function constants) are negative instances of circumscribed predicates and instances, both positive and negative, of variable predicates.

This is not true if function constants are allowed to vary. In such a case, both positive literals of circumscribed predicates and new instances of non-variable predicates may be obtainable.

No new formulas can be obtained by circumscribing “=”:

Theorem For any T, S and A:

CIRC_{SO} (T; =; S) ⊧ A iff T ⊧ A.

The domain closure assumption, with respect to a theory T, is the assumption that the only individuals to be considered are those forced by the Herbrand universe of T. In the case where T gives rise to a finite Herbrand universe {c_{1}, …, c_{n}}, the domain closure assumption can be formalized by employing the domain closure axiom (Reiter):

∀x. x = c_{1} ∨ ⋯ ∨ x = c_{n}.

Second-order circumscription cannot be used, at least for well-founded theories and without varying functions, to obtain the domain closure axioms:

Theorem If T (P , S) is well-founded with respect to (P; S), S contains no function constants, and α_{1}, …, α_{n} are ground terms, then

CIRC_{SO} (T; P; S) ⊧ ∀x. x = α_{1} ∨ ⋯ ∨ x = α_{n}

iff T ⊧ ∀x. x = α_{1} ∨ ⋯ ∨ x = α_{n}.

Frequently, second-order circumscription axiom can be replaced by an equivalent first-order sentence. This allows to avoid second-order logic and makes the formalism very attractive for the purpose of practical applications (see Łukaszewicz: “Non-Monotonic Reasoning” pp. 249-252).