Cofinal Circumscription

Tom Costello

Abstract

Circumscription is a form of non-monotonic reasoning, introduced by McCarthy (1977) as a way of characterizing common-sense defaults. It characterizes the non-monotonic consequences of a theory, as the formulas true in the minimal models of that theory under a partial-order. However, there are partial orders with no minimal models. In this case circumscription maps a satisfiable theory to falsity.

This would be of purely academic interest, but for the fact that many natural defaults have this character of lacking minimal models. The set of intuitive consequences of these defaults is not all sentences.

We propose an alternative to minimal semantics. We propose that reasonable beliefs are those whose models contain a dense ideal of the partial-order. We then look at some properties of this choice, for example, does it preserve the structural properties of circumscription?

We then look at how we can use this insight to modify circumscription, so that it maps satisfiable theories to satisfiable theories.

1 Introduction

Circumscription is a form of non-monotonic reasoning. It allows the default conclusions of a theory to be expressed in second order logic. It was introduced by McCarthy (1977, 1980, 1986). Classical logic has the property of monotonicity, if a conclusion is warranted by a set of premises, then it is warranted by every superset of those premises. It is precisely this property that non-monotonic logics deny.

In reasoning about common-sense phenomena humans often make judgments that are not certain. These conclusions later may have to be withdrawn in the light of new evidence. If we want computers and robots to function in the world they too will have to make speculative jumps that are not classically warranted. In Section 1.2 we give some examples of how a computer or robot could use non-monotonicity—or this ability to make leaps of judgment.

Circumscription is a formalism that allows us to make cognitive leaps of faith. It is based around the idea that a predicate or formula is minimized, or made true of as few things as possible. The consequences of this minimization can be defined in terms of the minimal models of a partial order on models. A model 𝔄 is considered minimal if no other model has an extension for that predicate that is a proper subset of the model 𝔄’s extension. This class of minimal models are the models of the circumscribed theory. This circumscribed theory contains conclusions that the original theory did not. Should new information be added however, these conclusions can be withdrawn.

The idea of using minimal models as a paradigm for non-monotonic reasoning was further considered by (Bossu and Siegel 1984) and later (Shoham 1986). Each of these took a different direction. Bossu and Siegel restricted the class of policy, or minimality criterion, but overcame the problem of presupposing that minimal models existed. They minimized all predicates, while circumscription classically only minimizes some predicates. They, following Lewis (1973), rejected the assumption that there were minimal models, and instead took as the resulting theory, all sentences true in sufficiently minimal models. Lewis called the assumption that there were minimal models or in his terminology, closest worlds, the Limit Assumption. Many orderings do not have the property that every subset of the ordering has a least element; ordering that have this property have been called well-founded by Lifschitz (1985), smooth by Kraus et al. (1990), and stoppered by Makinson(1989). Bossu and Siegel definition was in terms of all sufficiently minimal models, again following Lewis’s sufficiently close worlds. Removing the assumption that there was always a minimal model overcame the problem that circumscription could sometimes map a consistent theory onto the inconsistent theory.

Shoham took another path—he expanded the class of preferences between models to allow any preferences. Whereas in circumscription preferences must be expressible as set inclusion on the extension of a predicate or formula, Shoham considered all possible preferences. An advantage of this proposal is that new preferences are allowed, (however no new preferences are gained in the finite propositional case (Costello 1996b)) a disadvantage is that he did not supply a new language for describing these new preferences.

The formal system for circumscription, expressed in classical second order logic^{1}, was one of the strengths of circumscription. The benefits of a more expressive semantics are not as obvious if we lose the ability to represent the new semantics in a formal logical system.

1.1 Problems

Meanwhile, the formalization of circumscription itself was running into problems. Etherington et al. (1985) claimed that circumscription could never infer a new positive ground instance of a predicate. McCarthy attempted to answer this criticism in his 1986 paper (McCarthy 1986), explicating how predicates could be varied.

The varying of predicates allowed models that differed in some of their predicates to be compared. A set of predicates—called fixed predicates—that all comparable models must agree upon was specified. This allowed circumscription to infer new positive instances of varied predicates.

More seriously Etherington et al. following Davis (1980), show that circumscription could sometimes make theories inconsistent. This was not surprising in the light of the semantics being defined in terms of minimal models that did not necessarily exist. The set of minimal models always exists, it is, however, sometimes empty.

1This formalism was introduced by Lifschitz (1985), the original formalism was in terms of an axiom schema of first order logic.

1.2 Uses of Circumscription

Circumscription has been used for formalizing many different domains. We introduce a sample of these domains, where circumscription becomes inconsistent.

The assumption that a property is sufficiently or arbitrarily close to a certain value has many applications. In mathematics it is closely connected with the theory of limits. We say that a function f(x) has a value c in the limit as x approaches e, if for an arbitrarily small, non zero value δ we can always find a non-zero ϵ such that |x − e| < ϵ → |f(x) − c| < δ.

It is also used as a simplifying assumption in many common sense problems. If we are told that the price of a plane ticket is less than one hundred dollars, then for planning reasons it is wise to assume that it is only just less. To assume that it is $100 is inconsistent with what we have been told, so we cannot easily make that our assumption. On the other hand to assume that it was, say $40, is not in general wise.

