Domain Formula Circumscription

Tom Costello

Stanford University

Abstract.

Circumscription is a form of non-monotonic reasoning. The first version of circumscription, domain circumscription, is analogous to mathematical induction. Given a theory, it chooses the models of that theory whose domains are minimal with respect to inclusion. It captures the assumption that as few objects exist as possible.

Predicate and formula circumscription, introduced later, are characterized by a set of predicates or formulas to minimize. They choose the models that have as few objects true of the minimized predicates/formulas as possible. However, they do not compare models of different cardinality. Thus they are not an extension of domain circumscription, they are incomparable in expressive power.

We introduce a new form of circumscription that allows models that differ on domains to be compared. It extends both domain and formula circumscription, hence its name. It removes the artificial constraint that predicate and formula circumscription impose, and thus gives more intuitive semantics. Key words: non-monotonic reasoning, circumscription, logic, knowledge representation, equality, second order logic

1. Introduction

Circumscription was introduced by McCarthy(McC77) as a way of characterizing the defaults people and machines should use. The original form of circumscription described the default that we should assume there are as few objects as possible. McCarthy later introduced new forms of circumscription, predicate(McC80) and formula(McC86) circumscription, that characterized the default that a predicate/formula was false as often as possible. However, the later forms of circumscription did not extend the original form—rather they were incomparable. Later forms never changed the possible domains(Lif85) of the theory^{1}—if the theory had a model with domain U, then the circumscribed theory would have a model of domain U.

We introduce a more expressive form of circumscription that allows domains to be varied. We call this domain formula circumscription. It extends both domain circumscription, McCarthy’s first proposal, and predicate and formula circumscription, McCarthy’s later forms.

It is a more expressive form of circumscription than the union of both previous types. This can be seen in its circumscription policies. It allows formulas to be maximized as well as minimized. Maximizing a formula is not equivalent to minimizing another formula.

The expressive power that we have added allows models which were previously incomparable to be related. It differs from the attempts of pointwise circumscription in this way. Pointwise circumscription gives new ways to specify the preference on models, allowing more control over what is varied, but does not, for instance, allow models of differing cardinalities to be compared. Thus domain formula circumscription is more expressive that any form of pointwise circumscription in this regard.

A discussion of the expressive power of various forms of circumscription can be found in (Cos97), where it is show that in the finite propositional case formula circumscription can capture all preorders on valuations. This is not the case in for first order structures. Indeed, the second chapter of (Cos97) gives an example that can be captured in pointwise circumscription but not in formula circumscription, or for that matter domain formula circumscription. The proof that this order on structures can not be captured lifts easily to the case of domain formula circumscription.

1 This is only true if the the theory is smooth in the terminology of (KLM90). However, we gloss over this point, as we are only interested in this case.

This new form of circumscription also has nicer logical properties than the previous types of circumscription. It obeys a stronger form of the notion of conservative extension(see example 6). If one theory A is a conservative extension of a theory A_{1}, then the domain formula circumscription of A with respect to some policy C, in the language of A, is a conservative extension of the domain formula circumscription of A_{1} with respect to the same policy C.

This allows us to define the circumscription of non-finitely axiomatizable theories, such as Zermelo-Frankel set theory, real closed fields, and first order Peano arithmetic.

Perhaps the most important property of this new form of circumscription, is that it allows us to express natural defaults that were not previously expressible. Later, we give examples(see examples 1,3,4) of new defaults, that can be simply captured by the new theory, but cannot be captured by previous forms of circumscription.

This paper does not address the issue of making circumscription map satisfiable theories to satisfiable theories. Indeed, as this form of circumscription can model predicate circumscription, it sometimes maps satisfiable theories to unsatisfiable theories, e.g. Example 3.1 of (EMR85). Modifications to circumscription to avoid this issue are discussed in (Cos97).

2. Domain Formula Circumscription

We define a domain formula circumscription policy by a set of formulas, Γ, to minimize, and a set of formulas, Δ, to maximize. We now look at descriptions of domain formula circumscription in model-theoretic and syntactic terms. We then prove these two forms equivalent.

2.1. Semantics

We say two models 𝔄 and 𝔅 are in the relation ≤_{Γ;Δ} if the extension of each minimized formulas in 𝔄 is a subset of the extension of that formula in 𝔅, and the extension of each maximized formulas in 𝔄 is a superset of the extension of that formula in 𝔅. In model theoretic terms, the consequences of domain formula circumscription are the sentences true in all minimal models under this pre-order ≤_{Γ;Δ}.

In order to define precisely the semantics of this form of circumscription, we need to introduce some notation.

DEFINITION 1 (≤_{Γ;Δ} ). Given a first order language L, we define the relation ≤_{Γ,Δ} over the structures of that language as follows, where Γ and Δ are finite sets of formulas from L. We denote the extension of a formula γ in an L-structure 𝔄 as 𝔄[γ]. For any two L-structures 𝔄, 𝔅, we write 𝔄 ≤_{Γ;Δ} 𝔅 if,

1. 𝔄[γ] ⫅ 𝔅[γ] for every γ in Γ.

2. 𝔄[γ] ⫆ 𝔅[γ] for every γ in Δ.

We now look at some of the properties of ≤_{Γ;Δ}. It is a pre-order on the class of all structures over a given language. It is not in general a partial order, as there are distinct structures that are ≤_{Γ;Δ} than each other.

PROPOSITION 1. ≤_{Γ;Δ} is a pre-order.

Proof. This follow immediately from the transitivity and reflexivity of ⫅ and ⫆.

The consequences of the domain formula circumscription of a sentence α, minimizing Γ, maximizing Δ, are the sentences true in the minimal models of α under the pre-order ≤_{Γ;Δ}.

