Domain Formula Circumscription

Tom Costello

costello@steam.Stanford.EDU Dept. Computer Science, Stanford University Stanford, CA 94305

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.

This paper has not been submitted elsewhere in identical or similar form.

Keywords: non-monotonic reasoning, circumscription, logic, knowledge representation, equality, second order logic.

1. Introduction

Circumscription was introduced by McCarthy(McCarthy, 1977) 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(McCarthy, 1980) and formula(McCarthy, 1986) 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(Lifschitz, 1985) of the theory^{1}—if the theory had a model with domain A, then the circumscribed theory would have a model of domain A.

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.

1. This is only true if the the theory is well founded, or smooth in the terminology of (Kraus,

Lehmann, & Magidor, 1990). However, we gloss over this point, as we are only interested in this

case.

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, 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 froms of circumscription can be found in (Costello, 1997), where it is show that in the finite propositional case formula circumscription can capture all pre-orders on valuations. This is not the case in for first order structures. Indeed, the second chapter of (Costello, 1997) 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 strcutures can not be captured lifts easily to the case of domain formula circumscription.

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 17). 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 3,5,6) 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 satsifiable 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 (Etherington, Mercer, & Reiter, 1985). Modifications to circumscription to avoid this issue are discussed in (Costello, 1997).

Before we look at this new form of circumscription we consider previous versions of circumscription.

1.1 Domain Circumscription

McCarthy’s original example of non-monotonic reasoning was about the lack of a bridge (in the missionaries and cannibals problem)(Amarel, 1968). The idea of minimizing objects was therefore the first attempted solution. All of the objects in the problem were minimized—if they could fail to exist, then they were assumed not to exist.

Historically, domain circumscription was the earliest form of circumscription. It was introduced in (McCarthy, 1977). It was studied by Davis(Davis, 1980), and further investigated by Etherington and Mercer(Etherington & Mercer, 1987).

Domain description tries to capture the intuition that as few objects exist as possible. It attempts to carry out something like domain closure, that is to state that the only objects that exist are those that must exist.

The model theory for domain circumscription is applicable to arbitrary classes of models, however the syntactic form of domain circumscription restricts the set of theories to those axiomatizable by a finite set of first order sentences.

We now look at McCarthy’s definition of domain circumscription. We need an auxiliary definition of a formula which McCarthy called^{2} Axiom(ϕ), but which we call Closed_{L}(ϕ), as it states that ϕ is closed under the application of all the functions in L.

Definition: 1 (Closed_{L}(ϕ)) If ϕ is a unary predicate variable, Closed_{L}(ϕ) stands for the conjunction of ϕ(c) for every constant c in the language L, and the ∀x_{1} …, x_{n}.ϕ(x_{1}) ∧ … ϕ(x_{n}) → ϕ(f(x_{1}, …, x_{n})), for each n-ary function constant f in L.

2. We use ϕ for unary predicate variables, ψ for predicate variables of arbitrary arity, β, γ, δ for

formulas, α for sentences, L for languages, ζ for function variables, x, y, z, v, l, p for individual

variables, t for terms, Γ, Δ, for sets of formulas, \overline{P} , Z for sets of predicates, capital Roman letters

or words for predicate symbols, f for function symbols, c and capital Roman letters for constant

symbols, a, b for objects, German font for models, U for domains, S for sorts, and K to range

over all constants in a language. All of these may have subscripts. We note that α′ is used as an

abbreviation, not as a formula name.

We also need the standard notion of the relativization of a formula by a unary predicate.

Definition: 2 The relativization of a formula γ with respect to a unary predicate variable ϕ, written γ^{ϕ}, is the result of replacing ∀x. and ∃x. by ∀x.ϕ(x) → and ∃x.ϕ(x)∧ in γ, defined inductively as follows.

• If γ = P (t_{1}, …, t_{n}) then γ^{ϕ} = P (t_{1}, …, t_{n}).

• If γ = α ∧ β then γ^{ϕ} = α^{ϕ} ∧ β^{ϕ}.

• If γ = α ∨ β then γ^{ϕ} = α^{ϕ} ∨ β^{ϕ}.

• If γ = α → β then γ^{ϕ} = α^{ϕ} → β^{ϕ}.

• If γ = ¬α then γ^{ϕ} = ¬α^{ϕ}.