We also use the notion of sufficiently or arbitrarily close to specify behaviors. This differs from making a simplifying assumption. When we make an assumption we give a different value to a particular property. When we ask what a person would buy for their birthday if money were no object, we implicitly ask them to imagine that they had an arbitrarily large amount of money. This differs from assuming that whatever one does one will have sufficient money. When we want to characterize behaviors, we want to describe the results not for just some finite set, but for as large an area of inputs as possible. When the range of inputs is open-ended we need to talk about arbitrarily large or small values.

We now look at some cases in particular. The first example concerns a group of MBA students who discover that they can intercept satellite transmissions of the new prices from the Tokyo Stock Exchange. They see an opportunity for profit if they can buy or sell before the rest of the stock exchange gets the information. They ask a mathematically inclined friend to calculate whether this is possible. She naturally asks how fast a computer they will use to do the necessary computation—perhaps there is a small amount of encryption. They tell her to assume that she can use any computer—money is no object. The question is how we characterize the last assumption, that there is unlimited financial resources to be spent on computers.

Example 1 We have a theory of the stock market T which includes time information. The time between the satellite transmission and the publication of the information is t, the time for transmission by the MBAs is a, the time for one transaction is b and the computer time t_{c} is characterized by the following rules.

money < $2000 → c = pentium ∧ t_{c} = 10

$2000 ≤ money < $1, 000, 000 → c = sparcstation ∧ t_{c} = 5 $1, 000, 000 ≤ money → c = cray ∧ t_{c} = 1

The question is whether a + b + t_{c} < t. We wish to minimize λx.money < x. That is we prefer models where interpretation of λx.money < x is smaller. This is equivalent to preferring models where money is larger. We can write this in the notation of circumscription as,

Circ(T; λx.money < x).

There are no minimal models in this order, minimal entailment entails falsity,

The intuitive answer is that t_{c} = 1. However, because the amount of money available can grow without bound, we have no minimal model.

Our next example concerns an old favorite of logical AI, the blocks world. We wish to say that we can move a block through a space, as long it has some space on either side. The question arises, ‘how much space is needed’? A natural assumption is that there is no particular amount of space needed, there just has to be some.

Example 2 We have one unit cube C, positioned at (0, 0, 0), at time 0 in our blocks-world. We also have a predicate empty(p, x, y, z), that states that a rectangular region x by y by z, centered at p, is empty. We consider the notation of the situation calculus, a formalism for reasoning about action introduced in (McCarthy and Hayes 1969). A recent presentation is found in (Gelfond et al. 1991). We have the axioms,

\begin{matrix}∀t.empty((0, 0, 0), 1, 1 + ϵ, 1 + ϵ) → \\ at(C, (1, 0, 0), result(move(C, (1, 0, 0), 0), t)), \end{matrix}

ϵ > 0.

In this case we know that the entire space is empty, save for our one block. We would like to infer that we can move the block one unit in the x direction.

Now, as before, we wish to minimize ϵ, that is our preference on modes prefers models with smaller interpretation of ϵ. There are no minimal models in this order.

Thus we see that there are common-sense examples where our assumptions lead to situations where we do not have minimal models.

These two examples share a feature that does not exist in general. The models were totally ordered, rather than partially ordered. The intuitive answer is much easier to grasp in these totally ordered situations. For this reason we give a third example, where we do not have this totality.

Example 3 This example concerns ice-cream. Rather than consider what we minimize, we draw out order directly, as this is easier to visualize. For simplicity there are two flavors of ice-cream, chocolate and vanilla. Ice-creams can also be compared in smoothness. Ice-cream with smaller ice-crystals is smoother. Our subject likes smoother vanilla ice-cream. That is, for any two vanilla ice-creams, he prefers the smoother.

He does not have a preference among chocolate ice-cream, “no chocolate ice-cream is better than any other, nor can chocolate ice-creams be compared to other flavors”.

Ice-cream is totally ordered with respect to smoothness. Thus, we can represent his preferences by the following diagram.

[figure: .; .; .; .; .; .; Chocolate; icey; Chocolate; crunchy; Chocolate; smoothish; Chocolate; creamy; Chocolate; extra creamy; Vanilla; icey; Vanilla; Vanilla; smoothish; Vanilla; creamy; Vanilla; extra creamy; More Preferred; crunchy]

It is worth noting that we have not decided whether or not there is a smoothest ice-cream. We might imagine that it is always possible to make a smoother ice-cream, in which case, his favorite ice-cream would be chocolate, despite the fact that he considers chocolate ice-cream incomparable to vanilla ice-cream.

Our second character shares this preference for smoother vanilla ice-cream, but for a given smoothness of ice-cream she prefers chocolate to vanilla. Thus her preferences can be drawn as,

[figure: .; .; .; .; .; .; Chocolate; icey; Chocolate; crunchy; Chocolate; smoothish; Chocolate; creamy; Chocolate; extra creamy; Vanilla; icey; Vanilla; Vanilla; smoothish; Vanilla; creamy; Vanilla; extra creamy; More Preferred; crunchy]