We now note that if a structure 𝔅 is not minimal, the there exists a structure 𝔄 less than it, whose domain is not larger than |∥𝔅∥ ∪ X|, where X is some set with cardinality ℵ_{0}.

Let ∥𝔄∥, ∥𝔅∥, ∥ℭ∥ denote the domains of the structures 𝔄, 𝔅, ℭ. Let |𝔄| denote the cardinality of ∥𝔄∥. Let ∥𝔄∥^{n} denote the set of n-tuples of elements of ∥𝔄∥.

LEMMA 1. Let L be a countable first order language, Γ, Δ be two finite sets of formulas in L, and let 𝔅 be an L-structure.

If the L-structure 𝔅 is not a minimal structure with respect to ≤_{Γ;Δ}, then there exists some L-structure 𝔄, with |𝔄| ≤ max(|𝔅|, ℵ_{0}) such that 𝔄 ≤_{Γ;Δ} 𝔅, and 𝔅 ≰_{Γ;Δ} 𝔄.

Proof. Suppose that an L-structure ℭ is ≤_{Γ;Δ} than 𝔅, and 𝔅 is not ≤_{Γ;Δ} than ℭ.

By assumption we are told that 𝔅 is not ≤_{Γ;Δ} than ℭ. Therefore, either there exists a n-tuple \overline{a}, and a γ ∈ Γ such that \overline{a} ∉ ℭ[γ] and \overline{a} ∈ 𝔅[γ], or there exists a n-tuple \overline{a}, and a δ ∈ Δ such that \overline{a} ∈ ℭ[δ] and \overline{a} ∉ 𝔅[δ]. If only the first disjunct holds, then we choose Y to be empty. In the second case there is a tuple \overline{a} such that \overline{a} ∈ ℭ[δ] and \overline{a} ∉ 𝔅[δ]. We choose Y to be the set of objects in this tuple.

Take an elementary sub-model of ℭ, whose domain contains (∥𝔅∥ ∩ ∥ℭ∥) ∪ Y where Y is the set from C chosen above, and whose domain is included in (∥𝔅∥∩∥ℭ∥)∪X, where X is a countable set. This exists, as every substructure of a first order model of a countable language can be extended to an elementarily embedding by adding a countable number of objects(CK90) proposition 2.2.17.

The restriction of ℭ to the domain (∥𝔅∥∩∥ℭ∥)∪Y is a sub-model of ℭ, as long as (∥𝔅∥∩∥ℭ∥)∪Y is non-empty. If (∥𝔅∥ ∩ ∥ℭ∥) is empty, then as ℭ is ≤_{Γ;Δ} than 𝔅, either no formula in Γ or Δ can contain a free variable, as for the extensions of formulas with free variables to be in a subset relationship, their models must contain some shared elements, or all the formulas in Δ and Γ are false in both models, contradicting the inequality. Thus all the formulas in Γ, Δ are sentences, and thus we can choose 𝔄 to be an arbitrary elementarily equivalent model to ℭ, with domain max(|𝔅|, ℵ_{0}), which exists by the Lowenheim Skolem theorem, as the language is countable by assumption. Thus, without loss of generality, we can take (∥𝔅∥ ∩ ∥ℭ∥) ∪ Y to be non-empty.

Every sub-model of ℭ can be extended to an elementary sub-model of ℭ by adding a countable number of new objects, as our language is countable.

This is the desired model 𝔄, as it is has only a countable number of elements not in ∥𝔅∥ in its domain, and it is ≤_{Γ;Δ} than 𝔅, and 𝔅 ≰_{Γ;Δ} 𝔄 by the following.

We first show that 𝔄 ≤_{Γ;Δ} 𝔅. To show this we need to show that for all γ ∈ Γ 𝔄[γ] ⫅ 𝔅[γ]. We know that ℭ[γ] ⫅ 𝔅[γ], and thus ℭ[γ] ⫅ (∥𝔅∥ ∩ ∥ℭ∥)^{n}, where n is the number of free variables in γ. But 𝔄 and ℭ agree on all elements in (∥𝔅∥ ∩ ∥ℭ∥), so 𝔄[γ] = ℭ[γ], and thus 𝔄[γ] ⫅ 𝔅[γ]. Secondly we need to show that for all δ ∈ Δ 𝔅[δ] ⫅ 𝔄[δ]. We know that 𝔅[δ] ⫅ ℭ[δ], and thus 𝔅[δ] ⫅ (∥𝔅∥ ∩ ∥ℭ∥)^{n} where n is the number of free variables in δ. But 𝔄 and ℭ agree on all elements in (∥𝔅∥ ∩ ∥ℭ∥), so 𝔅[δ] ⫅ 𝔄[δ].

We now show that 𝔅 ≰_{Γ;Δ} 𝔄. By assumption we are told that 𝔅 is not ≤_{Γ;Δ} than ℭ. Therefore, either there exists a n-tuple \overline{a}, and a γ ∈ Γ such that \overline{a} ∉ ℭ[γ] and \overline{a} ∈ 𝔅[γ], or there exists a n-tuple \overline{a}, and a δ ∈ Δ such that \overline{a} ∈ ℭ[δ] and \overline{a} ∉ 𝔅[δ]. From either possibility we show that 𝔅 ≰_{Γ;Δ} 𝔄.

First we assume that there exists a n-tuple \overline{a}, and a γ ∈ Γ such that \overline{a} ∉ ℭ[γ] and \overline{a} ∈ 𝔅[γ]. 𝔄[γ] ⫅ ℭ[γ], as 𝔄 is an elementary sub-model. However, ℭ[γ] ⫋ 𝔅[γ], by our assumption. Thus, 𝔄[γ] ⫋ 𝔅[γ]. This implies that 𝔅 ≰_{Γ;Δ} 𝔄 as required.

