The Expressive Power of Circumscription

Tom Costello

Abstract

Circumscription is a form of non-monotonic reasoning, introduced in [McC77] as a way of characterizing defaults using second order logic. The consequences of circumscription are those formulas true in the minimal models under a pre-order on models. In the case of domain circumscription the pre-order was the sub-model relation. Formula circumscription [McC80, McC86] is characterized by minimizing a set of formulas—one model is preferred to another model when the extensions of the minimized formulas in the first are subsets of the extensions in the second.

We show that the propositional version of formula circumscription can capture all pre-orders on valuations of finite languages. We consider the question of infinite languages, and give the corresponding representation theorems.

1 Introduction

McCarthy’s circumscription [McC77] is the first application of the idea of relative likelihood, or preference between models, to non-monotonic reasoning. There, he recognized that a natural way of representing defaults was to order states of the world, according to what we thought was the case, and then to choose the sentences true in the minimal models in this order as our current beliefs. This has strong links to the notion of inductive definition and to the use of minimality as a definitional tool which is ever-present in mathematics. This basic idea has since been studied by many researchers. The original suggestion was to order models based on the size of their domain, preferring sub-models, analogously to mathematical induction. This was later changed to minimizing the extension of a predicate, and then of an arbitrary formula.

The notion of minimal entailment has been considered by many researchers. It has one of its roots in Ramsey’s [Ram78] definition of counterfactuals,

(Ramsey Test) Accept a propositional of the form “if A then C” in a state of belief K if and only if the minimal change of K needed to accept A also requires accepting C.

Since then the idea of representing counterfactuals using entailment in minimal models has been widely considered [Sta68, Lew73]. Gärdenfors [Gär78, Gär88], and Makinson [GM88] have considered similar themes in their work on belief revision, which has close connections with non-monotonic reasoning [GM94]. Shoham [Sho86] was the first to examine the model theory of McCarthy’s idea of using minimal entailment for non-monotonic reasoning. Since then, this notion of preferential entailment has become linked with approaches [Gab85] based on characterizing non-monotonicity through structural rules.

Despite the large amount of interest the area has attracted, some of the basic questions about circumscription remain unanswered. What is circumscription’s expressive power? How do the various forms of circumscription proposed compare in expressive power? How should the expressive power of non-monotonic systems be measured?

In the next sections we attempt to answer these questions. We first consider the structural meaning of minimizing predicates or formulas. We find that minimizing a formula is equivalent to stating that the models that satisfy that formula are an upper-set of the pre-order on models. Using this idea, it immediately follows that all pre-orders are definable using circumscription in the finite propositional case.

As the expressive power of first order logic with a fixed domain and propositional logic co-incide, this shows that circumscription captures all pre-orders on structures, for first order theories with a fixed domain.

When we look at infinite languages, we see that the circumscription formula can only describe pre-orders that are the product of a finite and a discrete pre-order.

Infinite languages, and infinite sets of minimized formulas can still not capture all preorders—only those pre-orders whose upper-sets have a basis, all of whose elements are finitely axiomatizable. Even if we minimize a countable set of infinitary formulas, we still cannot capture all pre-orders.

2 Notation

In this section we recap some notation we need concerning orders.

Definition 1 (pre-order) A pre-order, ≤, on a domain D, is a binary relation that is transitive and reflexive. We denote a pre-order on D, as ≤_{D}, we drop the subscript when the domain is obvious.

∀d d′ d′′ ∈ D.d ≤ d′ and d′ ≤ d′′ implies d ≤ d′′ (transitivity)
∀d ∈ D.d ≤ d (reflexivity)

Definition 2 (partial order) A partial order on a domain D is a pre-order that is anti-symmetric. We denote a partial order on D, as ≦_{D}, we drop the subscript when the domain is obvious.

∀d d′ ∈ D.d′ ≦ d and d ≦ d′ implies d = d′ (anti-symmetry)