The important point her example raises is that her favorite flavor is chocolate. This is despite the fact that for any given ice-cream there is a vanilla ice-cream that she considers incomparable.

In the first case, minimal entailment will incorrectly assume that his preferred flavor is chocolate. In the second case, minimal entailment will correctly infer that her preferred flavor is chocolate. Later we shall see that the second example acts a counterexample to some other approaches.

1.3 Plan of Paper

We have now discussed circumscription, and the notion of minimal entailment, that is considering the formulas true in the minimal models of a certain partial order on models. The previous examples have shown that certain natural defaults cannot be modeled in this way. For this reason we now look for a modification of minimal entailment that captures the same intuitions, without the problems of sometimes leading to inconsistency.

As we mentioned earlier, a proposal to modify minimal entailment was propounded by Lewis. He considered total pre-orders on worlds. He said a formula was true in all sufficiently close possible worlds, if there was some world w, such that the formula was true in all worlds less than or equal w.

We consider partial orders, rather than total pre-orders. For this reason, Lewis’s proposal does not agree with minimal entailment, even for partial orders over finite domains. In general, there will be incomparable minimal models. Each minimal model can be taken as the world w, considered above. If one minimal model entails ϕ and the other ¬ϕ, then Lewis’s notion of true in sufficiently close possible worlds will lead to inconsistency.

For this reason we re-examine the intuition behind minimal entailment, by looking at what are the reasonable states of belief, given an partial order on likliehood of states of the world. This leads us to a notion of reasonable beliefs that has certain consistency properties. We show that it agrees with minimal entailment, when enough minimal models exist. Finally, we show how this gives rise to a new form of circumscription that can be captured in second order logic.

2 Reasonable States of Belief

We now look at the question of what are the reasonable epistemic states, given that we have some facts we consider true, and some ordering on states of the world that represents likelihood. We consider several conditions that we claim any reasonable epistemic state should obey. We first formally define epistemic state, and state of the world to avoid misunderstandings.

Definition 1 We assume a fixed underlying first order language L. An epistemic state is a class of Lstructures. A state of the world is an L-structure.

The first possible criterion we consider is that any belief we have should not exclude a state of the world, if we believe that it is possible, and there is no other state that is more likely. Thus the structures that are minimal in our ordering should always be included in reasonable states of belief. The following propositions will all delimit the reasonable beliefs with respect to a partial ordering ≤, and a class of possible states of the world/models A.

Criterion 1 (Minimal) Given a notion of ≤ on states of the world, and a class of states of the world A that are possible, the reasonable epistemic states include all minimal states of A with respect to ≤.

It also seems reasonable that, given a particular model 𝔐 there should be at least one model in our final class, that is as likely as 𝔐. This is not implied by our previous consideration, as if we have an infinite descending chain, without a limit, then there is no minimal element. This new consideration would say that, in this case, we would include some model, below each particular model in the chain.

These two principles can be expressed formally by saying that the set of models we select out, should be a dense.

Definition 2 A class of objects M, is dense, with respect to a partial order ≤, over a class of objects, N, exactly when for each object x in N, there is an object y in M less than or equal to x.

∀x ∈ N∃y ∈ M.y ≤ x

Given a class of models, A, and a partial-order ≤ on A, then the class of models we select should be dense with respect to ≤. This is the second criterion on states of belief that we propose. However, it subsumes the first criterion.

Criterion 2 (Dense) Given a notion of ≤ on states of the world, and a class of states of the world A that are possible, the reasonable epistemic states should be dense in A with respect to ≤.

Proposition 3 Criterion 2 implies Criterion 1.

Proof: Consider the minimal objects in the partial-order. By density, there are objects less than or equal to them in the dense class. But the only elements less than or equal to a minimal element is itself. Therefore every dense class contains every minimal element.

Another principle that has some justification is that our class of models should be downwards closed. If a model 𝔄 is in our selected class, then every more likely model should also be in our class. This property can be stated as every acceptable class is a ideal, or downwards closed class. As we are considering partial orders not lattices an ideal is just a downwards closed class—there is not requirement that it be closed under meets. Ideals of partial orders are sometimes called order-ideals or lower sets.

Definition 4 A class M is an ideal of a partial order ≤, over a class N, exactly when M is downwards closed.

∀x ∈ M, y ∈ N.y ≤ x → y ∈ M

Definition 5 The restriction of a partial order ≤ to a class A, is the partial order ≤_{↓A} defined by,

∀x, y.x ≤ y ∧ x ∈ Ay ∈ A ≡ x ≤_{↓A} y.

Criterion 3 (Ideal) Given a notion of ≤ on states of the world, and a class of states of the world A that are possible, the reasonable epistemic states should be an ideal of ≤ restricted to A.

Having looked at these principles, we now consider what the reasonable beliefs of reasoner should be. The characterization we consider is that a reasoner should believe ϕ, is ϕ is true in some reasonable state of belief.

Because of the ambiguity of English we define the set of sentences true in some dense ideal of a partial-order on models more formally.

Definition 6 The set of sentences Φ true in some dense ideal of a partial-order ≤ on a class of models A is defined to be the set:

\{ϕ | \begin{matrix}∃N.∀x ∈ A∀y ∈ N.x ≤ y → x ∈ N∧ \\ ∀x ∈ A∃y ∈ N.y ≤ x ∧ N ⊧ ϕ \end{matrix} \}

We call Φ the reasonable beliefs, given a class of models A and a partial order ≤ on A.

Theorem 7 The class of models of the reasonable beliefs given a class of models A and a partial order ≤ need not be a reasonable epistemic state.

Proof: We imagine that our partial order on beliefs is an infinite descending chain, with no least element. For simplicity we imagine each structure interprets a constant c as a natural number, where 𝔐 ≤ 𝔑 if and only if c^{𝔐} ≤ ≤ ≤ c^{𝔑}, where ≥ ≥ ≥ is greater than or equal on the naturals. Here the class of models of the reasonable beliefs is not dense. Its only models have a non-standard interpretation of c, and no model in A has a non-standard interpretation of c.

This theorem may seem damning, but things are not as bad as they may now seem. The notion of reasonable beliefs still has nice properties.

We now question whether this notion of reasonable beliefs has certain consistency properties. We first note that as our logic is first order then the set of sentences true in some dense ideal of a partial-order is guaranteed to be logically closed, and consistent.

We first show that the intersection of two dense ideals is a dense ideal.

Lemma 8 The intersection of two dense ideals is a dense ideal.

Proof: We need to show that the intersection of two dense ideals, I_{1} and I_{2}, is dense, and an ideal. The intersection of two downwards closed classes is downwards closed. Finally, the intersection of two dense ideals is a dense ideal by the following argument. For each object y, there is an object x in I_{1} below y by density. Also by density there is an object z in the ideal I_{2} below x. This z is in the first ideal I_{1}, as the ideal is downwards closed. Thus z is in the intersection of I_{1} and I_{2}. We have thus shown that there is an object in the intersection below every object, as needed.

Theorem 9 For a first order language L and a non-empty class of L-structures A, and a partial order on A, ≤, there is a non-empty class of models, B that is the theory of the sentences true in some dense ideal of ≤.

Proof: We first show that the set of sentences true in some dense ideals is logically closed. Let Γ be the set of sentences true in some dense ideal. Let ϕ be a logical consequence of Γ. Then, by the compactness of first order logic, there is a finite subset Γ′ = {γ_{1}, …, γ_{n}}, of Γ such that Γ′ ⊧ ϕ. Let a dense ideal that entails γ_{i} be denoted I_{i}. These exist as every element of Γ was true in some dense ideal. Then, by the above Lemma, the intersection I′ = ⋂_{i≤n} I_{i} is a dense ideal. Further, every γ_{i} ∈ Γ′ is true in I′. This follows, as truth in a class of models is preserved by intersection. Thus, ϕ is true in I′, and thus it is in Γ, as Γ is the set of all sentences true in some dense ideal. Thus the set Γ is closed under logical consequence.

We now show that Γ is consistent. Suppose that Γ was not consistent, then, as it is logically closed, it would contain ⊥. Then there would be a dense ideal that entailed ⊥. But the only ideal that entails ⊥ is the empty ideal, which is not dense. Thus Γ is consistent, and hence its class of models is non-empty, as required.

Definition 10 A consequence relation |∼ is a binary relation on sets of formula and formulas.

We say that a consequence relation is consistency preserving if every satisfiable theory is mapped to a satisfiable theory.

Definition 11 A consequence relation Γ |∼ γ is consistency preserving exactly when, if Γ is consistent, then the set of γ, such that Γ |∼ γ, is consistent.

Theorem 12 Ideal entailment is consistency preserving.

Proof: This follows the analysis of Theorem 9.

We have now shown that our notion of reasonable beliefs does not map satisfiable sets of first order sentences to contradiction.

As next consideration we ask does the derived entailment relation obey the structural rules suggested by Gabbay(1985), and the rule Or suggested by Kraus, Lehmann and Magidor(1990). Kraus et al. considered compact consequence relations, and thus considered a binary relation on sentences, α |∼ β. We generalize their rules so that |∼ takes a set of formulas and a formula as arguments. In the following ⊧ denotes first order entailment, Γ and Δ sets of first order formulas, and γ, δ, α, β first order formulas.

Definition 13 A consequence relation |∼ over a language L is said to be preferential if and only if it contains all instances of the following Reflexivity axiom ID and is closed under the inference rules of Left Logical Equivalence LLE, Right Weakening RW, Cut Cut, Cautious Monotonicity CM, and Or.

(ID) Γ, α |∼ α
(LLE) \frac{Γ ⊧ δ|δ ∈ Δ, Δ ⊧ γ|γ ∈ Γ, Γ |∼ α}{Δ |∼ α}

(RW) \frac{⊧ α → β, Γ |∼ α}{Γ |∼ β}

(Cut) \frac{Γ, δ |∼ γ, Γ |∼ δ}{Γ |∼ γ}

(CM) \frac{Γ |∼ β, Γ |∼ γ}{Γ, β |∼ γ}

(Or) \frac{Δ |∼ α, γ |∼ α}{\{δ ∨ γ|δ ∈ Δ\} |∼ α}

We call this system P for preferential.