Now we assume that there exists a n-tuple \overline{a}, and a δ ∈ Δ such that \overline{a} ∈ ℭ[δ] and \overline{a} ∉ 𝔅[δ]. As 𝔅[δ] ⫋ ℭ[δ], thus 𝔅[δ] ⫋ ℭ[δ] ∩ ((∥𝔅∥ ∩ ∥ℭ∥) ∪ Y)^{n}, where n is the number of free variables of δ. We first prove the inclusion and then the inequality. The elements that satisfy 𝔅[δ] must be in both ∥ℭ∥ and ∥𝔅∥, as they are in ∥𝔅∥ by definition, and in ∥ℭ∥ by the subset assertion. Thus 𝔅[δ] ⫅ ℭ[δ] ∩ ((∥𝔅∥ ∩ ∥ℭ∥) ∪ Y)^{n}.

We are given 𝔅[δ] ⫋ ℭ[δ], and a tuple \overline{a} such that \overline{a} ∈ ℭ[δ] and \overline{a} ∉ 𝔅[δ]. We need to ensure that this tuple \overline{a} is in our model ℭ[δ] ∩ ((∥𝔅∥ ∩ ∥ℭ∥) ∪ Y)^{n}, for some δ. However, we choose Y to be exactly the necessary set that witnesses the inequality.

Thus 𝔅[δ] ⫋ 𝔄[δ], as 𝔄 contains all the elements in ((∥𝔅∥ ∩ ∥ℭ∥) ∪ Y)^{n}. Thus, 𝔅 ≰_{Γ;Δ} 𝔄 as required.

The author is grateful to Johan van Benthem for suggesting this key lemma. This lemma is not immediately obvious from Lowenheim Skolem, as the pre-order is defined in terms of subset inclusion on the extensions of formulas, and thus is not a congruence on elementarily equivalent structures.

2.2. Syntactic Form

We now need to introduce a condition analogous to the Closed_{L} condition(see page ??) we saw earlier. We will need to say that a set of unary predicates variables ϕ_{i} act correctly as domains for the sorts of L. They must contain the correct constants, and be closed under functions.

DEFINITION 2 ( CL_{L}^{\{ϕ_{1},...,ϕ_{o}\}}(\{ζ_{1}, …, ζ_{n}\}, \{x_{1}, … x_{m}\})). When L is a first order language ⟨\overline{P} , f_{1}, … f_{n}, C⟩, with o sorts, S_{1}, …, S_{o}, then CL_{L}^{{ϕ_{1},...,ϕ_{o}}}({ζ_{1}, …, ζ_{n}}, {x_{1}, … x_{m}}) is the conjunction of the sentences that state that, for each function variable ζ_{i}, it obeys the same sorting rules with respect to {ϕ_{1}, …, ϕ_{o}} as the corresponding function f_{i} does with respect to the sorts, and that each individual variable x is in the predicate variable ϕ_{i} corresponding to its sort S_{i}.

If the only function in a language L, with three sorts, is a binary function f, which takes an argument of sort S_{1}, and an argument of sort S_{2}, and returns and argument of S_{3}, then CL^{{ϕ_{1},ϕ_{2},ϕ_{3}}}(ζ), is the sentence,

∀x, y.ϕ_{1}(x) ∧ ϕ_{2}(y) → ϕ_{3}(ζ(x, y)).

We add that there are a countable number of objects not in any of these predicates—these are the objects that we will be free to use to create alternate models. We later show that a countable number of extra objects suffices for first order consequences.

DEFINITION 3 (inf(L)). Let L be a first order language. We define inf(L) to be the sentence in second order logic, that states that there are a countably infinite number of objects not in any of these sorts.

If the sorts of L are S_{1}, S_{2}, then this is the second order sentence,

∃ζ, x. \begin{matrix}∀y.ζ(y) ≠ x ∧ ∀y, z.ζ(y) = ζ(z) → y = z \\ ∧¬(S_{1}(x) ∨ S_{2}(x))∧ \\ ∀y.¬(S_{1}(y) ∨ S_{2}(y)) → ¬(S_{1}(ζ(y)) ∨ S_{2}(ζ(y))) \end{matrix}

Second order logic has models of every cardinality. This did not cause a problem for domain circumscription, as the smallest model was the model that was sought, and every model of the theory therefore contained enough elements to model a domain for this model. This is not the case for larger models. There will be times that there are simply not enough elements in the universe to make a domain of a particular size. To overcome this we postulate enough elements to make domains. As we are interested in the first order consequences it is sufficient to postulate a countable number of extra objects. We need these objects to be distinct from the sorts we already have so that we are free to use them in any way we choose.

If a theory A over a language L is finitely axiomatizable then we can express the consequences of domain formula circumscription as a second order sentence in a sorted language.

The idea behind the next definition is as follows. We start with a second order language, which extends the sorts of our first order language by a new sort, a super-sort of all the sorts in our first order language. We take a theory in a sorted language, and we replace every symbol by a variable of the appropriate type, whose sorts are from the new sort we have introduced. We then relativize the theory, with new unary predicate variables, one for each sort in our first order language, again each of these is over our new sort. We restrict the new unary predicate variables, so that they must behave as a valid domain, that is they must be non-empty and closed under function application.

Once we have these conditions, we note that tuples of predicate, function and constant variables, plus a set of unary predicate variables, acting for sorts, exactly characterize a model. We can then write the conditions that the extension of a formula in one model is a subset/superset of the extension of that formula in another model. This allows us to write that the models of the predicate function and constant symbols are the minimal models in the usual way.

This may seem quite complicated, as it seems to involve quite a lot of tinkering with formulas. However it involves no more complications than those in formula and domain circumscription. We already had the ideas of relativization in domain circumscription, and the notion of restricting a unary predicate variable so that it would act as a valid domain. What we have added is a formal treatment for the sorted case of circumscription, something that is usually glossed over.