The discrete partial order on D is the identity on D. We say a pre-order is finite when its domain is finite.

Definition 3 (Upper-set) An upper-set F of a pre-order ≤ on a domain D is a subset of D that is upwards closed, that is

∀d ∈ F, d′ ∈ D.d ≤ d′ implies d′ ∈ F

Upper-Sets are sometimes called order-filters.

Proposition 1 The family of all upper-sets of a pre-order ≤_{D} is closed under arbitrary unions and intersections.

Proposition 2 Every set of sets X is closed under arbitrary unions and intersections is the family of upper-sets of a unique pre-order ≤.

Definition 4 (basis) A basis B for F, a family of upper-sets of a pre-order ≤, is a subset of F, such that every element of F is definable in terms of the intersection and union of elements of B.

∀f ∈ F.∃b_{1,1}, ….b_{n,m} ∈ B. ⋃_{i=1}^{n} ⋂_{j=1}^{m} b_{i,j} = f

Definition 5 (minimal) An element d is said to be a minimal element in an order ≤, on a domain D, if there is no element d′ ∈ D such that d′ ≤ d and d ≰ d′.

Minimal_{≤}(d) ≡ d ∈ D ∧ ∀d′ ∈ D.d′ ≤ d → d ≤ d′

Definition 6 (restriction) The restriction of a pre-order ≤_{D}, to a subset D′ of D, is written, ≤_{↓D′}.

3 The Model Theory of Circumscription

In this section we look at a commonly used form of circumscription. This version includes the modifications introduced by Lifschitz [Lif85] in his reformulation of formula circumscription [McC86]. It also uses the device, introduced by deKleer and Konolige [dKK89], of fixing predicates by minimizing both the predicate and its negation. We define formula circumscription and its semantics in the propositional case. We then look at some of the properties of the pre-orders defined by circumscription. We see that they are not always partial orders, and that in the case of finite languages, minimal valuations always exist.

We then see that the formulas true in the minimal models of this pre-order on models are exactly the consequences of circumscription. We then consider the question of what preorders circumscription can capture. As our first step towards this we look at how minimized formulas are related to the pre-order on models they generate. We see that the set of models of each minimized formula is an upper-set of the pre-order on models. We next show that the pre-order is the unique pre-order that has these upper-sets as a basis. This establishes the basic representation result for circumscription—every pre-order of the valuations of a finite propositional language can be captured by a circumscription policy.

We then show the restriction to finite languages is necessary.

3.1 Propositional Formula Circumscription

McCarthy [McC86] introduced a form of circumscription, called formula circumscription. It extends predicate circumscription [McC80] 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 [McC80].

Definition 7 (≤ on formulas) It is useful to introduce the notation γ_{1}, γ_{2} ≤ δ_{1}, δ_{2} for the formula (γ_{1} → δ_{1}) ∧ (γ_{2} → δ_{2}).

Definition 8 (McCarthy [McC86]) If γ_{1}, γ_{2} is a pair^{1} of formulas from a propositional language L, and P_{1}, …, P_{n} are the propositional letters in our language L, then we define the circumscription of α, a formula in L minimizing γ_{1}, γ_{2}, written Circ(α; γ_{1}, γ_{2}) as follows.

We use α′ to denote the formula, α[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}], that is the result of the replacement of the propositional letters P_{i} in α by the propositional variables ψ_{i}.

α ∧ ∀ψ_{1}, …, ψ_{n}. [α′ ∧ γ′_{1}, γ′_{2} ≤ γ_{1}, γ_{2}] → γ_{1}, γ_{2} ≤ γ′_{1}, γ′_{2}

We use the notation Circ_{L\overline{P}} when we wish to stress that the propositional letters in the language are the set \overline{P}. This may differ from the letters that occur in α.

1For notational simplicity we minimize two formulas, the extension to more formulas is the natural one.

3.2 Semantics of Propositional Circumscription