The rule Or differs from the rule proposed by Kraus et al. in that they insisted that both Δ and γ be formulas, while we allow Δ, though not γ to be a set of formulas.

Definition 14 Let ≤ be a partial order on L-structures. We say a set of sentences Γ in L ideally entails, under ≤, a sentence α if α is in the reasonable beliefs of the models of Γ under ≤.

This defines a consequence relation. That is, a binary relation between sets of sentences in L and sentences in L.

Theorem 15 Ideal entailment, over a first order language, is a preferential consequence relation.

Proof: We need to check each rule. Let ∥Γ∥ denote the models of Γ. Let an dense ideal of ∥Γ∥ be understood to be an dense ideal of ∥Γ∥ relative to some fixed order ≤.

ID is immediate, as every α state models α, and the α states are a subset of the Γ, α states.

LLE is immediate as if Γ ⊧ Δ and Δ ⊧ Γ then the Δ states are exactly the Γ states. RW is true as satisfaction on a set of states is defined classically. Cut We need to show that if a dense ideal I of ∥Γ, δ∥ models γ, and a dense ideal I′ of

∥Γ∥ models δ, then there is a dense ideal I_{1} of ∥Γ∥ that models γ. We can choose I′ ⊃ I as density and ideality are preserved under subsets. We claim that I ∩ I′ is the necessary dense ideal of ∥Γ∥. It is an ideal, as intersection preserves downwards closedness. We need to show that it is an ideal. We consider a models 𝔄 of Γ, we show that there is a model below it in I ∩ I′. As I′ is dense in ∥Γ∥ there is a model 𝔅 ∈ I′. Further, as Γ |∼ δ, 𝔅 ⊧ δ. Thus 𝔅 ∈ ∥Γ, δ∥. But as I is a dense ideal of ∥Γ, δ∥, there is a model ℭ ∈ I below 𝔅 that models γ. This is also in I′ as I′ is downwards closed, and I′ ⊃ I. Therefore ℭ is our needed witness of density.

Finally we need to show that I ∩ I′ ⊧ γ. This follows as I models γ.

CM We need to show that if a dense ideal I of ∥Γ∥ models γ, and a dense ideal I′ of ∥Γ∥ models δ, then there is a dense ideal I_{1} of ∥Γ, δ∥ that models γ.

This follows as a dense ideal I of a given class ∥Γ∥ , restricted to a subset of the class ∥Γ, δ∥ is a dense ideal of the class ∥Γ, δ∥.

Or We need to show that if a dense ideal I of ∥γ∥ models α, and a dense ideal I′ of ∥Δ∥ models α, then there is a dense ideal I_{1} of ∥{δ ∨ γ|δ ∈ Δ}∥ that models α.

We consider the union of the two dense ideals. This set I ∪ I′ is downwards closed, and models α. Thus we need just show that it is dense in ∥{δ ∨ γ|δ ∈ Δ}∥. Consider a model of {δ ∨ γ|δ ∈ Δ}, call it 𝔄. Either 𝔄 is a model of γ, in which case, as I is dense in ∥γ∥, we can find a 𝔅 ≤ 𝔄 in the set I and hence in I ∪ I′, or 𝔄 is a model of Δ, in which case, as I is dense in ∥Δ∥, we can find a 𝔅 ≤ 𝔄 in the set I′ and hence in I ∪ I′. Thus in both cases, I ∪ I′ is dense, as required.

We now show that when enough minimal models exist, our new semantics agrees with minimal entailment.

Proposition 16 For a given class of models A, and a partial order ≤ on A, if for every model 𝔄 there is a minimal model 𝔅 such that 𝔅 ≤ 𝔄, then the theory of the minimal models of A is the reasonable beliefs of A under ≤.

Proof:

⇒: By the assumption, there is a minimal model below every model, therefore the minimal models are a dense ideal. Therefore, each sentence ϕ in the theory of the minimal models is a reasonable belief, as the models of ϕ contain a dense ideal, as the models of ϕ are a superset of the models of the theory of the minimal models of A.

⇐: Consider any reasonable belief ϕ, we show that it is true in all minimal models. ϕ is true in a dense ideal, therefore it is true in every minimal model, as every dense ideal contains all minimal elements.

Thus we have an entailment relation that is consistency preserving, and obeys the rules of preferential entailment. We now ask whether is correctly models the examples we considered earlier.

2.1 Examples

In our first example, the models of t_{c} = 1, that is, the models where the computer time is one unit, contains a dense ideal. In fact, the models of our theory of the stock market, that satisfy t_{c} = 1 are a dense ideal in the order generated by preferring models where money is larger. Furthermore, we have avoided the inconsistency, as ideal entailment is consistency preserving.

In our second example we tried to move a block, but minimal entailment led to inconsistency. In this example, the models of our domain that model the statement that we can move the block one unit in the x direction contain a dense ideal. In fact, these models are all the models of our theory, and thus the improper dense ideal.

The third example, rather than presume, as minimal entailment does that the preferred flavor is chocolate, ideal entailment denies this, as the models where chocolate is true do not contain a dense ideal, in particular there is no chocolate model below any given vanilla model.