• If γ = α ≡ β then γ^{ϕ} = α^{ϕ} ≡ β^{ϕ}.

• If γ = ∃x.α then γ^{ϕ} = ∃x.ϕ(x) ∧ α^{ϕ}.

• If γ = ∀x.α then γ^{ϕ} = ∀x.ϕ(x) → α^{ϕ}. If ϕ_{1}, ϕ_{2} is a sequence of predicate variables, then γ^{ϕ_{1},ϕ_{2}} denotes the iterated relativization of γ, i.e. (γ^{ϕ_{1}})^{ϕ_{2}}.

Definition: 3 The domain circumscription of the sentence α in a language L, denoted DomCirc_{L}(α), is the following formula of second order logic.

α ∧ ∀ϕ.Closed_{L}(ϕ) ∧ α^{ϕ} → ∀x.ϕ(x) where ϕ is a one place predicate variable.

Domain circumscription has a natural semantics. We say that one model 𝔄 is ≤_{domain} than another model 𝔅, if and only if 𝔄 is a sub-model of 𝔅. By this we mean that 𝔄 is the reduct of 𝔅 to the domain of 𝔄. The relation sub-model naturally forms a pre-order. The minimal models under this pre-order are the intended models of domain circumscription.

Definition: 4 For a given language L and two L-structures, 𝔄 and 𝔅, we say that 𝔄 ≤_{domain} 𝔅, if and only if 𝔄 is a sub-model of 𝔅.

Example: 1 Let the sentence α be the conjunction of the following sentences:

Bird(T weety) ∧ P enguin(Opus),  (1)
∀x.P enguin(x) → Bird(x).  (2)

The domain circumscription of this theory is the above sentences conjoined with,

∀ϕ.[ϕ(T weety) ∧ ϕ(Opus) ∧ Bird(T weety) ∧ P enguin(Opus)∧
∀x.[ϕ(x) → (P enguin(x) → Bird(x))]] → ∀x.ϕ(x).

This entails,

∀x.x = T weety ∨ x = Opus.

In fact it is equivalent to,

(∀x.x = T weety ∨ x = Opus) ∧ Bird(T weety) ∧ Bird(Opus) ∧ P enguin(Opus), that is, it has three models, one containing a single object which is both a penguin and a bird, and two models containing two objects, one called Tweety, one called Opus, where all objects are birds, and either just Opus is a penguin, or both birds are Penguins.

To show this we use the standard trick(Lifschitz, 1985) of removing second order quantifiers. We do this by instantiating the quantifier ∀ϕ by λx.x = T weety ∨ x = Opus.

1 Theorem: (McCarthy 1977,Soundness) Let ⊢ represent any sound proof theory for second order logic.

If DomCirc_{L}(α) ⊢ γ then γ is true in every minimal model of α under the preorder ≤_{domain}.

Etherington and Mercer modified the definition of domain circumscription by adding a conjunct, ∃x.ϕ(x), to the left hand side of the implication in the definition. This is only of interest in the case when the signature of the language contains no constants. If the language contains a constant c, ϕ(c) is added as part of Closed_{L}. As ϕ(c) implies ∃x.ϕ(x), adding ∃x.ϕ(x) makes no difference in this case. From now on we assume that there are some constants.

1.2 Predicate Circumscription

McCarthy introduced a new form of circumscription predicate circumscription(McCarthy, 1980). This form of circumscription differed greatly from domain circumscription. It was not an extension, there being problems that domain circumscription could solve that predicate circumscription could not.

It was also based on minimization, but rather than minimize the amount of objects in the domain, it minimized the extension of a predicate symbol. McCarthy originally defined it as a first order logic schema, however it is more easily understood as a sentence of second order logic.

Definition: 5 (≤, < on formulas) It is useful to introduce the notation γ_{1}, γ_{2} ≤ δ_{1}, δ_{2} for the formula (∀\overline{x}.γ_{1}(\overline{x}) → δ_{1}(\overline{x})) ∧ (∀\overline{y}.γ_{2}(\overline{y}) → δ_{2}(\overline{y})), and γ_{1}, γ_{2} < δ1, δ_{2} for the formula γ_{1}, γ_{2} ≤ δ_{1}, δ_{2} ∧ ¬(δ_{1}, δ_{2} ≤ γ_{1}, γ_{2}), where \overline{x} and \overline{y} are sequences of variables equal in number to the free variables of γ_{1}, δ_{1} and γ_{2}, δ_{2}.