Definition 9 (≤^{Γ}) Given a propositional language L\overline{P} and a set of formulas Γ from L\overline{P}, we define the relation ≤^{Γ} on the valuations of L\overline{P} as follows.

We denote the truth value of a formula γ in a valuation 𝔄 as 𝔄[γ]. For any two valuations 𝔄, 𝔅, we write 𝔄 ≤^{Γ} 𝔅 if

• 𝔄[γ] = 1 implies 𝔅[γ] = 1 for every γ in Γ.

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

Proposition 3 For a given propositional language L\overline{P}, and a set of formulas Γ from L\overline{P}, ≤^{Γ} is a pre-order but not always a partial order.

Proof: That ≤^{Γ} is a pre-order follows from the transitivity and reflexivity of implication.

To show transitivity we assume that 𝔄 ≤ 𝔅 and 𝔅 ≤ ℭ and show that this implies that 𝔄 ≤ ℭ.

To show that 𝔄 ≤ ℭ, it suffices to show that for each γ ∈ Γ, if 𝔄[γ] = 1, then ℭ[γ] = 1. Thus we assume that 𝔄[γ] = 1 and show this implies ℭ[γ] = 1.

As 𝔄 ≤ 𝔅, then

𝔄[γ] = 1 implies 𝔅[γ] = 1.

Therefore, 𝔅[γ] = 1. But, also, as 𝔅 ≤ ℭ, then ℭ[γ] = 1, as required.

To show reflexivity, it is sufficient to show that if 𝔄[γ] = 1 then 𝔄[γ] = 1, which is immediate. To see that it is not always a partial order, let Γ be {P }, the language be L_{{P,Q}}. Then

the two valuations 𝔄, and 𝔅, where 𝔄[P] = 0, 𝔄[Q] = 0, 𝔅[P] = 0, 𝔅[Q] = 1, provide a counterexample to anti-symmetry.

As we considered earlier there are minimal elements in many pre-orders. Thus we can define the minimal models of a theory with respect to ≤^{Γ}.

Proposition 4 Let α be a formula of L\overline{P}, and Γ a finite set of formulas of L\overline{P}.

A valuation 𝔄 for a finite set of propositional letters \overline{P} is a model of Circ_{L\overline{P}} (α; Γ), if and only if 𝔄 is minimal in the set of models of α with respect to ≤^{Γ}.

Proof:

We show the two propositions are inter-derivable. We first note that both propositions imply that 𝔄 is a model of α. We then show the second conjuncts of both are inter-derivable.

Minimal_{≤^{Γ}↓_{{ℭ|ℭ⊧α}}}𝔄 ≡
∀𝔅.𝔅 ⊧ α ∧ (𝔅 ≤^{Γ} 𝔄) → (𝔄 ≤^{Γ} 𝔅) ≡
∀𝔅.𝔅 ⊧ α ∧ (∀γ ∈ Γ.𝔅[γ] → 𝔄[γ]) → (∀γ ∈ Γ.𝔄[γ] → 𝔅[γ]) ≡
∀ψ_{1}, …, ψ_{n}.α[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}]∧
γ_{1}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}], …, γ_{n}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}] ≤ γ_{1}, …, γ_{n} →
γ_{1}, …, γ_{n} ≤ γ_{1}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}], …, γ_{n}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}]

The first equivalence follows from the definition of Minimal. The second follows from the definition of ≤^{Γ}. The third equivalence is valid as a model can be viewed as a valuation function, and from the definition of satisfiability. Note this requires that there be only a finite number of propositional letters. The last formula is the second conjunct in the definition of circumscription.

Thus we have shown that minimal entailment over pre-orders on valuations describe circumscription. The next obvious question is what pre-orders can circumscription capture?

3.3 Characterization of Minimized Formulas

We begin by relating the minimized formulas to properties of the pre-order,

Proposition 5 Given a set Γ of formulas from a propositional language L\overline{P}, the set of models of each γ ∈ Γ is an upper-set of the pre-order ≤^{Γ}.