DEFINITION 4 (Domain Formula Circumscription). If γ_{1}, γ_{2} are a pair of formulas in a first order language L to minimize, and δ_{1}, δ_{2} are a pair of formulas in L to maximize, and S_{1}, S_{2} are the sorts in L, and P, F, c is the sequence of the predicate, function and constant symbols in L, then we define the domain formula circumscription of a finitely axiomatized theory, viewed as a sentence α in L, minimizing γ_{1}, γ_{2}, maximizing δ_{1}, δ_{2} written Circ_{D}(α; γ_{1}, γ_{2}; δ_{1}, δ_{2}) as the following sentence, in sorted second order logic, with sorts S_{1}, S_{2}, and a new super-sort of all those sorts.

We write α′ as a shorthand for α^{ϕ_{1},ϕ_{2}}[ψ/P, ζ/f, x/c], that is, relativizing α with respect to new unary predicates ϕ_{1} and ϕ_{2}, and replacing the predicates, functions and constants, with predicate, function and constant variables.

\begin{matrix}α ∧ inf(L)∧ \\ ∀ϕ_{1}, ϕ_{2}, ψ, ζ, x.¬ [α′ ∧ CL_{L}^{ϕ_{1},ϕ_{2}}(\{ζ\}) ∧ γ′_{1}, γ′_{2}, δ_{1}, δ_{2} < γ_{1}, γ_{2}, δ′_{1}, δ′_{2}] \end{matrix}

where ψ, ζ are predicate and function variables respectively agreeing in arity with P and f, while x is an individual variable.

At this point it is worth noting that the methods for reducing second order sentences to equivalent first order sentences are sometimes applicable to this form of circumscription. These methods, (DLS96) and (GO92) are general methods that apply to any second order sentence, sometimes constructing an equivalent first order formula. In many simple examples these methods succeed when applied to domain formula circumscriptions. We use the DLS algorithm of (DLS96) below to compute an equivalent for our first example. We later show that there are domain formula circumscription policies that are equivalent to formula circumscription and domain circumscription. It follows that in these cases the algorithms that find a first order equivalent for formula circumscription and domain circumscription also apply to these cases of domain formula circumscription.

EXAMPLE 1. We consider a language L with one predicate P, and one sort S. We have two constants, B and C of sort S.

Given the sentence α:

P (B) ∧ P (C)

we note that Circ_{D}(α; S(x); ) gives

P (B) ∧ P (C) ∧ inf(L)∧
∀P′, b, c, ϕ.[P′(b) ∧ P′(b) ∧ ϕ(b) ∧ ϕ(c)∧
∀y.ϕ(y) → S(y)] → ∀y.S(y) → ϕ(y).

If we instantiate y = B ∨ y = C for ϕ, B for b, C for c and λx.x = B ∨ x = C for P′, we get

∀y.S(y) ≡ (y = B ∨ y = C)

In fact

\begin{matrix}P (B) ∧ P (C) ∧ inf(L)∧ \\ ∀y.(y ≠ B ∧ y ≠ C) → ¬S(y) \end{matrix}

is logically equivalent to Circ_{D}(α; S(x); ), as may be shown by applying the DLS algorithm (DLS96) to the second order formula.

The DLS algorithm is easiest to explain in an unsorted logic, thus we explicitly add the sort S and state that it is true of B and C.

P (B) ∧ P (C) ∧ S(B) ∧ S(C) ∧ inf(L)∧
∀P′, b, c, ϕ.[P′(b) ∧ P′(c) ∧ ϕ(b) ∧ ϕ(c)∧
∀y.ϕ(y) → S(y)] → ∀y.S(y) → ϕ(y).

We are only interested in the second order part, namely

∀P′, b, c, ϕ.[P′(b) ∧ P′(c) ∧ ϕ(b) ∧ ϕ(c)∧
∀y.ϕ(y) → S(y)] → ∀y.S(y) → ϕ(y).

We consider its negation.

∃P′, b, c, ϕ.[P′(b) ∧ P′(c) ∧ ϕ(b) ∧ ϕ(c)∧
∀y.ϕ(y) → S(y)] ∧ ∃y.¬ϕ(y) ∧ S(y)].

We put the matrix into disjunctive normal form.

∃P′, b, c, ϕ.P′(b) ∧ P′(c) ∧ ϕ(b) ∧ ϕ(c)∧
∀y.¬ϕ(y) ∨ S(y) ∧ ∃y.¬ϕ(y) ∧ S(y).

We push the second order quantifiers in as far as possible.

∃b, c.(∃P′.P′(b) ∧ P′(c)) ∧ (∃ϕ.ϕ(b) ∧ ϕ(c)∧
∀y.¬ϕ(y) ∨ S(y) ∧ ∃y.¬ϕ(y) ∧ S(y)).

The first conjunct is immediately True as P′ occurs only positively. We thus simplify to

∃b, c.(∃ϕ.ϕ(b) ∧ ϕ(c)∧
∀y.¬ϕ(y) ∨ S(y) ∧ ∃y.¬ϕ(y) ∧ ¬S(y)).

We separate the positive occurrences from the negative occurrences.

∃b, c.∃ϕ.ϕ(b) ∧ ϕ(c)∧

∀y.¬ϕ(y) ∨ S(y) ∧ ∃y.¬ϕ(y) ∧ S(y).

We collect the b and c to get,

∃b, c.∃ϕ.(∀x.x ≠ b ∧ x ≠ c ∨ ϕ(x))∧
∧∃y.¬ϕ(y) ∧ S(y) ∧ ∀y.¬ϕ(y) ∨ S(y).

We apply the first form of Ackerman’s Lemma,

∃Φ∀x̄[Φ(x̄) ∨ A(x̄, z̄)] ∧ B(Φ ← ¬Φ) ≡ B(Φ ← A(x̄, z̄))