This definition of predicate circumscription does not allow “varied” predicates. We later look at formula circumscription, a version that does allow varied predicates. McCarthy(McCarthy, 1980) suggested varying predicates, but gave no examples. In our definitions of circumscription from now on we assume that we minimize two formulas/predicates, in a language with one or two predicate symbols, one function symbol, and one constant. The extension to n predicates/formulas, and larger languages is the obvious one.

Definition: 6 Let L be a first order language with equality, whose predicates include P_{1}, P_{2}. Let α be a sentence in L. The circumscription of α minimizing P_{1}, P_{2}, denoted Circ_{P} (α; P_{1}, P_{2}) is the second order formula:

α ∧ ∀ψ_{1}, ψ_{2}.¬ [α[ψ_{1}/P_{1}, ψ_{2}/P_{2}] ∧ ψ_{1}(\overline{x}), ψ_{2}(\overline{y}) < P_{1}(\overline{x}), P_{2}(\overline{y})]

where ψ_{1} and ψ_{2} are predicate variables equal in arity to P_{1} and P_{2}, and \overline{x}, \overline{y} are tuples of variables.

We now introduce semantics for predicate circumscription. We use A to denote the domain of 𝔄, and 𝔄[K] to denote the interpretation of K in 𝔄.

Definition: 7 Let α be a sentence of L, a first order language with equality, whose predicates are \{P_{1}, …, P_{n}\}. Let \overline{P} be a subset of P_{1}, …, P_{n}. A model 𝔄 of α is a \overline{P} -sub-model of a model 𝔅, written 𝔄 ≤\overline{P} 𝔅, if and only if:

• A = B, that is the domains of 𝔄 and 𝔅 are equal.

• 𝔄[K] ⊆ 𝔅[K], for every predicate constant K ∈ \overline{P},

• 𝔄[K] = 𝔅[K], for every function, object, or predicate constant K not in \overline{P}.

𝔄 is \overline{P} -minimal model of A if and only if no other model of α is a \overline{P} -sub-model of 𝔄.

2 Theorem: (McCarthy 80) Let α, γ be sentences of L, a first order language with equality, whose predicates are \{P_{1}, …, P_{n}\}. Let \overline{P} be a subset of P_{1}, …, P_{n}.

If ⊢ is a sound inference system for second order logic, then if Circ_{P} (α; \overline{P}) ⊢ γ then γ is true in every \overline{P} -minimal model of α.

We now look at a simple example of circumscription, taken from Lifschitz(Lifschitz, 1985).

Example: 2 Consider the language L, with a unary predicate P and three constants B, C, and D, let the sentence α be P (D) ∨ (P (B) ∧ P (C)), then

Circ_{P} (α; P) ≡ (∀x.P (x) ≡ x = D) ∨ (∀x.P (x) ≡ x = B ∨ x = C ∧ D ≠ B ∧ D ≠ C).

1.3 Formula Circumscription

McCarthy(McCarthy, 1986) introduced a new form of circumscription, called formula circumscription. It extends predicate circumscription in two ways.

• The new form of circumscription allows the extensions of arbitrary formulas to be minimized rather than only minimizing predicates.

• Certain predicates are allowed to be varied in the minimization process. This notion was suggested, but not explored, by McCarthy(McCarthy, 1980).

Definition: 8 If γ_{1}, γ_{2} is a pair of formulas of a first order language L, and P_{1} is a predicate symbol of L, then the circumscription of α minimizing γ_{1}, γ_{2}, formulas in L, varying P_{1}, written Circ_{F} (α; γ_{1}, γ_{2}; P_{1}) is,

α ∧ ∀ψ_{1}.¬ [α′ ∧ γ′_{1}, γ′_{2} < γ_{1}, γ_{2}]

where ψ_{1} is a predicate variable equal in arity to P_{1}. We use α′ to denote the formula, α[ψ_{1}/P_{1}], that is the replacement of the predicate P_{1} in α by a predicate variable.

We now introduce the semantics for formula circumscription.