Proof: We need to show that the models of γ are upward closed. Let Γ be a set of formulas of a propositional language. Let γ be an element of Γ. Let 𝔄 be a model of γ, and let 𝔅 be a valuation such that 𝔄 ≤^{Γ} 𝔅. We show that 𝔅 ⊧ γ. As 𝔄 ≤^{Γ} 𝔅 we have 𝔄[γ] = 1 implies 𝔅[γ] = 1 for every γ in Γ. We have 𝔄 ⊧ γ, by assumption. Therefore 𝔅 ⊧ γ as required.

This gives a structural interpretation of minimizing a formula. The set of models of a minimized formula is an upper-set of the pre-order on valuations.

We now show that the pre-order ≤^{Γ} is the pre-order with the fewest upper-sets that contains all the upper-sets in Γ.

Proposition 6 Given a set Γ of formulas of a propositional language L\overline{P} the pre-order ≤^{Γ} is the unique preorder whose upper-sets include the models of each formula in Γ and whose set of upper-sets is minimal.

Proof: We know that every formula in Γ generates an upper-set of ≤^{Γ}. We further know that arbitrary unions and intersections of upper-sets are upper-sets by Proposition 1. We consider the set of sets of models M, whose elements are the set of models of each element of Γ. We close out M under arbitrary unions and intersections, to get M′. M′ is a set of upper-sets, as M′ is closed under unions and intersections, by Proposition 2. M′ is minimal as any smaller set would deny that every set in M was an upper-set. As every set of sets closed under unions and intersection corresponds to a unique pre-order, M′ corresponds to a unique pre-order. M′ includes the models of each formula in Γ by construction.

Thus we need to show that this M′ is the set of upper-sets of ≤_{Γ}. We show every element of M′ is an upper-set of ≤_{Γ}. Every element of M′ is definable in terms of union and intersection from element of M, which are upper-sets of Γ. Thus, by Proposition 1, every element of M′ is an upper-set of ≤_{Γ}.

Finally we show that every upper-set of ≤_{Γ} is an element of M′. We consider an arbitrary upper-set F of ≤_{Γ}. We can divide F into disjoint sets F_{Δ}, each of which satisfy a different subset Δ of Γ. If there is a model 𝔄 ∈ F such that for γ ∈ Γ, 𝔄 ⊧ γ if and only if γ ∈ Δ, then every 𝔅, such that γ ∈ Γ, 𝔅 ⊧ γ if γ ∈ Δ, is in F, as F is upwards closed, and 𝔅 ≤_{Γ} 𝔄, by the definition of ≤_{Γ}. The set of all 𝔅’s such that 𝔅 ⊧ γ if γ ∈ Δ is the intersection of the sets, {ℭ|ℭ ⊧ δ}. Each of these sets {ℭ|ℭ ⊧ δ} is an upper-set.

Thus if F contains 𝔄, such that for γ ∈ Γ, 𝔄 ⊧ γ if and only if γ ∈ Δ, then F contains the intersections of the upper-sets {ℭ|ℭ ⊧ δ} for each δ ∈ Δ. We call this intersection, F′_{Δ}. We will need the fact that F_{Δ} ⊃ F′_{Δ}, which follows from the definition of F′_{Δ}.

Further, as F is the union of the F_{Δ}’s, and each F_{Δ} is contained in the respective F′_{Δ}’s, which are in turn contained in F, then F is the union of the F′_{Δ}’s. Thus F is the union of intersections of upper-sets from M, as every {ℭ|ℭ ⊧ δ} for δ ∈ Δ is an element of M, as Δ ⊂ Γ. Thus every upper-set of ≤_{Γ} is an element of M′.

We now use the fact that every pre-order is uniquely defined by its set of upper-sets, to show that every pre-order on the valuations of a finite propositional language is defined by some ≤^{Γ}.

Theorem 7 If ≤ is a pre-order on the valuations of a finite propositional language L\overline{P}, then there is a finite set of formulas Γ, such that ≤ = ≤^{Γ}.