getting,

(∀y.y ≠ b ∧ y ≠ c ∨ S(y)) ∧ ∃b, c.(∃y.y ≠ b ∧ y ≠ c ∧ S(y)).

This is equivalent to,

∃b, c, y.y ≠ b ∧ y ≠ c ∧ S(y) ∧ S(a) ∧ S(b).

We negate this to get our answer,

∀b, c, y.(y ≠ b ∧ y ≠ c → ¬S(y)) ∨ ¬S(a) ∨ ¬S(b).

However, S(B) and S(C) imply the above formula is equivalent to

∀y.y ≠ C ∧ y ≠ B → ¬S(y).

The forward direction can be seen by deriving the above formula by instantiation B and C for a and b, and the backwards direction by replacing S by λx.x = B ∨ x = C in the result of our quantifier elimination.

Therefore the circumscription formula is equivalent to

P (A) ∧ P (B) ∧ S(B) ∧ S(C) ∧ inf(L) ∧ ∀y.y ≠ C ∧ y ≠ B → ¬S(y).

We now give an example where we vary the domain.

EXAMPLE 2 (Witnesses). Tom, Dick, and Harry are members of a criminal organization. We have a default that witnesses are normally present at crimes. We have two sorts, locations and people. We have a predicate, At(p, l), that means the person p is at the location l and a predicate Crimeloc(l), that states that l is the location of a criminal act. We also have a predicate F elon(p), that is true of any member of a proscribed organization.

We know that:

F elon(T om) ∧ F elon(Harry) ∧ F elon(Dick) ∧ ∀p∃l.At(p, l)

We call this theory Crime. It states that Tom, Dick and Harry are felons, and that everyone is at some location.

We now try to capture the default that crimes are usually witnessed by some non-criminal. We do this by minimizing

∀p.Crimeloc(l) → ¬At(p, l) ∨ F elon(p),

while we fix the predicate Crimeloc. This states that usually non-felons are present at crimes, or that it unlikely that there is a location where a crime happened, where all the people present were felons. We fix Crimeloc, that is we both minimize and maximize Crimeloc , as otherwise we allow the possibility that there is no crime. This notion of fixing predicates that are not to be changed in the minimization process was introduced by McCarthy (McC86).

The intended solution is that, as there is no evidence to the contrary, we assume that there is a witness at each location. When we minimize in domain formula circumscription, we get this result.

To infer that there is a witness at each location there must be at least as many non-felons as there are locations. However, the original theory has models where there are many locations but no non-felons. As circumscription does not compare models that have different domains, there are minimal models which have many locations but no non-felons. Thus in these models there are crimes that are not witnessed.

Thus, if we circumscribe normally, using formula circumscription, we do not get witnesses at each crime location. If we circumscribe using domain formula circumscription we find that every crime is witnessed.

We now show this more formally.

Circ_{D}(Crime; ∀p.Crimeloc(l) → ¬At(p, l) ∨ F elon(p), Crimeloc(l);
Crimeloc(l)) ⊧ (∀l.Crimeloc(l) → ∃p.At(p, l) ∧ ¬F elon(p))

We can find an equivalent first order theory to

Circ_{D} ( \begin{matrix}Crime; \\ ∀p.Crimeloc(l) → ¬At(p, l) ∨ F elon(p), Crimeloc(l); \\ Crimeloc(l) \end{matrix} )

by using the DLS algorithm. In this case we find that

\begin{matrix}F elon(T om) ∧ F elon(Harry) ∧ F elon(Dick) ∧ ∀p∃l.At(p, l) \\ ∀l.Crimeloc(l) → ∃p.At(p, l) ∧ ¬F elon(p) \end{matrix}

is equivalent to the above circumscription, where p and l are variables of type person and location respectively.

This is not the case for formula circumscription,

Circ_{F} (Crime; ∀p.Crimeloc(l) → ¬At(p, l) ∨ F elon(p), Crimeloc(l),
¬Crimeloc(l)) |̸= (∀l.Crimeloc(l) → ∃p.At(p, l) ∧ ¬F elon(p)).

This can be seen as the model where there is one location, that is the location of a crime, and only three people, Tom, Dick and Harry, is minimal, and does not satisfy (∀l.Crimeloc(l) → ∃p.At(p, l) ∧ ¬F elon(p)).

2.3. Why Maximizing

It might seem strange that we have introduced the idea of maximizing, when this is usually achieved in normal circumscription by minimizing the negation of that which is to be maximized. However, we show that in domain formula circumscription the two notions do not co-incide.

A way of explaining this is to realize that minimizing the negation maximized the original predicate because the domain was fixed, and thus anything removed from one, was forced into the other. Now that we can vary the domain this no longer applies.

EXAMPLE 3. Let the sentence α be,

(∀x.x = Opus ∨ x = T weety ∨ x = Joe) ∧ P enguin(Opus).

We now minimize P enguin,

Circ_{D}(α; P enguin; ) ≡ \begin{matrix}(∀x.P enguin(x) ≡ x = Opus)∧ \\ ∀x.x = Opus ∨ x = T weety ∨ x = Joe \end{matrix}

We then maximize ¬P enguin,

Circ_{D}(α; ; ¬P enguin) ≡
Joe ≠ T weety∧
(∀x.¬P enguin(x) ≡ x = T weety ∨ x = Joe)∧
∀x.x = Opus ∨ x = T weety ∨ x = Joe

We do not get the same results.

PROPOSITION 2. Maximizing a formula in domain formula circumscription is not the same as minimizing its negation.

Proof. Immediate from example 3 above, as

Circ_{D}(α; P; ) ≢ Circ_{C}(α; ; ¬P).