Definition: 9 Let α be a sentence of L, a first order language with equality, whose predicates are P_{1}, …, P_{n}. Let Z be a subset of P_{1}, …, P_{n}. A model 𝔄 of α is a γ_{1}, … γ_{n}; Z-sub-model of a model 𝔅, written 𝔄 ≤_{γ_{1},...γ_{n};Z} 𝔅, if and only if:

• ∥𝔄∥ = ∥𝔅∥,

• 𝔄[γ_{i}] ⊆ 𝔅[γ_{i}], for i = 1 … n.

• 𝔄[K] = 𝔅[K], for every function, object, or predicate constant not in Z.

𝔄 is a γ_{1}, … γ_{n}; Z-minimal model of A if and only if it is a minimal model of α under ≤_{γ_{1},...γ_{n};Z}.

3 Theorem: (McCarthy 1986) Let α, β, γ_{1}, …, γ_{n} be sentences of L, a first order language with equality, whose predicates are {P_{1}, …, P_{n}}. Let Z be a subset of P_{1}, …, P_{n}.

If ⊢ is a sound inference system for second order logic, then If Circ_{F} (α; γ_{1}, …, γ_{n}; Z) ⊢ β then β is true in every γ_{1}, … γ_{n}; Z-minimal model of α.

1.4 Second Order Circumscription

Lifschitz(Lifschitz, 1985) modifies the definition of circumscription to allow the varied symbols to include constant or function symbols.

deKleer and Konolige prove(de Kleer & Konolige, 1989) that not varying a predicate symbol, in formula circumscription, can be expressed by minimizing both the predicate symbol and its negation. Thus we may assume that all predicates are varied.

Definition: 10 (Circ(α; Γ)) If γ_{1}, γ_{2} is a pair of formulas in a first order language L, and P, f, c are the predicates, functions and constants in L, then we define the circumscription of a sentence α in L minimizing γ_{1}, γ_{2}, written Circ(α; γ_{1}, γ_{2}) as follows. We use α′ to denote the formula α[ψ/P, ζ/f, x/c], that is the replacement of the predicates P, functions F and constants c in α by predicate, function and constant variables, ψ, ζ and x, respectively.

α ∧ ∀ψ, ζ, x.¬ [α′ ∧ γ′_{1}, γ′_{2} < γ_{1}, γ_{2}] ,

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

Definition: 11 (≤_{Γ}) If two L-structures have the same domain then we say they are comparable. We say two comparable structures 𝔄 and 𝔅 are in the relation ≤_{Γ}, where Γ is a set of formulas in L, if the extension in 𝔄 of each formula in Γ is a subset of the extension of that formula in 𝔅.

In model theoretic terms, the consequences of second order circumscription are the sentences true in all minimal models under this pre-order ≤_{Γ}. This is now the most common form of circumscription.

1.5 Other Modifications of Circumscription 1.5.1 Hintikka

Hintikka(Hintikka, 1988) suggests model minimization as an alternative to domain circumscription. Rather than prefer one model to another when the second is a submodel of the first, he suggests that one model be preferred to another when the first is isomorphic to a sub-model of the second. This is essentially the notion of varying all predicates in domain circumscription. Lorenz(Lorenz, 1994) calls this variable domain circumscription. Doherty, Lukaszewicz and Szalas(Doherty, Lukaszewicz, & Szalas, 1996b) suggest an extension, general domain circumscription, where subsets of the predicates functions and constants are allowed to vary.

1.5.2 Bossu and Siegel

Bossu and Siegel(Bossu & Siegel, 1984) proposed a treatment of non-monotonicity which is similar to circumscription. There are two notable differences however. Firstly they restrict themselves to minimizing every predicate symbol. Secondly, and more importantly, they change the notion of non-monotonic consequence. Rather than looking at the sentences that are true in all minimal models, they look at the sentences that are true at some model, and in all smaller models. In this way they drop the restriction that minimal models must exist.

1.5.3 Shoham

Shoham(Shoham, 1988) suggests that non-monotonic reasoning can be characterized by defining the sentences non-monotonically entailed by a theory as those sentences that are true in the minimal models of that theory, under some partial order. He considered other languages not just first order logic, and he considered arbitrary partial orders, not just those defined by circumscription policies. This work has been greatly extended in the study of non-monotonic consequence relations, (Gabbay, 1985; Kraus et al., 1990; Makinson, 1989, 1994) and others, an area outside the remit of this paper.

1.5.4 Rathmann, Winslett and Manasse