Proof: Let Γ′ be the set of all formulas whose models are upper-sets of ≤. We know there are only a finite number of logically inequivalent formulas as, by assumption, our language is finite. We now form a set Γ by choosing one formula from each set of logically equivalent formulas in Γ′. This set contains all formulas whose set of models are upper-sets, and is finite, thus it generates the unique pre-order which has exactly those upper-sets, by Proposition 6.

This shows that circumscription can capture all pre-orders on finite propositional languages.

3.4 First Order Finite Domains

In Artificial Intelligence the case where we need only consider theories with domains smaller than a fixed size is often useful. For these structures the results for propositional languages with finite number of letters apply, by considering the well-known translation of fixed finite domain theories into propositional logic.

Thus for fixed finite domain theories, formula circumscription can capture all pre-orders on structures. For the case where our theories have infinite models results are more difficult to come by. We no longer have categoricity, that is, we cannot specify a model up to isomorphism by a formula, or even a set of formulas. In our previous construction 7, we explicitly use the fact that every upper-set of the pre-order on models is axiomatized by a single formula.

3.5 Infinitary Cases

Note that the restriction to finite propositional languages was necessary in the previous theorem. We give an example.

Example 1 Let L be the propositional language containing the propositional letters P_{1}, …, P_{n}, …, n ∈ ω. Consider the following pre-order ≤_{1} on L-valuations. Let one equivalence class S be the set of valuations where exactly one propositional letter is true. Let the other class \overline{S} be the complement of this class. Let all elements of S be greater than every element of \overline{S}.

There is no formula γ that is satisfied only in S. Let us suppose that there was. Choose a valuation that agrees with a valuation in S on all letters that are mentioned in the formula γ, but which is not in S. This valuation satisfies γ, and is not in γ, thus there is no formula γ that is satisfied only in S.

Thus for this pre-order, the set of non-empty, non-trivial upper-sets that are represented by formulas is empty. However, the empty set of formulas is also a basis for the discrete pre-order, the identity on the domain.

Thus, there is no set of formulas Γ, such that ≤_{Γ}=≤_{1}. Any possible set of formulas Γ must contain only formulas whose sets of models are upper-sets of ≤_{1}, by Proposition 5. But the only formulas that are upper-sets of ≤_{1} are tautologies and the negations of tautologies. Thus, Γ must be a set of tautologies and the negations of tautologies. But then ≤_{Γ} is the discrete pre-order, not ≤_{1} which shows that there is no set of formulas Γ, such that ≤_{Γ}=≤_{1}.

We can achieve an analogue of Theorem 7 for the infinite case, if we allow Γ to be infinite. For this analogue we need to add a restriction that certain upper-sets are finitely axiomatizable. This is necessary as shown above.

Theorem 8 If ≤ is a pre-order of the valuations of a propositional language L\overline{P} then there is a set of formulas Γ, such that ≤ = ≤^{Γ} if and only if there is a basis for the upper-sets of ≤ where each element in the basis is finitely axiomatizable.

Proof: ⇐: We take the axiomatizations of the finitely axiomatizable upper-sets as our set Γ. By Proposition 6 the pre-order ≤^{Γ} is the unique pre-order whose upper-sets include the models of each formula in Γ and whose set of upper-sets is minimal. Thus given a set of formulas Γ, that axiomatize a basis for a set of upper-sets, ≤_{Γ} generates the pre-order with that set of uppersets. As there is a finitely axiomatizable basis for the upper-sets of ≤, the finitely axiomatizable upper-sets of ≤ ( which are axiomatized by Γ) form a basis, and thus ≤_{Γ}=≤.

⇒: We prove the contrapositive.

Suppose there is no basis, all of whose members are finitely axiomatizable. Then consider all finitely axiomatizable upper-sets. Let these be Γ′. Then our assumption is that there is an upper-set F, that is not definable in terms of the elements of unions and intersection of elements of Γ′.