The second part of the third example would have us infer chocolate. In this case the chocolate models are a dense ideal. The clause that requires us to find a chocolate model below or equal to every given model is supplied by choosing the model with equal smoothness and with chocolate flavor.

It is worth noting that there are linearizations of the partial-order from the e second part of the third example that do not have the property that the chocolate models contain a dense ideal. Consider the linearization that orders all flavors by smoothness. This has alternating chocolate and vanilla models, and thus does not contain a dense ideal.

3 Second Order Characterizations

Now that we have chosen to use ideal entailment as our basis for reformulating circumscription, we recapitulate the changes that we make to the semantics, and then look at possible second order characterizations of these notions.

3.1 Semantics

Our semantics differ from classical circumscription in one important way. We shall consider our final theory to be the sentences that are true in some dense ideal, rather than those true in all (possible non-existent) minimal models.

The justification for the difference from classical circumscription is simple. In the case where there are enough minimal models so that every non-minimal model has a minimal model below it, the two semantics agree, as we showed in proposition 16. Lifschitz (1985) calls this condition well-foundedness, Kraus et al, (1990) call this smoothness. When there is a model that has no minimal model below it then the original semantics are defined in terms of something non-existent, that is, the class of minimal models is the empty class.

We call our new version Cofinal Circumscription. The entailment relation generated by Cofinal Circumscription is the syntactic analogue of ideal entailment. We use ideal entailment for arbitrary preferences on models, and Cofinal entailment etc. for preferences defined by circumscription policies.

3.1.1 Semantics of Cofinal Circumscription

We will define the semantics so that they do not assume minimal models exist. We notice that this formalism has some advantages over regular circumscription, namely it never makes a satisfiable first order theory unsatisfiable.

Let L be a first order language. The objects under consideration, referred to as (circumscriptive) theories, are finite sets of sentences stated in L. We will often view this as a first order sentence (the conjunction of all sentences in the set).

Let A(\overline{P}) be a theory in L, all of whose predicate constants are among \overline{P} = \{P_{1}, …, P_{n}\} and whose functions are f_{1} …, f_{m} n, m ∈ ω, and whose constants are all the constants in some set C. Let Φ = {ϕ_{1}, …, ϕ_{l}} be the minimized formulas, and Ψ = {ψ_{1}, …, ψ_{o}} l, o ∈ ω, be the maximized formulas.

Definition 17 Let 𝔄 and 𝔅 be models of A. We say that 𝔄 is preferred to 𝔅 written 𝔄 ≤_{Φ,Ψ}^{Cofinal} 𝔅, if and only if

1. 𝔄[ϕ] ⊆ 𝔅[ϕ] for every minimized formula ϕ ∈ Φ.

2. 𝔄[ψ] ⊇ 𝔅[ψ] for every maximized formula ψ ∈ Ψ.

We write 𝔄 <_{Φ,Ψ}^{Cofinal} 𝔅 if 𝔄 ≤_{Φ,Ψ}^{Cofinal} 𝔅 and 𝔅 ≰_{Φ,Ψ}^{Cofinal} 𝔄.

Note that this is exactly how preferences are defined in domain formula circumscription (Costello 1996a). The semantics differ on the definition of entailment ⊧_{≤_{Φ,Ψ}^{Cofinal}}.

Definition 18 (⊧_{≤_{Φ,Ψ}^{Cofinal}}) We say a sentence ϕ is entailed by A in this semantics if every model 𝔄 has a model that is smaller or equal to it 𝔅, that satisfies ϕ, and all smaller models than 𝔅 satisfy ϕ.

A ⊧_{≤_{Φ,Ψ}^{Cofinal}} ϕ =^{def} (1)

∀𝔄.(𝔄 ⊧ A) →
∃𝔅.((𝔅 <_{Φ,Ψ}^{Cofinal} 𝔄) ∨ (𝔅 = 𝔄))∧
(𝔅 ⊧ A) ∧ (𝔅 ⊧ ϕ)∧
∀ℭ.((ℭ <_{Φ,Ψ}^{Cofinal} 𝔅) ∧ (ℭ ⊧ A)) → (ℭ ⊧ ϕ)

This states that ϕ is entailed only if every model has a model below it, such that it and everything below it entails ϕ, or the model itself entails ϕ as does every model below it. Thus this can be thought of as saying that if we go sufficiently far down the preference relation, then all the models will entail ϕ.

Lemma 19 The set of first order sentences ϕ such that A ⊧_{≤_{Φ,Ψ}^{Cofinal}} ϕ is the theory of a class of models. We call these sentences the Cofinal sentences.

Proof: The theory of a class of models is a set of sentences closed under logical consequence. This follows as if two sentences are Cofinally entailed, then their conjunction is. Therefore if a set of sentences are Cofinally entailed, then their consequences will be Cofinally entailed.

3.2 Formal System

3.2.1 Motivations

We have given a new semantics to circumscription. Classically circumscription had both a simple semantics and a simple formal system, expressed in second order logic. We here develop a formal system for our new semantics.

We use the language of sorted second order logic in this section.

Definition 20 The relativization of a formula γ with respect to a unary predicate variable ϕ, written γ^{ϕ}, is the result of a syntactic replacement applied to γ which we define inductively as follows.

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