Rathmann, Winslett and Manasse(Rathmann, Winslett, & Manasse, 1990, 1994) introduce a form of circumscription that they call structural circumscription. It is similar in model theoretic terms to classical circumscription, save that it redefines the notion of ≤ on the models of a sentence α. One model 𝔐 is ≤ a model 𝔑 is there is a homomorphism h, a function from the domain U_{1} of 𝔑 to the domain U of 𝔐, that satisfies the following conditions:

• The mapping h preserves functions constants and predicates that are not varied. If f is function, predicate or constant symbol from α’s signature, with extensions f_{𝔐} and f_{𝔑} in 𝔐 and 𝔑, we require that:

∀a_{1}, …, a_{n} ∈ U_{1}.h(f_{𝔑}(a_{1}, …, a_{n})) = f_{𝔐}(h(a_{1}), …, h(a_{n}))

Where n is the appropriate arity for each predicate and function, and is 0 for constants.

• The truth of minimized formulas is preserved. If γ is a minimized n-ary formula with extensions γ_{𝔐} and γ_{𝔑}, in 𝔐 and 𝔑, with n object variable and m predicate variables, then

∀a_{1}, …, a_{n} ∈ U_{1}b_{1}, …, b_{m} ∈ 2^{U_{1}}.γ_{𝔑}(a_{1}, …, a_{n}, b_{1}, …, b_{m}) →
γ_{𝔐}(h(a_{1}), …, h(a_{n}), h(b_{1}), …, h(b_{m}))

This defines a pre-order, and the consequences of the structural circumscription of a sentence α minimizing γ_{1}, …, γ_{n}, varying \overline{Q}, \overline{F}, \overline{C}, written StrCirc(α; γ_{1}, …, γ_{n}; \overline{Q}, \overline{F} , \overline{C}) are the sentences true in all minimal models under the pre-order ≤.

Structural circumscription does achieve maximally unique names. However it also affects that part of the domain of objects that is not referred to by closed terms. This is not warranted by the original definition of the unique names assumption.

A second problem with structural circumscription is that it does not allow equality to be varied. This can be avoided by changing the semantics, as proposed by Rathmann et al.(Rathmann et al., 1994), but then the original ideas of Goguen and Burstall’s(Goguen & Burstall, 1985) initial models are lost. The preferred models are no longer the initial models of the theory, as preference is no longer defined in terms of homomorphisms, but rather in terms of a binary relation which they call a generalized homomorphism.

1.5.5 Other Suggestions

Minker and Perlis(Minker & Perlis, 1984) suggest protected circumscription, which modifies circumscription in an analogous way to allowing predicates to be varied. Perlis(Perlis, 1987) looks at how circumscription can be described in the language of set-theory rather than second order logic. Auto-circumscription,(Perlis, 1988) is a version of circumscription that provides for negative introspection. Lifschitz(Lifschitz, 1989b) also considers this question. The modifications we suggest are also appropriate in these cases.

Non-recursive circumscription(Mott, 1987) builds on Minker and Perlis’s variable circumscription(Perlis & Minker, 1986). It weakens the circumscription formula so that it can no longer map satisfiable theories to unsatisfiable theories. We recognize that this is an important issue, but again this question lies outside the scope of this paper. Besnard, Moinard, and Mercer(Besnard, Moinard, & Mercer, 1989) stress the importance of the extra expressive power that full circumscription gives over nonrecursive circumscription.

Lifschitz(Lifschitz, 1986) explores the connection between logic programming and circumscription using a new variant, called pointwise circumscription. Its novelties include a weakening of circumscription, so that models are connected, in that the minimal models can be reached by changing instances of a predicate from true to false at a “point”. More importantly, it introduces a richer language for describing preferences. This work has been extended in the framework of pointwise circumscription (Lifschitz, 1989a).

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: 12 (≤_{Γ;Δ} ) 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 |B ∪ X|, where X is some set with cardinality ℵ_{0}.

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

Lemma: 2 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}) which is ≤_{Γ;Δ} than 𝔅, and 𝔅 ≰_{Γ;Δ} 𝔄.

Proof: Suppose that an L-structure ℭ is ≤_{Γ;Δ} than 𝔅, and 𝔅 is not ≤_{Γ;Δ} than ℭ. Take an elementary sub-model of ℭ, whose domain contains (B ∩ C) ∪ Y where Y is a countable set from C, and whose domain is included in (B ∩ C) ∪ 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(Chang & Keisler, 1990) proposition 2.2.17.