Every pre-order ≤^{Γ} with Γ ⊂ Γ′ does not contain F, and thus is not equal to ≤. Every preorder ≤^{Γ} with Γ ⊋ Γ′ contains an upper-set axiomatized by some γ that is not in Γ′. Therefore, ≤^{Γ} has some new γ, whose set of models is an upper-set. However, this new γ is finitely axiomatizable, and thus its set of models is not an upper-set of ≤, as all finitely axiomatizable upper-sets are elements of Γ′, by assumption. Thus ≤^{Γ} contains an extra upper-set and is not equal to ≤, as required.

This gives us a characterization of what minimizing infinite sets of formulas can capture. It is notable that the condition that there is a basis which is finitely axiomatizable is a weaker condition that every upper-set being finitely axiomatizable.

3.6 Finite Strings of Quantifiers

In the above theorem we allow Γ to be infinite. If we wish to capture exactly what a circumscription formula can represent, we need to look at the case where Γ is finite, and where the number of universally quantified propositional variables in the circumscription formula is finite.

We now give a representation theorem for circumscription. We characterize exactly those pre-orders that propositional formula circumscription can define. They are the pre-orders that can be factored into a finite pre-order and a discrete, or unconnected, pre-order. We first make the notion of the product of pre-orders precise and then state the result.

Definition 10 Given a pre-order ≤_{D} and a pre-order ≤_{D′} the pre-order ≤_{D×D′}=≤_{D} × ≤_{D′} is defined over all pairs ⟨d, d′⟩d ∈ Dd′ ∈ D′, such that:

∀d_{1}, d_{2}, d′_{1}, d′_{2}. d_{1} ≤_{D} d_{2} ∧ d′_{1} ≤_{D′} d′_{2} ≡ ⟨d_{1}, d′_{1}⟩ ≤_{D×D′} ⟨d_{2}, d′_{2}⟩

Lemma 9 If ≤ is a pre-order on valuations of a language L\overline{P}, and ≤′ is a pre-order on valuations of a language L\overline{P′} where \overline{P} and \overline{P′} are disjoint then ≤ × ≤′ is isomorphic to a pre-order on valuations of a language L_{\overline{P} ∪\overline{P′}}.

Proof: We consider the pair of valuations to be a single valuation over the union of the propositional letters. This is then a pre-order on valuations of L_{\overline{P} ∪\overline{P′}}.

We now define a pre-order ≤^{Γ;\overline{P′}} that betters captures the notion that the number of universally quantified variables in the circumscription formula is finite. \overline{P′} is a finite subset of the letters in the propositional language and corresponds to the letters replaced by variables in the circumscription formula. These can alternately be considered to the the letters that are varied (in the sense of [McC86]) in the minimization process.

Definition 11 ( ≤^{Γ;\overline{P′}}) Given a propositional language L\overline{P} and a finite set of formulas Γ in L\overline{P} and a finite set \overline{P′} ⊂ \overline{P}, we define the relation ≤^{Γ;\overline{P′}} on the valuations of L\overline{P} as follows. For any two valuations 𝔄, 𝔅 on \overline{P}, we write 𝔄 ≤^{Γ;\overline{P′}} 𝔅 if

• 𝔄[γ] = 1 implies 𝔅[γ] = 1 for every γ in Γ.

• 𝔄[P_{i}] = 𝔅[P_{i}] for every P_{i} such that P_{i} ∈ \overline{P} and P_{i} ∉ \overline{P′}

Here we give the representation theorem for propositional formula circumscription over propositional languages with infinite sets of propositional letters.

Theorem 10 If ≤ is a pre-order on the valuations of a propositional language L\overline{P} then there is a set of formulas Γ from L\overline{P′} and a finite subset \overline{P′} of \overline{P}, such that ≤ = ≤^{Γ;\overline{P′}} if and only if there are pre-orders ≤_{f} and ≤_{d} on valuations of disjoint subsets of \overline{P} where ≤_{f} is finite and ≤_{d} is discrete and ≤ ≅ (≤_{f} × ≤_{d}).