THEOREM 1. If α is a finitely axiomatizable first order theory in a first order language L, viewed as a sentence, and Γ and Δ are finite sequences of formulas from L, and γ is a sentence from L, then if Circ_{D}(α; Γ; Δ) ⊧ γ then γ is true in all minimal models of α under ≤_{Γ,Δ}.

Proof.

We assume that Circ_{D}(α; Γ; Δ) ⊧ γ and show that it is true in all minimal models.

Assume it was not true. Then there would be a minimal model 𝔄 such that 𝔄 ⊧ ¬γ. We now consider the interpretation of all predicates, constants and functions in this model. We from Lemma 1 can choose the domain to be a set U, a subset of the union of the infinite set we postulated in inf and the domain of 𝔄. We then instantiate the quantifiers in our circumscription with this set, and the derived sets of tuples, functions and constants.

We claim these instantiations satisfy the first condition, minimality. If they did not, then from a tuple smaller than it we could construct a model smaller than 𝔄 contradicting our assumption.

Thus we can derive the left-hand side of that condition, establishing that if this tuple satisfies α then the predicates of our theory are exactly those in 𝔄. As 𝔄 is a model, we satisfy the first part. Thus one model of the circumscription satisfies ¬γ. Therefore the circumscription does not entail γ, as needed to establish a contradiction.

THEOREM 2. If α is a finitely axiomatizable first order theory in a language L, viewed as a sentence, and Γ, Δ are finite sequences of formulas in L, and γ is a sentence in L, then if γ is true in all minimal models of α under ≤_{Γ,Δ} then Circ_{D}(α; Γ; Δ) ⊧ γ.

Proof.

We assume the opposite and show a contradiction.

Circ_{D}(α; Γ; Δ) |̸= γ, then |̸= Circ_{D}(α; Γ; Δ) → γ. We construct a model that denies this. Call it 𝔄. In it γ is false and Circ_{D}(α; Γ; Δ) is true. Thus every assignment of predicates, functions and constants that satisfies α, over subsets U of the universe of this model, correspond to models that are not preferred to 𝔄. Thus 𝔄 is minimal, contradicting our assumption that all minimal models satisfy γ.

We now show that our new version of circumscription can capture the two earlier forms of circumscription, domain and predicate.

PROPOSITION 3. If α is a finitely axiomatizable first order theory in a language L, viewed as a sentence, and γ_{1}, …, γ_{n} is a finite sequence of formulas in L, then there exists two finite sets of formulas in L, Γ, Δ such that for all γ ∈ L,

Circ_{D}(α; Γ; Δ) ⊧ γ if and only if Circ(α; γ_{1}, …, γ_{n}) ⊧ γ

Proof. We maximize and minimize x = x for every sort, and minimize γ_{1}, …, γ_{n}. This gives an equivalent formula of second order logic modulo relativization.

We show that it can also capture the domain circumscription of McCarthy(McC77).

PROPOSITION 4. Fixing a formula γ is achieved by minimizing and maximizing γ.

Proof. All models that are comparable will now agree on γ. Note that we minimize and maximize γ rather than minimize γ and ¬γ.

Fixing a function or constant f or c is achieved by minimizing and maximizing the equation, f(\overline{y}) = x , c = x respectively.

PROPOSITION 5. If α is a finitely axiomatizable first order theory in a language L, viewed as a sentence, then there exists two finite sets of formulas in L, Γ, Δ, such that,

DomCirc(α) ⊧ γ if and only if Circ_{D}(α; Γ; Δ) ⊧ γ

Proof. We minimize x = x, and fix (maximize and minimize) every predicate, function, and constant symbol. This is an equivalent sentence of second order logic.

3. Equality of Closed Terms

Previous versions of circumscription have difficulty dealing with the equality of closed terms. In this section we look at how our new version of circumscription overcomes these problems. We then look at how this relates to the other approaches to minimizing equality.

3.1. The Unique Names Assumption

Reiter is credited with introducing the terminology, Unique names assumption, for the default that distinct ground terms have different denotations, if possible. We capture this in our form of circumscription by minimizing the sentences that express the equality of these terms, or alternatively maximizing the sentences that state these terms are distinct.

EXAMPLE 4. Let L be the language with the unary predicate Bird and two constants Joe and T weety. Let α be the following sentence in L:

Bird(T weety) ∧ Bird(Opus) ∧ ¬Bird(Joe),

then

Circ_{D}(α; T weety = Joe, T weety = Opus, Opus = Joe; ) ≡
Circ_{D}(α; ; T weety ≠ Joe, T weety ≠ Opus, Opus ≠ Joe) ≡
Bird(T weety) ∧ Bird(Opus) ∧ ¬Bird(Joe)∧
T weety ≠ Joe ∧ T weety ≠ Opus ∧ Opus ≠ Joe

Note that this is non-monotonic, in the sense that if T weety = Opus is conjoined to α to give α_{1} then,

Circ_{D}(α_{1}; T weety = Joe, T weety = Opus, Opus = Joe; ) ≡
Circ_{D}(α_{1}; ; T weety ≠ Joe, T weety ≠ Opus, Opus ≠ Joe) ≡
Bird(T weety) ∧ Bird(Opus) ∧ ¬Bird(Joe)∧
T weety ≠ Joe ∧ T weety = Opus

Having seen this, one might ask why this was ever considered a problem. For this reason we re-capitulate some of the difficulties that arose in other approaches.

3.2. Etherington, Mercer and Reiter

Etherington et al.(EMR85) argue that McCarthy’s circumscription cannot deal with the unique names assumption.

Another limitation relates to equality; predicate circumscription yields no new information about the equality predicate for a large class of first-order theories. … Recently McCarthy has proposed a generalization of predicate circumscription, which minimizes arbitrary first-order expressions rather than simple predicates. … Some of the limitations of predicate circumscription that we describe in this paper do not apply to his generalized form of circumscription, but equality appears to remain problematic.