The restriction of ℭ to the domain (B ∩ C) ∪ Y is a sub-model of ℭ, as long as (B ∩ C) ∪ Y is non-empty. If B ∩ C is empty, then as ℭ is ≤_{Γ;Δ} than 𝔅, 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. 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 langauge is countable by assumption. Thus, without loss of generality, we can take (B ∩ C) ∪ 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 langauge is countable.

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

Let γ be a formula in Γ and δ a formula in Δ, then 𝔄[γ] ⊆ ℭ[γ], as 𝔄 is an elementary sub-model. However, ℭ[γ] ⊊ 𝔅[γ], by our assumption. Thus, 𝔄[γ] ⊊ 𝔅[γ], as required.

As 𝔅[δ] ⊊ ℭ[δ], thus 𝔅[δ] ⊊ ℭ[δ] ∩ ((B^{n} ∩ C^{n}) ∪ 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 C and B, as they are in B by definition, and in C by the subset assertion. Thus 𝔅[δ] ⊆ ℭ[δ] ∩ ((B^{n} ∩ C^{n}) ∪ Y^{n}).

We are given 𝔅[δ] ⊊ ℭ[δ], thus there is a tuple c such that c ∈ ℭ[δ] and c ∉ 𝔅[δ]. We need to ensure that this tuple c is in our model ℭ[δ] ∩ (B^{n} ∩ C^{n} ∪ Y^{n}), for each δ. However, as Δ is finite, a countable set of objects Y suffices. This is the countable set Y we posited earlier.

Thus 𝔅[δ] ⊊ 𝔄[δ], as 𝔄 contains all the elements in (B^{n} ∩ C^{n} ∪ Y^{n}). □

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 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 5) we saw earlier. We will need to say that a set of predicates variables ϕ_{i} act correctly as domains for the sorts of L. They must contain the correct constants, and be closed under functions.

Definition: 13 ( CL_{L}^{\{ϕ_{1},... ,ϕ_{o}\}}(\{ζ_{1}, …, ζ_{n}\}, \{x_{1}, … x_{m}\})) If 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 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: 14 (inf) Let L be a first order language. We define inf(L) to be the sentence in the 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 supersort 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. We also state that all the sorts in the language are countable. This is so that we can generate models with universes in our new sort, that correspond to whatever models are possible.

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 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: 15 (Domain Formula Circumscription) If γ_{1}, γ_{2} is a pair of formulas in a first order language L to minimize, and δ_{1}, δ_{2} is 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.

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

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, (Doherty, Lukaszewicz, & Szalas, 1996a) and (Gabbay & Olbach, 1992) 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 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: 3 We consider a language 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 ∧ ∀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

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

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

The DLS algorithm is easiest to explain in an unsorted logic, thus we explicitly add sorts.

P (B) ∧ P (C) ∧ S(B) ∧ S(C) ∧ inf ∧ ∀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.

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

We put the matrix into disjunctive normal form.

∃b, c, P′ϕ.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)).

We consider each conjunct separately. The first is immediately True as P′ occurs only positively. We consider the second.

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

We separate the positive occurences from the negative occurences.

∃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,

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

We negate this to get our answer,

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

However, as we are given S(C) and S(B), as we are told that B and C are in the sort S, the circumscription formula is equivalent to

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

We now give an example where we vary the domain.

Example: 4 (Witnesses) Tom, Dick, and Harry are members of a criminal organization. We have a default however 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 (McCarthy, 1986).

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 this models there are crimes that are not witnessed.

Thus, if we circumscribe normally 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}(Crime; ∀p.Crimeloc(l) → ¬At(p, l) ∨ F elon(p), Crimeloc(l); Crimeloc(l))

by using the DLS alorithm. 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.

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: 5 Let the sentence α be the conjunction of,

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

We now minimize P enguin, and then we maximize ¬P enguin We see that

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

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

Proposition: 3 Maximizing a formula in domain formula circumscription is not the same as minimizing its negation.

Proof: Immediate from the example above. □

Theorem: 4 If α is a finitely axiomatizable first order theory in a first order language L, viewed as a sentence, and Γ, Δ are finite sequences of formulas in L, and γ is a sentence in 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 2 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: 5 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. If 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 regular circumscription.