Proof: ⇒: Let the two disjoint subsets of \overline{P} be \overline{P′} and \overline{P} − \overline{P′}.

Let valuations on \overline{P′} be ordered by ≤^{Γ}, this will be ≤_{f}. It is finite, as \overline{P′} is finite. Let ≤_{d} be the identity on valuations on \overline{P} − \overline{P′}. This is a discrete order.

We now need to show that the product of these pre-orders is the required ≤. We consider two valuations 𝔄 and 𝔅 ordered by ≤. We show that they are ordered by ≤_{f} × ≤_{d}. By definition if 𝔄 and 𝔅 are ordered, then they agree on all letters in \overline{P} − \overline{P′}. Thus, the restrictions of 𝔄 and 𝔅 to the letters in \overline{P} − \overline{P′} are ordered by ≤_{d}. Similarly if 𝔄 and 𝔅 are ordered, then by the second clause in the definition of ≤, their restriction to \overline{P′} are ordered by ≤_{f}.

If 𝔄 and 𝔅 not ordered by ≤, a similar case analysis show that they either disagree on the valuations of the letters in \overline{P} − \overline{P′}, and are not ordered by ≤_{d}, or their restrictions to \overline{P′} are not ordered by ≤_{f}. Therefore, ≤_{d} × ≤_{f} ≅≤, as required.

⇐: We are given ≤_{f} and ≤_{d}. Take Γ to be a finite set of formulas such that ≤_{f}=≤^{Γ}. This exists by our earlier theorem. Let \overline{P′}, be the disjoint subset of \overline{P} that is ordered by ≤_{f}.

We now need to show that ≤^{Γ;\overline{P′}}=≤. This follows from Lemma 9, and the fact that ≤_{f}=≤^{Γ}, and that ≤^{Γ;\overline{P′}} restricted to letters outside \overline{P} is the identity on valuations.

Thus we have shown that our propositional formula circumscription captures all pre-orders of a certain general class. Pre-orders over models have been proposed as a general semantic framework for non-monotonic reasoning. Thus we have shown that circumscription captures this notion of non-monotonic reasoning.

3.7 Infinite Strings of Quantifiers

In the last two theorems we saw that circumscription’s ability to define pre-orders was impaired by the finite nature of the the circumscription formula. It is possible to consider languages with infinitary connectives. Chapter 2 of [Cos97] considers the propositional languages L_{ω_{1}}, which allow countable conjunctions and disjunctions of formulas. These languages shed light on the treatment of the first order case. A countable conjunction can be viewed as a universal quantifier over a fixed domain. As circumscription only compares models which have the same domain, this notion seems appropriate.

A direct investigation of the first order case seems difficult at this time, because of the difficulties that circumscription has in characterizing defaults about equality or the domain [EMR85]. Neither domain closure, nor the unique names assumption are naturally captured in formula circumscription. Modifications to circumscription [RWM94, Lif95] that do capture these defaults have been proposed, but are significantly more complicated to analyze.

Comparison to other approaches is also made difficult by the lack of a compelling treatment of the first order case in non-monotonic consequence relations. Circumscription has a well developed treatment of the first order case of non-monotonic reasoning. Current proposals for first order reasoning with consequence relations are much less developed, and are highly nontrivial [LM90]. In particular many do not accept a Barcan like rule—rather there are competing proposals, some of which order domain objects [Bra96], while other order structures [Del88].

The disadvantages of infinitary languages of this kind are that they do not have a complete proof system in the absence of infinitary proof rules.

Not every pre-order is captured by a circumscription policy even if we allow infinitary logics and restrict ourselves to countable languages.