They prove the following theorem.

THEOREM 3 (Etherington et al., 1984). Let α be a first order sentence containing, as a conjunct, the axioms for equality. Then

Circ(α; =) ⊧ α.

THEOREM 4 (Etherington et al., 1984). Suppose that α is a smooth sentence containing, as a conjunct, axioms that define the equality predicate, t_{1} and t_{2} are ground terms, and \overline{P} is some set of predicates of the language of L. Then

Circ(α; \overline{P}) ⊧ t_{1} = t_{2} if and only if α ⊧ t_{1} = t_{2}
Circ(α; \overline{P}) ⊧ t_{1} ≠ t_{2} if and only if α ⊧ t_{1} ≠ t_{2}

These theorems are proved by noticing that models are only compared if they agree on the denotation of t_{1} and t_{2}, and thus, if there are minimal models, then t_{1} and t_{2} will be distinct if and only if they were distinct in all models, and equal if and only if they were equal in all models.

3.3. McCarthy’s Suggestion

We look at McCarthy’s suggestion(McC86), which uses models where we assume that all distinct closed terms are distinct, and where we introduce a new predicate to represent classical equality.

McCarthy adds a new sort, which is to be interpreted as the concepts for each ground term. These concepts are distinct, thus we state unique names axioms for all these concepts we add. He then introduces a predicate e(x, y), which attempts to capture the notion that the concepts x and y have equal denotations.

DEFINITION 5 ( Equality Theory). Given a first order language L = ⟨{P_{1}^{b(1)}, …, P_{n}^{b(n)}}, {f_{1}^{a(1)}, …, f_{m}^{a(m)}}, {c_{1}, …, c_{o}}⟩, where the P ’s are predicates, and the f’s functions and the superscripts denote arity, and a sentence α, the Equality Theory is the circumscription of the following theory, minimizing e:

⋀_{i=1,i<j}^{n} c_{i} ≠ c_{j},

⋀_{i=1,k=a(i)}^{m} ∀x_{1}, … x_{k}, y_{1}, …, y_{k}. \begin{matrix}f_{i}(x_{1}, …, x_{k}) = f_{j}(y_{1}, …, y_{k}) → \\ x_{1} = y_{1} ∧ … ∧ x_{k} = y_{k}, \end{matrix}

⋀_{i=1,i<j} ∀x_{1}, …, x_{a(i)}, y_{1}, …, y_{a(j)}.f_{i}(x_{1}, …, x_{a(i)}) ≠ f_{j}(y_{1}, …, y_{a(j)}) α[e/ =], ∀x.e(x, x), ∀x, y.e(x, y) → e(y, x), ∀x, y, z.e(x, y) ∧ e(y, z) → e(x, z), ⋀_{i=1}^{m} ∀x_{1}, …, x_{k}, y_{1}, …, y_{k}. ⋀_{j=1}^{k} e(x_{j}, y_{j}) →

f_{i}(x_{1}, …, x_{k}) = f_{i}(y_{1}, …, y_{k}),

⋀_{i=1,k=b(i)}^{n} ∀x_{1}, …, x_{k}, y_{1}, …, y_{k}. \begin{matrix}⋀_{j=1}^{k} e(x_{j}, y_{j}) → \\ P_{i}(x_{1}, …, x_{k}) ≡ P_{i}(y_{1}, …, y_{k}) \end{matrix}

The first three lines encode a Herbrand universe assumption, that every distinct term denotes a distinct object. The fourth line α[e/ =], is where every sub-formula in α that mentions equality is recast in terms of e. Finally we add that e is an equivalence relation, and objects in this equivalence relations behave similarly in predicates and functions.

This gives a theory where e behaves like equality, and can successfully be minimized.

This approach has been criticized on the grounds that it does not ensure that all things that exist are denoted by concepts. Because of this existentials can cause problems. This method does not state that the result of a function f applied to an object o that is not denoted by a concept is distinct from the object o. Whether this is desirable is questionable.

3.4. Lifschitz

Lifschitz(Lif84) describes a different approach using true equality rather than a new predicate e. His method has been substantially extended by Arima(Ari88). They both introduce a new sort, that act as concepts. They vary function and constant symbols, while minimizing the amount of concepts that denote the same term.

The major problems with this approach are the ugliness of introducing Gödel numbers for terms, and the fact that varying functions in standard circumscription can make satisfiable theories unsatisfiable. The Gödel number of this approach function much like the extra countable numbers of objects added in our new version. We do not need to bind these new objects to particular terms, as we vary all constants and functions.

4. Non-finitely Axiomatizable Theories

We now define the circumscription of a non-finitely axiomatizable theory. We do this by considering a finitely axiomatizable conservative extension of the theory. The consequences of the circumscription of this extended theory that are in our original language are our consequences. We show that, for domain formula circumscription, it does not matter how we choose our finitely axiomatizable extension. We show this is not the case for standard circumscription.

We first recall the result by Kleene(Kle52), that says if a theory A is recursively enumerable (r.e.) axiomatizable in first order predicate calculus with equality and its language has only finitely many basic symbols, and if A has only infinite models then it is has a conservative extension by means of a finitely axiomatized theory. There are two generalizations where one drops the restriction to infinite models only, one due to Craig and Vaught(CV58) and one due to Feferman(Fef74).

DEFINITION 6 (conservative extension). A theory A in a first order language L, is a conservative extension of a theory A_{1} in a first order language L_{1} exactly when L ⫆ L_{1} and A ∩ L_{1} = A_{1}. We say a sentence α is a conservative extension of a theory A, when the theory of α is a conservative extension of A.