Proposition: 6 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(McCarthy, 1977).

Proposition: 7 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 every predicate, function, and constant symbol. This is an equivalent sentence of second order logic.□

Proposition: 8 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 ¬γ.□

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: 6 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.(Etherington et al., 1985) 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 firstorder 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.

4 Theorem: (Etherington et al., 1984) Let α be a first order sentence containing, as a conjunct, the axioms for equality. Then Circ(α; =) ⊧ α.

5 Theorem: (Etherington et al., 1984) Suppose that α is a well-founded 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(McCarthy, 1986), where he 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: 16 (McCarthy Equality Theory) Given a first order language ⟨{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 McCarthy 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}. ⋀_{j=1}^{k} e(x_{j}, y_{j}) → P_{i}(x_{1}, …, x_{k}) ≡ P_{i}(y_{1}, …, y_{k})

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(Lifschitz, 1984) describes a different approach using true equality rather than a new predicate e. His method has been substantially extended by Arima(Arima, 1988). 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 results 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(Kleene, 1952), 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(Craig & Vaught, 1958) and one due to Feferman(Feferman, 1974).

Definition: 17 (conservative extension) A theory A over a first order language L, is a conservative extension of a theory A_{1} over 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: 18 (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 Δ, are the consequences of Circ_{D}(α, Γ; Δ) that are in the language L_{1}, where α is a conservative extension of A_{1}.

Theorem: 9 If α is a finitely axiomatizable theory in a language L_{1}, viewed as a sentence, then,

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

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

Theorem: 10 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 variable v_{i} ranging over the sort S_{2}. Let α be the sentence ∃v_{1}, v_{2}.v_{1} ≠ v_{2} ≡ P (B). Then,

Circ(A_{1}; P) ≡ ∀x.¬P (x),

while,

Circ(A; P) ≡ (∀x.P (x) ≡ x = B ∧ ∀v_{1}, v_{2}.v_{1} = v_{2}).

□

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 and Anna Patterson for their assistance and advice.

References

Amarel, S. (1968). On representations of problems of reasoning about actions. In Michie, D. (Ed.), Machine Intelligence 3, Vol. 3, pp. 131–171. Elsevier/North-Holland, Amsterdam, London, New York.

Arima, J. (1988). A connotative treatment of circumscription. Tech. rep. TM-0640, Institute for New Generation Computer Technology.

Besnard, P., Moinard, Y., & Mercer, R. E. (1989). The Importance of Open and

Recursive Circumscription. Artificial Intelligence, 39 (2). Bossu, G., & Siegel, P. (1984). Saturation, nonmonotonic reasoning, and the closed

world assumption. Artificial Intelligence, 25 (1), 13–64. Chang, C., & Keisler, H. (1990). Model Theory (third edition edition)., Vol. 73 of

Studies in Logic and the foundations of mathematics. North Holland. Costello, T. (1997). Non-monotonicity and Change. Ph.D. thesis, Stanford University. Craig, & Vaught (1958). Finite axiomatizability using additional predicates. Journal

of Symbolic Logic, 23, 289–308. Davis, M. (1980). The mathematics of non-monotonic reasoning. Artificial Intelli-

gence, 13 (1–2), 73–80. de Kleer, J., & Konolige, K. (1989). Eliminating the Fixed Predicates from a Cir-

cumscription. Artificial Intelligence, 39, 391–398. Doherty, P., Lukaszewicz, W., & Szalas, A. (1996a). Computing Circumscription

Revisited: A Reduction Algorithm. Journal of Automated Reasoning, x, 1–42. Doherty, P., Lukaszewicz, W., & Szalas, A. (1996b). General Domain Circumscription

and its First-Order Reduction. Tech. rep. LiTH-IDA-R-01, Linköping University.

Etherington, D. W., & Mercer, R. E. (1987). Domain circumscription: A reevaluation. Computational Intelligence, 3 (2), 94–99.

Etherington, D. W., Mercer, R. E., & Reiter, R. (1985). On the Adequacy of Predicate Circumscription for Closed World Reasoning. Computational Intelligence, 1.

Feferman, S. (1974). Applications of many sorted interpolation theorems. In Proceedings of the Symposium on Pure Mathematics, pp. 102–148. American Mathematical Society.

Gabbay, D. (1985). Theoretical foundations for non-montonic reasoning in expert systems. In Apt, K. R. (Ed.), Logics and Models of Concurrent systems. Springer Verlag.

Gabbay, D., & Olbach, H. (1992). Quantifier elimination in second-order predicate logic. Tech. rep. MPI-I-92-231, Max-Planck Institut für Informatik, Saarbruüken.

Goguen, J. A., & Burstall, R. M. (1985). Institutions: Abstract model theory for computer science. Tech. rep. CSLI-85-30, Center for Study of Language Logic and Information, Stanford.

Hintikka, J. (1988). Model minimization - an alternative to circumscription. Journal of Automated Reasoning, 4, 1–13.

Kleene, S. (1952). Finite axiomatizability of theories in the predicate calculus using additional predicate symbols. In Kleene, S. (Ed.), Two papers on the predicate calculus, Memoirs of the American Mathematical Society No. 10, Vol. 10. American Mathematical Society.

Kraus, S., Lehmann, D., & Magidor, M. (1990). Nonmonotonic Reasoning, Preferential Models and Cumulative Logics. Artificial Intelligence, 44 (1), 167–207.

Lifschitz, V. (1984). Some Results on Circumscription. In First Workshop on Nonmonotonic Reasoning, pp. 151–164 Stanford University.

Lifschitz, V. (1985). Computing Circumscription. In Proc. Ninth International Joint Conference on Artificial Intelligence (IJCAI ’85), pp. 121–127.

Lifschitz, V. (1986). Pointwise Circumscription. In Proc. National Conference on Artificial Intelligence (AAAI ’86).

Lifschitz, V. (1989a). Circumscriptive theories: a logic-based framework for knowledge representation. In Thomason, R. (Ed.), Philosophical Logic and Artificial Intelligence, pp. 109–160. Kluwer.

Lifschitz, V. (1989b). Between circumscription and autoepistemic logic. In Brachman, R. J., & Levesque, H. J. (Eds.), Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, pp. 235–244 Toronto, Ontario. Morgan Kaufmann.

Lorenz, S. (1994). A Tableuau Prover for Domain Minimization. Journal of Automated Reasoning, 13, 375–390.

Makinson, D. (1989). General Theory of Cumulative Inference. In Reinfrank, de Kleer, Ginsberg, & Sandewall (Eds.), Non-Monotonic Reasoning. Lecture Notes in Artificial Intelligence 346, Springer-Verlag.

Makinson, D. (1994). General patterns in nonmonotonic reasoning. In Gabbay, D. M., Hogger, C. J., & Robinson, J. A. (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. Vol. 3, Nonmonotonic and Uncertain Reasoning, pp. 35–110. Oxford University Press.

McCarthy, J. (1977). Epistemological Problems of Artificial Intelligence. In Proc. Fifth International Joint Conference on Artificial Intelligence (IJCAI ’77), pp. 223–227 Cambridge, MA.

McCarthy, J. (1980). Circumscription - a Form of Non-Monotonic Reasoning. Artificial Intelligence, 13 (1 and 2), 27–39.

McCarthy, J. (1986). Applications of Circumscription to Formalizing Commonsense Knowledge. Artificial Intelligence, 28, 89–116.

Minker, J., & Perlis, D. (1984). Protected circumscription. In Proc Workshop on Non-Monotonic Reasoning, pp. 337–343 New Platz.

Mott, P. L. (1987). A theorem on the Consistency of Circumscription. Artificial Intelligence, 31, 87–98.

Perlis, D. (1987). Circumscribing with Sets. Artificial Intelligence, 31, 201–211.

Perlis, D. (1988). Autocircumscription. Artificial Intelligence, 36, 223–236.

Perlis, D., & Minker, J. (1986). Completeness Results for Circumscription. Artificial Intelligence, 28, 29–42.

Rathmann, P. K., Winslett, M., & Manasse, M. (1994). Circumscription with homomorphisms: Solving the equality and counterexample problem. Journal of the ACM, 41 (5), 819–873.

Rathmann, P. K., Winslett, M., & Manasse, M. (1990). Equality and circumscription. Tech. rep. 1615, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, Illinois.

Shoham, Y. (1988). Reasoning about Change. MIT Press, Cambridge, USA.