Theorem 11 (Theorem 15, [Cos97]) There exists pre-orders ≤ on valuations of a countable propositional language L\overline{P}, that are not equal to any pre-order of the form ≤^{Γ}, where Γ is a countable set of formulas from L_{ω_{1},\overline{P}}.

4 Conclusion

We have shown that minimizing a certain formula γ corresponds to stating that, in minimal models semantics, the set of models that satisfy γ is an upper-set of the pre-order on models. We show that all finite pre-orders on models are representable by formula circumscription. We show how the result extends to the infinite case, both in terms of languages and in terms of infinitary connectives and strings of quantifiers.

We have explained what the meaning of minimizing a formula is, in terms of the model theory of circumscription. This greatly clarifies why we minimize certain formulas, and make finding a circumscription policy for a particular pre-order trivial. The correct formulas to minimize are those that correspond to a basis for the family of upper-sets. This paper does not suggest using this connection to implement non-monotonic reasoning. Rather the paper is an investigation into the theory of a particular form of non-monotonic reasoning, so that its strengths and weaknesses can be better understood.

References

[Bra96] R. Brafman. “Statistical” First Order Conditionals. In L.C. Aiello, J. Doyle, and S. Shapiro, editors, Principles of Knowledge Representation and Reasoning, Proc. Fifth International Conference, pages 421–431. Morgan Kaufmann, 1996.

[Cos97] Tom Costello. Non-monotonicity and Change. PhD thesis, Stanford University, 1997.

[Del88] J. P. Delgrande. An Approach to Default Reasoning based on a first-order conditional Logic. Artificial Intelligence, 36(1):63–90, 1988.

[dKK89] J. de Kleer and K. Konolige. Eliminating the Fixed Predicates from a Circumscription. Artificial Intelligence, 39:391–398, 1989.

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

[Gab85] D. Gabbay. Theoretical Foundations for Non-Monotonic Reasoning in Expert- Systems. In K. R. Apt, editor, Logics and Models of Concurrent systems, pages 439–458. Springer Verlag, 1985.

[Gär78] P. Gärdenfors. Conditionals and changes of belief. Acta Philos. Fennica, 30:381–404, 1978.

[Gär88] P. Gärdenfors. Knowledge in Flux. Cambridge University Press, Cambridge, UK, 1988.

[GM88] P. Gärdenfors and D. Makinson. Revisions of knowledge systems using epistemic entrenchment. In Moshe Y. Vardi, editor, Proceedings of the Second Conference on Theoretical Aspects of Reasoning About Knowledge, pages 83–95, Monterey, California, March 1988. Morgan Kaufmann.

[GM94] P. Gärdenfors and D. Makinson. Nonmonotonic inference based on expectations. Artificial Intelligence, 65(2):197–245, Jan 1994.

[Lew73] D. K. Lewis. Counterfactuals. Harvard University Press, Cambridge, MA., 1973.

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

[Lif95] V. Lifschitz. Nested abnormality theories. Artificial Intelligence, 74:351–365, 1995.

[LM90] D. Lehmann and M. Magidor. Preferential logics: the predicate calculus case. In Rohit Parikh, editor, Proceedings of the Third Conference on Theoretical Aspects of Reasoning About Knowledge, pages 57–72, Monterey, California, March 1990. Morgan Kaufmann.

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

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

[McC86] J. McCarthy. Applications of Circumscription to Formalizing Commonsense Knowledge. Artificial Intelligence, 28:89–116, 1986.

[Ram78] F. P. Ramsey. General Propositions and Causality (1925). In D. H. Mellor, editor, Foundations: Essays in Philosophy, Logic, Mathematics and Economics, pages 237– 257. Routledge and K. Paul, London, 1978.

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

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

[Sta68] R. Stalnaker. A theory of conditionals. In N. Rescher, editor, Studies in logical theory, number 2 in American philosophical quarterly monograph series. Blackwell, Oxford, 1968. Also appears in Ifs, (ed., by W. Harper, R. C. Stalnaker and G. Pearce), Reidel, Dordrecht, 1981.