DEFINITION 7 (re-circ). Let A_{1} be a theory in a first order language L_{1}, and let Γ, Δ, be finite sets of formulas in L_{1}, and α a sentence in L an extension of L_{1}, then, the consequences of the re-circ of A_{1}, minimizing Γ, maximizing Δ, written Circ_{re}(A_{1}; Γ; Δ), are the consequences of Circ_{D}(α, Γ; Δ) that are in the language L_{1}, where α is a conservative extension of A_{1}.

THEOREM 5. If α is a finitely axiomatizable theory in a language L_{1}, viewed as a sentence, and α is a conservative extension of a theory A_{1} in a language L′, then,

Circ_{re}(A_{1}; Γ; Δ) ≡ Circ_{D}(α; Γ; Δ).

Proof. We note that for any conservative extensionα′ of A_{1}, in a language L′′, models of α′, are ordered by ≤_{Γ;Δ}^{L′′} exactly when their reducts to L′ are ordered by ≤_{Γ;Δ}^{L′}. Thus the two systems agree on minimality over the formulas in L′.

Thus for domain formula circumscription, it does not matter how we choose our finitely axiomatizable extension.

THEOREM 6. There are finitely axiomatizable theories, viewed as sentences, α_{1}, in a language L_{1}, with conservative extensions α in L, such that Circ(α; Γ) and Circ(α_{1}, Γ) do not agree on the sentences in L_{1}.

Proof. Consider the language with one unary predicate P, and two constants B and C, let α_{1} be T rue. Let L be the two sorted language with the same constants, where P has sort S_{1}, B and C are of sort S_{1}, and there is another sort, S_{2}. We have variables v_{i} ranging over the sort S_{2}. Let α be the sentence (∃v_{1}, v_{2}.v_{1} ≠ v_{2}) ≡ P (B). Then,

Circ(α_{1} : P) ≡ Circ(T rue; P) ≡ ∀x.¬P (x),

while,

Circ(α; P) \begin{matrix}≡ Circ(∃v_{1}, v_{2}.v_{1} ≠ v_{2} ≡ P (B); P) \\ ≡ ((∀x.P (x) ≡ x = B) ∧ (∃v_{1}, v_{2}.v_{1} ≠ v_{2}))∨ \\ ((∀v_{1}, v_{2}.v_{1} = v_{2}) ∧ (∀x.¬P (x))). \end{matrix}

5. Discussion

We have extended circumscription by removing the restraints on what models can be compared. In this new form of circumscription maximizing is not the same as minimizing. This form of circumscription subsumes both domain and predicate/formula circumscription. It does not have difficulties representing defaults about equality or domains. It naturally captures defaults that are not expressible in other frameworks. This form of circumscription, unlike classic circumscription, extends naturally to non-finitely axiomatizable theories.

Acknowledgements

The author wishes to thank John McCarthy, Johan van Benthem, Grigori Mints and Anna Patterson for their assistance and advice.

References

J. Arima. A connotative treatment of circumscription. Technical Report TM-0640, Institute for New Generation

Computer Technology, 1988. C. Chang and H. Keisler. Model Theory, volume 73 of Studies in Logic and the foundations of mathematics. North

Holland, third edition, 1990. Tom Costello. Non-monotonicity and Change. PhD thesis, Stanford University, 1997. Craig and Vaught. Finite axiomatizability using additional predicates. Journal of Symbolic Logic, 23:289–308, 1958. P. Doherty, W. Lukaszewicz, and A. Szalas. Computing Circumscription Revisited: A Reduction Algorithm. Journal

of Automated Reasoning, x:1–42, 1996. D. W. Etherington, R. E. Mercer, and R. Reiter. On the Adequacy of Predicate Circumscription for Closed World

Reasoning. Computational Intelligence, 1, 1985. S. Feferman. Applications of many sorted interpolation theorems. In Proceedings of the Symposium on Pure Mathe-

matics, pages 102–148. American Mathematical Society, 1974. D. M. Gabbay and H. Jürgen. Quantifier Elimination in Second Order Logic. South African Computer Journal,

7:35–43, July 1992. D. M. Gabbay and H. Jürgen. Quantifier Elimination in Second Order Logic. In Proc. Third International Conference

on Principles of Knowledge Representation and Reasoning (KR ’92), pages 425–435, San Francisco, CA, 1992. Morgan Kaufmann.

D. Gabbay and H.J Olbach. Quantifier elimination in second-order predicate logic. Technical Report MPI-I-92-231,

Max-Planck Institut für Informatik, Saarbruüken, 1992. S. Kleene. Finite axiomatizability of theories in the predicate calculus using additional predicate symbols. In S. Kleene,

editor, Two papers on the predicate calculus, Memoirs of the American Mathematical Society No. 10, volume 10. American Mathematical Society, 1952.

S. Kraus, D. Lehmann, and M. Magidor. Nonmonotonic Reasoning, Preferential Models and Cumulative Logics.

Artificial Intelligence, 44(1):167–207, 1990. V. Lifschitz. Some Results on Circumscription. In First Workshop on Non-monotonic Reasoning, pages 151–164,

Stanford University, August 1984. V. Lifschitz. Computing Circumscription. In Proc. Ninth International Joint Conference on Artificial Intelligence

(IJCAI ’85), pages 121–127, 1985. J. McCarthy. Epistemological Problems of Artificial Intelligence. In Proc. Fifth International Joint Conference on

Artificial Intelligence (IJCAI ’77), pages 223–227, Cambridge, MA, 1977. J. McCarthy. Circumscription - a Form of Non-Monotonic Reasoning. Artificial Intelligence, 13(1 and 2):27–39, 1980. J. McCarthy. Applications of Circumscription to Formalizing Commonsense Knowledge. Artificial Intelligence,

28:89–116, 1986.

Address for correspondence: Dept. of Computer Science, Stanford University, Stanford, CA 94305