• 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 γ, that is, (γ^{ϕ_{1}})^{ϕ_{2}}.

Definition 21 ((Z, S) <_{Φ,Ψ} (Z′, S′)) Given a sorted second order language L, and two finite sets of formulas in L, Φ = {ϕ_{1}, … , ϕ_{n}}, Ψ = {ψ_{1}, …, ψ_{m}}, we define the following notation:

(Z, S) ≤_{Φ,Ψ} (Z′, S′) ≡

\begin{matrix}∀\overline{x_{1}}.ϕ_{1}^{S}(\overline{x_{1}}) → ϕ_{1}[Z/Z′]^{S′}(\overline{x_{1}}) ∧ … ∧ ∀\overline{x_{n}}.ϕ_{n}^{S}(\overline{x_{n}}) → ϕ_{n}[Z/Z′]^{S′}(\overline{x_{n}})) \\ ∧ ∀\overline{x_{1}}.ψ_{1}^{S′}(\overline{x_{1}}) ← ψ_{1}[Z/Z′]^{S′}(\overline{x_{1}}) ∧ … ∧ ∀\overline{x_{m}}.ψ_{m}^{S}(\overline{x_{m}}) ← ψ_{m}[Z/Z′]^{S′}(\overline{x_{m}})) \end{matrix}

where Z and Z′ are tuples of second and first order variables, of equal length, sort and type, α[Z/Z′] denotes the simultaneous replacement of all occurrences of Zs by Z′s in α, S and S′ are formulas of L with one free variable, and \overline{x_{i}} is a tuple of variables equal in number and sort to the free object variables of ϕ_{i} while \overline{y_{i}} is a tuple of variables equal in number and sort to the free object variables of ψ_{i}.

We define:

\begin{matrix}(Z, S) <_{Φ,Ψ} (Z′, S′) =^{def} \\ (Z, S) ≤_{Φ,Ψ} (Z′, S′) ∧ ¬[(Z′, S′) ≤_{Φ,Ψ} (Z, S)] \end{matrix}

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

Definition 23 (inf) We define inf(L) to be the sentence that states that there are a countable 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}

Definition 24 (Circ_{L}(A; Ψ; Φ)) Given a language L, the circumscription of A minimizing Φ, a finite set of formulas in L, and maximizing, Ψ, a finite set of formulas in L, denoted Circ_{L}(A; Φ; Ψ), is defined to be the following schema with schematic variable ϕ which ranges over first order formulas from L:

inf ∧ A^{U} ∧ [(∀Z S.A^{S}[Z] ∧ Closed(S, Z) →
∃Z′S′.(A^{S′}[Z′] ∧ Closed(S′, Z′) ∧ ϕ^{S′}[Z′]∧
(Z′, S′) <_{Φ,Ψ} (Z, S) ∨ Z, S = Z′, S′
∧(∀Z′′S′′.A^{S′′}[Z′′] ∧ Closed(S′′, Z′′)∧
(Z′′S′′) <_{Φ,Ψ} (Z′S′) → ϕ^{S′′}[Z′′])))
→ ϕ^{U}]

Here Z, S = Z′, S′ representes ∀0\overline{x}.P (\overline{x}) ≡ P′(\overline{x}), for each pair of predicate P and P′ from Z, S and Z′, S′.

Lemma 25 If L = ⟨\overline{P} , \overline{F} , C⟩ is a sorted first order language, and 𝔄 and 𝔅 are L-structures, and A is the set of domains of 𝔄, and 𝔄[P] is the interpretation of P in 𝔄 then

𝔄 ≤_{Φ,Ψ}^{Cofinal} 𝔅 ≡
(𝔄[\overline{P}], 𝔄[\overline{F}], 𝔄[C], A) ≤_{Φ,Ψ} (𝔅[\overline{P}], 𝔅[\overline{F}], 𝔅[C], B).

Proof: We first note that a sequence of domains can be read as a set of sorts, and the interpretations of predicates, functions and objects can be read as an instantiation of a sequence of variables. Thus the second part of the above formula is well formed.

We expand the definitions of ≤_{Φ,Ψ}^{Cofinal} and ≤_{Φ,Ψ} and see that the two notions are equivalent.

Lemma 26 If L = ⟨\overline{P} , \overline{F} , C⟩ is a sorted first order language, and 𝔄 and 𝔅 are L-structures, then if 𝔄 is less than 𝔅 in some partial-order on L-structures ≤_{Φ,Ψ}, then there is an L-structure ℭ elementarily equivalent to 𝔄, whose domain is contained in B ∪ X, where X is a countable new set of objects.

Proof:

We denote the domain of 𝔄 as A etc. We consider the objects B∩A. We construct a model ℭ, such that C ⊆ (B ∩A)∪X, that agrees with 𝔄 over the objects B ∩A, and is elementarily equivalent to 𝔄. This exists, as every substructure of a first order model can be extended to an elementarily embedding by adding a countable number of objects(Chang and Keisler 1990) proposition 2.2.17.

We now notice that this model ℭ is ≤_{Φ,Ψ} 𝔅, as 𝔄 ≤_{Φ,Ψ} 𝔅, and ℭ agrees with 𝔄 on all objects in the intersection of 𝔄 and 𝔅, and the fact that the ≤_{Φ,Ψ} relation is defined in terms of subset inclusion on the objects common to both models.

The author is grateful to Johan van Benthem for suggesting this key Lemma.

Theorem 27 If ϕ is a sentence in a first order language L, and Φ and Ψ are finite sets of formulas in L, and A is a finitely axiomatizable theory in L, then

if A ⊧_{≤_{Φ,Ψ}^{Cofinal}} ϕ then Circ_{L}(A; Φ; Ψ) ⊧ ϕ

Proof:

We assume the opposite and show a contradiction. We know that ϕ is a Cofinal sentence under the partial-order ≤_{Φ,Ψ}^{Cofinal}, but ϕ is not a result of the circumscription of A minimizing Φ and maximizing Ψ.

We instantiate ϕ for the schematic variable ϕ in the circumscription schema. We know that the left-hand side of the last implication is not valid, as our assumption is that the circumscription does not entail ϕ.

As before we see we can safely interpret tuples of predicates and a unary predicate as a model. This is because we are only interested in first order properties, from Lemma 26, we need only consider the models whose universe is a subset of the the domain of the current model and some countable set, in this case the set induced by inf.

We choose a model that makes this sub-formula false. But this sub-formula says that there is a model below every model, with the property that ϕ is true in this model and in all smaller models. If this is not the case, then there is a model, such that every model below it has a model below it that does not satisfy ϕ. But then ϕ is not a Cofinal sentence, a contradiction

Theorem 28 If ϕ is a sentence in a first order language L, and Φ and Ψ are finite sets of formulas in L, and A is a finitely axiomatizable theory in L, then

if Circ_{L}(A; Φ; Ψ) ⊧ ϕ then A ⊧_{≤_{Φ,Ψ}^{Cofinal}} ϕ.

Proof:

We need to show that is ϕ is entailed by the circumscription, then it is a Cofinal sentence. To show it is a Cofinal sentence is suffices to show that its models contain a dense ideal. This dense ideal is witnessed by the circumscription formula. Strictly speaking the circumscription formula only gives us a dense ideal of the partial order restricted to models whose universes differ only on a countable number of objects. However, by Lemma 26 this suffices. The circumscription formula, which implies ϕ states that there is an ideal, that entails ϕ below every model. The union of these ideals is the necessary dense ideal. The union of ideals is an ideal, and by construction is it dense. Thus the models of ϕ contain a dense ideal, and thus ϕ is Cofinally entailed.

We again stress that it is necessary that the circumscription be a schema. If we rewrote it as with a universal second order quantified variable rather than a schematic variable ϕ, we would allow instantiations that were not first order definable. However, second order logic is not compact, and thus Lemma 19 does not apply. In fact cofinal circumscription redefined using second order quantification maps satisfiable theories to unsatisfiable theories.

3.3 Conclusions

We have introduced a new semantics for circumscription. It has one new principal feature— it does not consider the sentences true in the minimal models, rather it looks for sentences whose models contain a dense ideal. This feature is desirable, as it ensures circumscription is consistent.

In summary, the problem that circumscription had—mapping satisfiable theories to unsatisfiable theories—can be seen as a byproduct of defining the semantics in terms of nonexistent minimal models.

The notion of Cofinal sentences is not tied to circumscription. All semantics based on a notion of truth in the most preferred models have natural variants where we consider Cofinal sentences rather than truth in minimal models. It is worth noting that this approach is not immediately applicable to approaches that consider orderings on sets of models rather than models. As assuming minimal models exist is a strong and unnecessary assumption we claim that moving to variants defined in terms of Cofinal sentences is the correct choice.

References

Bossu, G., and P. Siegel. 1984. Saturation, nonmonotonic reasoning, and the closed world assumption. Artificial Intelligence 25(1):13–64.

Chang, C., and H. Keisler. 1990. Model Theory. Vol. 73 of Studies in Logic and the foundations of mathematics. North Holland. third edition edition.

Costello, T. 1996a. Domain Formula Circumscription. under review.

Costello, T. 1996b. The Expressive Power of Circumscription. under review.

Davis, M. 1980. The mathematics of non-monotonic reasoning. Artificial Intelligence 13(1–2):73–80.

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

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

Gelfond, M., V. Lifschitz, and A. Rabinov. 1991. What are the limitations of the situation calculus. In Working Notes: AAAI Spring Symposium Series on the Logical Formalization of Commonsense Reasoning, 59–69.

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

Lewis, D. K. 1973. Counterfactuals. Cambridge, MA.: Harvard University Press.

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

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

McCarthy, J. 1977. Epistemological Problems of Artificial Intelligence. In Proc. Fifth International Joint Conference on Artificial Intelligence (IJCAI ’77), 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.

McCarthy, J., and P. Hayes. 1969. Some Philosophical Problems From the Standpoint of Artificial Intelligence. In D. Michie (Ed.), Machine Intelligence 4, 463–502. Edinburgh, UK: Edinburgh University Press.

Shoham, Y. 1986. Reasoning about Change: Time and Causation from the Standpoint of Artificial Intelligence. PhD thesis, Yale University.