NON-MONOTONICITY AND CHANGE

a dissertation

submitted to the department of computer science

and the committee on graduate studies

of stanford university

in partial fulfillment of the requirements

for the degree of doctor of philosophy

By Tom Costello February 1997

\begin{matrix}c \\ ◯ \end{matrix} Copyright 1997 by Tom Costello All Rights Reserved

I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

John McCarthy (Principal Adviser)

I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

Grigori Mints

I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

Johan van Benthem

Approved for the University Committee on Graduate Studies:

Dean of Graduate Studies

Abstract

Non-monotonic reasoning is reasoning that will deny conclusions it the light of new evidence. This kind of reasoning is important for many common sense phenomena. In particular it is useful in reasoning about change.

Circumscription is a common methodology for capturing non-monotonic inferences. I characterize its expressive power, and show how it can be extended, to be more tolerant of new defaults, and so that it can capture defaults that current versions cannot express.

Examples from reasoning about action are used as the primary motivating tool.

Preface

This thesis is about non-monotonicity and change. It considers the problem of capturing the commonsense defaults humans make using formal logic. In particular it attempts to characterize those defaults that concern reasoning about change.

Acknowledgments

I would like to thank Anna Patterson for reading the very rough early drafts, John McCarthy for help and support for many years, Grigori Mints for teaching me what logic I know, and Johan van Benthem for all his advice on reshaping this thesis into its current form.

Contents

Preface vii

Acknowledgments ix

1 Introduction 1 1.1 Non-monotonicity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Preference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 The Expressive Power of Circumscription 11 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2 Logical Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3 The Model Theory of Circumscription . . . . . . . . . . . . . . . . . 15

2.3.1 Propositional Formula Circumscription . . . . . . . . . . . . . 16 2.3.2 Semantics of Propositional Circumscription . . . . . . . . . . . 17 2.3.3 Characterization of Minimized Formulas . . . . . . . . . . . . 19 2.3.4 Infinitary Cases . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.3.5 Finite Sequences of Quantifiers . . . . . . . . . . . . . . . . . 21 2.3.6 Infinite Sequences of Quantifiers . . . . . . . . . . . . . . . . . 23 2.4 Consequence Relations . . . . . . . . . . . . . . . . . . . . . . . . . . 26

2.4.1 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

3 Conditional Circumscription 31 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.2 Logical Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.3 Compositionality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

3.3.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.3.2 Conditional Circumscription . . . . . . . . . . . . . . . . . . . 35 3.3.3 Compositionality and Elaboration Tolerance . . . . . . . . . . 38

3.4 First Order Case . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.4.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.4.2 Conditional Circumscription Sentence . . . . . . . . . . . . . . 43

3.5 The Projection Problem . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.5.1 The Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.5.2 The Situation Calculus . . . . . . . . . . . . . . . . . . . . . . 45 3.5.3 The Language of the Situation Calculus . . . . . . . . . . . . 45

3.6 Projection with Circumscription . . . . . . . . . . . . . . . . . . . . . 46 3.6.1 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.6.2 Chronological Ignorance . . . . . . . . . . . . . . . . . . . . . 50 3.6.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

3.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 4 Domain Formula Circumscription 54

4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 4.1.1 Domain Circumscription . . . . . . . . . . . . . . . . . . . . . 56 4.1.2 Predicate Circumscription . . . . . . . . . . . . . . . . . . . . 59 4.1.3 Formula Circumscription . . . . . . . . . . . . . . . . . . . . . 61 4.1.4 Second Order Circumscription . . . . . . . . . . . . . . . . . . 62

4.2 Domain Formula Circumscription . . . . . . . . . . . . . . . . . . . . 63 4.2.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 4.2.2 Syntactic Form . . . . . . . . . . . . . . . . . . . . . . . . . . 65 4.2.3 Why Maximizing . . . . . . . . . . . . . . . . . . . . . . . . . 69

4.3 Non-finitely axiomatizable theories . . . . . . . . . . . . . . . . . . . 72 4.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

5 Cofinal Circumscription 75

5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 5.1.1 Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 5.1.2 Uses of Circumscription . . . . . . . . . . . . . . . . . . . . . 78

5.2 Reasonable States of Belief . . . . . . . . . . . . . . . . . . . . . . . . 80 5.3 Advantages and Disadvantages . . . . . . . . . . . . . . . . . . . . . . 85

5.3.1 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 5.4 Second Order Characterizations . . . . . . . . . . . . . . . . . . . . . 89

5.4.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.4.2 Formal Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 91 5.4.3 Comparison with Other Work . . . . . . . . . . . . . . . . . . 95 5.4.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 6 The Frame Problem 97

6.0.5 Frame Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 6.0.6 Non-monotonic Logic . . . . . . . . . . . . . . . . . . . . . . . 98 6.0.7 What a solution should generate . . . . . . . . . . . . . . . . . 99

6.1 A Natural Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 6.2 Baker’s Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 6.3 Other Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105

6.3.1 Monotonic Solutions . . . . . . . . . . . . . . . . . . . . . . . 105 6.3.2 Hand-crafted Second Order Axioms . . . . . . . . . . . . . . . 109 6.3.3 Why we need disjunction . . . . . . . . . . . . . . . . . . . . . 112

6.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 6.4.1 The Yale Shooting Problem . . . . . . . . . . . . . . . . . . . 116 6.4.2 The Walking Yale Shooting Problem . . . . . . . . . . . . . . 117 6.4.3 Explanation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118

6.5 Advantages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 6.6 Other Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 6.7 Caveats . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 6.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122

7 Conclusion 123

7.1 Goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 7.1.1 Consistency Preservation . . . . . . . . . . . . . . . . . . . . . 123 7.1.2 Naturality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124 7.1.3 Domains and Equality . . . . . . . . . . . . . . . . . . . . . . 125 7.1.4 Contingent Defaults . . . . . . . . . . . . . . . . . . . . . . . 126 7.1.5 Expressive power . . . . . . . . . . . . . . . . . . . . . . . . . 126

7.2 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 8 Appendix 128

8.1 Other Modifications of Circumscription . . . . . . . . . . . . . . . . . 128 8.1.1 Hintikka . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 8.1.2 Bossu and Siegel . . . . . . . . . . . . . . . . . . . . . . . . . 128 8.1.3 Shoham . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 8.1.4 Rathmann, Winslett and Manasse . . . . . . . . . . . . . . . . 129 8.1.5 Other Suggestions . . . . . . . . . . . . . . . . . . . . . . . . . 130 8.1.6 Nested Abnormality Theories . . . . . . . . . . . . . . . . . . 131

8.2 Equality of Closed Terms . . . . . . . . . . . . . . . . . . . . . . . . . 133 8.2.1 The Unique Names Assumption . . . . . . . . . . . . . . . . . 133 8.2.2 Etherington, Mercer and Reiter . . . . . . . . . . . . . . . . . 134 8.2.3 McCarthy’s Suggestion . . . . . . . . . . . . . . . . . . . . . . 135 8.2.4 Lifschitz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136

Bibliography 137

Chapter 1

Introduction

1.1 Non-monotonicity

There is perhaps no field of study where examples are easier to find than nonmonotonic reasoning. Almost everything we believe we can be made to doubt. Some philosophers would claim that we are capable of doubting everything^{1}. Nonmonotonic reasoning, being the study of losing faith in one’s previous conclusions, is thus perhaps the most human of all subjects. It is difficult to imagine religion, drama, tragedy, or politics, in a world where no-one ever made a mistake.

As such, this thesis does not intend to be definitive on the subject of the human condition. Rather than being an over-arching review of all that is fallible, I intend to look at a simple, but hopefully useful, subset of the mistakes people make. By mistakes, I mean no insult to the robots, programs, and humans that carry out these actions, for I strongly believe (though I may be wrong) that sometimes we all have to jump to conclusions.

The first and most basic reason for needing to assent to beliefs that are possibly defeasible, is that sometimes we need to act. In life, as in the jungle, waiting until you are absolutely sure that the large striped animal is indeed a tiger is often fatal.

1Some would claim that because we can doubt we can be sure that we actually exist, but this is not important right now.

There are times when we need to act on less than perfect information. As we do not have all the facts we need to make a decision, the course we choose may turn out to be sub-optimal. If we later acquire the facts we lacked then we need to be able to assimilate this new information and change our beliefs.

This is not the only reason for non-monotonic reasoning. Perhaps the best understood, and most easily defined, use of non-monotonic formalisms is acting as a communication convention. Rather than list all the facts we believe, we state a metatheoretical construction that allows the other party to complete the facts when they are given a particular subset. This may sound complicated, but it is not. Statements like, “the following list is complete” are meta-theoretical ways of telling us that the only things with the property in question are the ones that are listed. The usual example of this is an airline reservation program. The only flights that exist are the flights that are listed.

Later we return to communication conventions, and consider several reasons why we might choose to use a convention. For now we point out that there need not be any particularly good reason for a communication convention, it may not be better, faster, or smaller. “What I tell you three times is true” is a convention, but this does not mean it is preferable to our usual assumptions.

A lot of early work on defeasible reasoning took its motivation from typical, or canonical objects. It looked at the properties of the typical, or most normal bird. This notion of normality is not the frequentist notion, we certainly cannot naively find out what is typical by mere counting. While most birds that ever were are dead, the typical bird is not dead, furthermore, while most people who ever lived are still alive, it would be hopelessly optimistic to claim that typically humans don’t die. The notion of typicality is closely related to probability, and to notions such as “few” “usually” and “most”. Perhaps there is a single notion behind these ideas, but it seems to the present author that it is more profitable to consider the utility of these ideas, rather than questioning their inherent meaning.

An interesting kind of default reasoning, that is strongly antithetical to any notion of probability, is the use of a default as a policy. If one is trying to escape from a maze, one may, by default, choose to follow the left hand wall. This is not based on any belief that this is the shortest route. A policy that meetings are on Wednesday, if not otherwise stated, does not imply that most meetings are on Wednesday, and showing that in fact most meetings were on Friday would rarely constitute a valid excuse. We assume by default that defendants are innocent, this stands in strong opposition to the fact that most defendants are in fact guilty.

Perhaps the least ambitious, and therefore of course the most useful application of non-monotonicity is as a storage convention. This is related to using it as a communication convention, but here we have decided on why we want to use a convention. Information can be compressed, and thus stored more efficiently if we use a little non-monotonic reasoning. Again, a simple example is that dictionaries list only those sequences of letters that correspond to correctly spelled words. Despite the fact that people often look up sequences of letters that are not words, dictionaries continue this practice, realizing that humans are capable of carrying out whatever reasoning is necessary to solve their conundrum. This is a non-trivial problem for the human, as it is quite possible that their sequence of letters is a word in some better dictionary. Clearly a dictionary that listed some common sequences that were not words would be a veritable boon for scrabble players, linguists and others, but due to space considerations this is sadly not the case.

A notion that we will return to time and time again in this thesis, is that of elaboration tolerance. It, like storage conventions, is closely related to communication conventions, but it is a subtler notion. A representation of knowledge is elaboration tolerant, if, when new information is assimilated, the amount of change that has to be made is proportional to the amount of information added. Ideally, information should be added by conjoining it to our current evidence. This clearly entails a non-monotonic system.

Much of our arguments in favor of non-monotonicity can be countered by the claim that while this use of defaults might be useful for humans, machines may not need to act in this way. While I reject this argument entirely, even if it were the case, machines will need to understand defaults in order to communicate with humans. Defaults are deeply ingrained in our psyche. Most people find it difficult to come up with more than three things that are unassailably true. Whether we came to use defaults by accident, or whether they are a natural out-growth of the way we learn is unimportant. It is undeniable that we cannot communicate without their use.

We often believe that certain states of affairs are more likely than others. However, we often cannot put numbers on these probabilities. Orders over how likely certain states are can act as a sort of streamlined probability, where the actual numbers are not available to the reasoner.

We now summarize some of the causes of the ubiquity of non-monotonicity:

• Decisions with incomplete information.

• Communication convention.

• Storage convention.

• Elaboration tolerance.

• Policy.

• Fuzzy quantifiers—typically, usually, most, few.

• Streamlined probability

• Communications with humans.

1.2 Preference

As we have seen non-monotonicity is constantly encountered. This thesis concentrates on one particular way of looking at this phenomena. We look at the idea of preference, that is, that sometimes we think that we should assume that one state of the world is the case rather than another. We shall take this as our underlying guide throughout this thesis.

Naturally, taking a notion of this as basic leads us to consider our model theory as more fundamental than our proof theory. We claim that this is justified, as our intuitions about model theory usually tend to be sufficiently general, the problems we encounter are usually that we have made distinctions we cannot justify. On the other hand, proof theory often leads us to confuse ideas that are best kept separate. For this reason we take as our fundamental bedrock model theory tempered with proof theory rather than vice-versa.

Once we have decided to look at this notion of preference, we are by no means out to the woods. Ideas that seem crystal clear initially can often have much confusion hidden inside. Our methodology for detecting these flaws is firstly our proof theory, but more importantly it is our experience of the world. Examples shall constantly drive the intuitions of this thesis.

1.3 Examples

We draw examples from many parts of everyday life, before this thesis is finished we shall all be close acquaintances with royal elephants, flying penguins, damp grass, and the occasional assassination of Fred. Our major source of extended examples will be reasoning about change. When differing intuitions push in opposite (or even different) directions we shall follow the intuitions that reasoning about change offers. We do not choose this guide lightly, long experience has taught us that change offers a challenging but approachable path.

We have very strong intuitions about change. Sometimes, after far too much consideration of a trivial problem, our intuitions may become muddied, but a brief discussion with anyone outside academia will swiftly disabuse us of any nonsense of which we may have convinced ourselves.

Change, however, is not an easy master. The problems it offers can be subtle and challenging. The most basic problems in the area, the frame and qualification problems are among the best known problems in logical AI. Thus it offers a worthy opponent for non-monotonic theories.

The frame problem is perhaps the most classic A.I. problem. It has changed over the years from a problem of how to store information efficiently, into a question of how we should represent information so that one can easily add to it.

Before dealing with representing defaults in particular instances, the question of how to represent defaults at all must be tackled. Here we are offered a wealth of possibilities. These can naturally be split into four approaches. The first approach, in no particular order, grew out of logic programming. It encompasses default logic, Sandewall’s unless, negation as failure, the closed world assumption and its generalizations, justification based truth maintenance systems, and all notions which centered on a notion of groundedness, expressed as a minimal fixed-point, or as end-regulated sequences. This approach is firmly centered in a computational interpretation of defaults, where a default is something that should be applied, much like an inference rule. I do not like this approach. I find its semantics unwieldy, and find its computational metaphor over-stretched.

The second main school is based around the notion of introspection. Its earliest proponents were McDermott and Doyle. It is based around the idea that we should equip a reasoner with the ability to represent information about its own beliefs. We can then simply tell the reasoner about its own storage conventions, and indeed about any particular biases that it might have. This area has become known as autoepistemic logic. The first successful logic in this area is due to Moore, but there is a wealth of research, all of which extends the basic ideas of how to naturally treat a modal operator, usually denoted Lϕ that represents ones own beliefs. This inherits all the problems of modal logic, and offers no clear path as to what defaults should be the case. It offers us a powerful language, when extended to the first order case, but little intuition on how to proceed.

The third main approach has its roots in conditional logic. It is perhaps the most disparate area, encompassing belief change conditionals, counterfactual semantics, defeasible logics, and more recently non-monotonic consequence relations. The work in this area has attempted to give a meaning to conditionals, sentences of the form, “If … were the case then … would be the case”. We shall look at one thread of this approach, non-monotonic consequence relations. In the course of this work we shall show this approach is very similar in spirit to the following approach. However, our heart remains firmly in the next camp.

The last cluster of researchers into non-monotonic reasoning are those based around the idea that some states of the world are more likely than other states of the world, so much more likely in fact that if both states are possible we would discount the less likely state. Thus this area has its feet firmly placed in the semantic realm. Its basic entities are states of the world, often viewed as models of a theory. It orders these states, and views the more likely states as better guides to what the world is like than the less likely states.

This clearly has strong roots in probability theory, but unlike that theory, it is willing to go from a probability near one to certainty in many situations. It also has strong roots in the semantic approaches to counterfactuals, which often talk of the most similar worlds to the current world.

McCarthy’s circumscription 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 than to choose the sentences true in the minimal models or worlds 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 been studied by many researchers. McCarthy’s original suggestion was to order models based on the size of their domain, preferring smaller domains, analogously to mathematical induction. He later extended this to minimizing the extension of a predicate, and then of an arbitrary open formula. Other researchers considered going to richer models than first order frames.

Of the four methodologies, I intend to pursue the last. I feel that in all the uses of non-monotonic reasoning that I have looked at there we have strong intuitions as to which models should be chosen in each particular circumstances. However, this is not to say that the approach is without its difficulties. Overcoming these difficulties will be a major part of the work of this thesis. Accordingly, we look at what these stumbling blocks are.

1.4 Problems

While it seems reasonable that we often view one state of the world as more likely than another, it is not immediately obvious that the states we order are complete states of the world. Perhaps what we order are sets of states of the world, and perhaps we might view one set of states as more likely than a subset. Indeed we can find natural examples of this. Suppose I knew that the stock price of IBM was not going to rise tomorrow. In that case, I could make a lot of money selling options. On the other hand, should I know that the price of IBM was going to rise tomorrow, I could also make a lot of money on the stock market. Yet, every day I know that tomorrow either IBM stock will rise or it won’t. This does not make me rich. While the two states, my knowing IBM is going up, and knowing it will go down, together are a very normal state of affairs, each on its own is unusual. In this example, as in many of the examples that seem to prefer a set of states to one of its members, we can detect a hidden, (badly in this case), epistemic operator. It was not the world I was actually talking about, but actually my knowledge of the world. This is no proof that in general we order states of the world, rather than individual states, but in the absence of any evidence to the contrary I intend to take the path of least resistance and assume that what we are talking about, when we say that something is more likely than something else, are states.

Another question left unanswered is what properties does the relation, “preferred to” have. It is transitive and reflexive, but does it have more properties than that. Does it order all possible worlds, or just a subset? Is it a partial order, a total pre-order, or a total order?

A property many researchers have assumed that “preferred to” has it the property that it is well-founded in some way. That is, that it has minimal elements. From a semantic viewpoint this is nonsense. There is no possible reason to believe that preferences on states of the world are well-founded a-priori. Secondly, there are many obvious examples of preferences that are not well-orders.

However, the researchers that assumed this smoothness have their reasons. If we do not assume that minimal worlds exist, how are we to define our conclusions— remember we said they were the consequences true in all the minimal worlds.

Even if we settled these questions, we still must decide whether we have perfect information about our preferences on worlds. Is it possible that we might be unsure what the actual preference might be? I find it reasonable that we could be unsure.

Finally once we have settled all the semantics questions we are left with the implementation question. How should we represent this preference on worlds? McCarthy suggested generating a preference by minimizing the extent of a formula. Boutilier, following Lewis suggests using a pair of modal operators. Naturally those studying conditional logics would push for using a conditional, while probabilists suggest standard probability theory augmented by non-standard probabilities. This question can only be answered by considering what benefits one way of describing an order has over other ways. Our criterion for deciding how to proceed is elaboration tolerance. We wish to be able to modify our preferences easily, when we receive the kind of new information that is usually received.

To summarize I list the defaults I intend to capture, and the difficulties that await in applying the current non-monotonic logics to these problems

• The first problem is minimizing the amount of change. How can we simply express the idea that the amount of change between each state should be minimized.

• The second problem is expressing the default that actions have as few effects as possible. This problem seems very similar to the first, but as we shall see it is not the same.

We see there are several problems with current non-monotonic formalisms.

• Many formalisms based on circumscription map consistent(satisfiable) theories to inconsistent(unsatisfiable) theories. This is clearly unacceptable if the theories we are likely to use to describe the world fall into this set.

• Many formalisms do not have intuitive semantics—it is difficult to see why their models are a description of our view of the world.

• Some formalisms have difficulty representing defaults that involve equality.

• Some formalisms do not easily represent contingent defaults, that is defaults that only apply in certain circumstances.

• The expressive power of many formalisms is unknown.

• Many formalisms does not allow defaults to change the domain of the original theory.

All these problems need to be addressed before we use non-monotonic reasoning to solve problems.

The Expressive Power of

Circumscription

Summary

Circumscription is a form of non-monotonic reasoning, introduced by McCarthy (1977) as a way of characterizing defaults using second order logic. McCarthy defined the consequences of circumscription as those sentences 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(McCarthy 1980, McCarthy 1986) 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 over finite languages. We consider the question of infinite languages, and give the corresponding representation theorems. Infinitary propositional logics correspond closely to first order logics with fixed domains. We show that even logics with countable connectives cannot describe all pre-orders over countable infinite languages.

Finally, contrary to previous claims, we show that propositional formula circumscription can capture all preferential consequence relations over finite propositional languages, as defined by Kraus et al.(1990). Thus, in the finite propositional case, there is no restriction on the kinds of preferential defaults that circumscription can describe.

2.1 Introduction

McCarthy’s circumscription(1977) 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. McCarthy’s original suggestion was to order models based on the size of their domain, preferring sub-models, analogously to mathematical induction. He later extended this to minimizing the extension of a predicate, and then of an arbitrary open formula.

The notion of minimal entailment has been considered by many researchers. It has one of its roots in Ramsey’s (1978) 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 Stalnaker (1968), Lewis (1973). Gärdenfors (1978, 1988), and Makinson (1988) have considered similar themes in belief revision, which has connections with non-monotonic reasoning (Gärdenfors and Makinson 1994). Shoham (1986b) 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 initiated by Gabbay (1985) based on characterizing non-monotonicity through proof 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 since McCarthy’s domain circumscription 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 a filter 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.

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

If we use infinite languages, and infinite sets of minimized formulas, we can still not capture all pre-orders—only those pre-orders whose filters 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.

Finally we look at preferential consequence relations as defined by Kraus et al. (1990). We show that formula circumscription of propositional theories can capture all preferential consequence relations, over finite propositional languages. Previously Kraus et al. (1990)(pp. 169) have claimed that circumscription was unable to characterize these relations.

2.2 Logical Preliminaries

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

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

∀d d′ d′′ ∈ D.d ≲ d′ and d′ ≲ d′′ implies d ≲ d′′

∀d ∈ D.d ≲ d

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

∀d d′ ∈ D.d′ ≦ d and d ≦ d′ implies d = d′

We use ≤ to denote an order, when we do not wish to specify whether it is a partial order or a pre-order.

Definition: 3 (ideal/filter) An ideal I of a pre/partial order ≤ over a domain D is a subset of D that is downwards closed: that is

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

A filter F of a pre/partial order ≤ over a domain D is a subset of D that is upwards closed, that is

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

Proposition: 1 • Every pre/partial order is uniquely defined by its filters.

• Every pre/partial order is uniquely defined by its ideals.

• The complement of a filter is an ideal.

Proposition: 2 The family of filters F of a pre/partial order ≤_{D} is closed under arbitrary unions and intersections.

Proof: Let {F_{i}|i ∈ I} ⊂ F be a family of filters. Consider ⋃_{i∈I} F_{i}. We show it is upwards closed. Assume it was not, then there would be an d and d′ such that d ≤ d′ but d ∈ ⋃_{i∈I} F_{i} and d′ ∉ ⋃_{i∈I} F_{i}. But, we know that if d ∈ ⋃_{i∈I} F_{i} then d ∈ F_{j} for some j ∈ I. As F_{j} is a filter d′ is in F_{j}, and thus in ⋃_{i∈I} F_{i}, in contradiction to our assumption. The proof of intersection is similar.

Proposition: 3 Every family of sets F whose elements are closed under arbitrary union and intersection is the family of filters of a unique pre-order ≤.

Proof: We are given a family of sets F. We retrieve a relation ≲ by taking d ≲ d′ exactly when ∀F ∈ F.d ∈ F → d′ ∈ F. We now show that this is a pre-order. It is clearly reflexive, and it is transitive, as implication is transitive. Finally we show that this pre-order is unique. This can be seen by the fact we can re-create F, by taking the filters of ≲. Thus ≲ is the required ≤.

Definition: 4 (basis) A basis B for a family F of filters of a pre-order ≤, is a subset of F, such that every set in 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 ≤, over 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′}.

2.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 (1985) in his reformulation of formula circumscription (McCarthy 1986). It also uses the device introduced by deKleer and Konolige (1989) 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 the pre-orders 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 relative to this preorder are exactly the consequences of circumscription. We then consider the question of what pre-orders circumscription can capture. As our first step towards this we look at how minimized formulas are related to the pre-order they generate. We see that the set of models of each minimized formula is a filter of the pre-order on valuations. We next show that the pre-order is the unique pre-order generated by these filters. This establishes the basic representation result for circumscription— minimal entailment over 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.

2.3.1 Propositional Formula Circumscription

McCarthy (1986) introduced a form of circumscription, called formula circumscription. It extends predicate circumscription (McCarthy 1980) 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 (1980).

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 (1986)) If γ_{1}, γ_{2} is a pair^{1} of formulas, and P_{1}, …, P_{n} are the propositional letters in our language, then we define the circumscription of a formula α minimizing formulas γ_{1}, γ_{2}, written Circ(α; γ_{1}, γ_{2}) as follows.

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

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 α.

2.3.2 Semantics of Propositional Circumscription

Definition: 9 (≤^{Γ}) Given a propositional language L\overline{P}, over a set of letters, \overline{P}, and a set of formulas Γ, in L\overline{P}, we define the relation ≤^{Γ} over 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 over a given propositional language. It is not in general a partial order, as there are distinct valuations that are ≤^{Γ} than each other.

Proposition: 4 For a given propositional language L\overline{P}, and a set of formulas Γ, in L\overline{P}, ≤^{Γ} is a preorder, but not always a partial order.

Proof: That ≤^{Γ} is a pre-order follows immediately 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 reflexitivity, 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. This provides a counterexample to anti-symmetry.

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

We then have the following proposition.

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

A valuation 𝔄 over 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 sentence is the second conjunct in the definition of circumscription.

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

2.3.3 Characterization of Minimized Formulas

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

Proposition: 6 Given a set Γ of formulas from a propositional language L\overline{P}, the set of models of each γ ∈ Γ is a filter 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 𝔄 ⊧ γ. Therefore 𝔅 ⊧ γ as required.

This gives a structural interpretation of minimizing a formula. A minimized formula is a filter of the pre-order on valuations.

We now show that the pre-order ≤^{Γ} is the pre-order with the fewest filters that has all the filters in Γ.

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

Proof: We know that every formula in Γ generates a filter. We further know that arbitrary unions and intersections of filters are filters. We consider the set of sets of valuations, M corresponding to Γ. We close out M under arbitrary unions and intersections, to get M′. M′ is a family of filters, as the union and intersection of elements of M′ are in M′. M′ is minimal as any smaller family would deny that every set in M was a filter.

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

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

Proof: For each filter of ≤, take a formula defining it. The set of all these filter formulas is the required set Γ.

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

2.3.4 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_{n}|n ∈ ω . Consider the following pre-order 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 γ.

Thus the family of filters that are represented by formulas of this pre-order is empty. However, the empty set of formulas is also a basis for the discrete pre-order.

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

Theorem: 9 If ≤ is a pre-order over 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 filters where each element in the basis is finitely axiomatizable.

Proof: ⇐: We take the finitely axiomatizable filters as our set Γ. As there is a finitely axiomatizable basis for the filters, the finitely axiomatizable filters form a basis, and thus they characterize ≤.

⇒: We prove the contrapositive.

Suppose there is no basis, all of whose members are finitely axiomatizable. Then consider all finitely axiomatizable filters. Let these be Γ′. Then our assumption is that there is a filter x, that is not definable in terms of the elements of Γ′ and union and intersection.

Every pre-order ≤^{Γ} with Γ ⊂ Γ′ does not contain x, and thus is not equal to ≤. Every pre-order ≤^{Γ} with Γ ⊋ Γ′ contains a γ, that is not in Γ′. Therefore, ≤^{Γ} has γ as a filter. However, γ is finitely axiomatizable, and thus, is not a filter of ≤, as all finitely axiomatizable filters are elements of Γ′, by assumption. Thus ≤^{Γ} contains an extra filter, and thus is not equal to ≤.

This gives us a characterization of what minimizing infinite sets of formulas can capture.

2.3.5 Finite Sequences 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 variables in the circumscription formula is finite.

We now give a representation theorem for circumscription. We characterize exactly those pre-orders that 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 ∈ D d′ ∈ 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: 10 If ≤ is a pre-order on valuations over a language L\overline{P}, and ≤′ is a pre-order on valuations over a language L\overline{P′}, where \overline{P} and \overline{P′} are disjoint then ≤ × ≤′ is isomorphic to a pre-order on valuations over 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 over 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 sentence. These can alternately be considered to the letters that are varied ( in the sense of McCarthy (1986)) in the minimization process.

Definition: 11 ( ≤^{Γ;\overline{P′}}) Given a propositional language L\overline{P}, and a finite set of formulas Γ, in L, and a finite set \overline{P′} ⊂ \overline{P}, the varied letters, we define the relation ≤^{Γ;\overline{P′}} over the valuations of L\overline{P} as follows. For any two valuations 𝔄, 𝔅, we write 𝔄 ≤^{Γ} 𝔅 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 infinite languages.

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

Proof: ⇐: From Theorem 8, we can choose a set Γ that exactly characterizes ≤_{f}. We choose \overline{P′} to be the propositional letters in the valuations of ≤_{d}.

⇒: we choose ≤_{f} to be ≤^{Γ} over the the valuations of L\overline{P′}, and we choose ≤_{d} to be the identity on the valuations of L_{\overline{P} −\overline{P′}}.

Thus we have shown that our propositional formula circumscription captures all pre-orders of a certain general class. Pre-orders over models, of this type, 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.

2.3.6 Infinite Sequences 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. We now look at the case of languages with infinitary connectives. We first consider the propositional language L_{ω_{1}}, which allows countable conjunctions and disjunctions of formulas. We look at these languages because they 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.

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.

Definition: 12 The language L_{ω_{1},\overline{P}} is the propositional language whose formulas are the smallest set containing all the letters in \overline{P}, and closed under negation, and countable conjunction and disjunction.

The language L_{ω_{1}ω_{1},\overline{P}}^{2} , is the second order extension of L_{ω_{1},\overline{P}} with countable strings of quantifiers ranging over propositions.

It is notable that we shall only use the fragment of this language without nesting of quantifiers. We shall only use sequences of the universal quantifier.

Definition: 13 If γ_{1}, γ_{2} is a pair of formulas in L_{ω_{1},\overline{P}}, and P_{i}|i ∈ ω are the propositional letters in our language, then we define the infinite circumscription of a formula α of L_{ω_{1},\overline{P}} minimizing γ_{1}, γ_{2}, written InfCirc(α; γ_{1}, γ_{2}) as follows. We use α̃ to denote the formula, α[ψ_{1}/P_{1}, …, ψ_{i}/P_{i}, …], that is the result of the replacement of the propositional letters P_{i} in α by the propositional variables ψ_{i}.

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

Proposition: 12 Let α be a formula of L_{ω_{1},\overline{P}}, and Γ a countable set of formulas of L_{ω_{1},\overline{P}}.

A valuation, 𝔄, over a countable set of propositional letters, \overline{P} satisfies the second order formula InfCirc_{L\overline{P}} (α; Γ), if and only if 𝔄 is minimal in the set of models of α with respect to ≤^{Γ}.

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

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

γ_{1}[ψ_{1}/P_{1}, …, ψ_{i}/P_{i}, …], …, γ_{j}[ψ_{1}/P_{1}, …, ψ_{i}/P_{i}], … ≤ γ_{1}, …, γ_{i}, …] → γ_{1}, …, γ_{j}, … ≤ γ_{1}[ψ_{1}/P_{1}, …, ψ_{i}/P_{i}, …], …, γ_{j}[ψ_{1}/P_{1}, …, ψ_{i}/P_{i}, …], … The first equivalence follows from the definition of Minimal. The second follows from the definition of ≤^{Γ}, the third is valid as a model can be viewed as a valuation function, and from the definition of satisfiability. This is the first place we have used the fact we are dealing with an infinitary logic. Note this requires that there be only a countable number of propositional letters. The last sentence is the right conjunct in the definition of infinite circumscription.

Proposition: 13 Given a set Γ of formulas from a propositional language L_{ω_{1}ω_{1},\overline{P}}, the set of models of each γ ∈ Γ is a filter of the pre-order ≤^{Γ}.

Proof: Exactly as proposition 6.

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

Theorem: 14 Given a set Γ of formulas of a propositional language L_{ω_{1}ω_{1},\overline{P}}, the pre-order ≤^{Γ} is the unique pre-order whose filters include the models of each formula in Γ, and whose set of filters is minimal.

Proof: Exactly as proposition 7.

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

Theorem: 15 There exists pre-order ≤ over 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}ω_{1},\overline{P}}.

Proof: Consider a total order on the valuations. This pre-order has 2^{ω} filters, none of which are definable in terms of the union or intersection of other filters. Thus the only Γs, such that ≤^{Γ}=≤, that can represent this have 2^{ω} elements.

Thus, as the power of InfCirc is exactly those pre-orders that can be expressed by a ≤^{Γ}, with Γ countable, we have exactly captured the boundary of what we can describe.

2.4 Consequence Relations

We now compare propositional circumscription to another proposal for characterizing non-monotonicity. This other proposal, non-monotonic consequence relations has its roots in conditional logic (Veltman 1986). It differs from conditional logic in two notable ways. It studies only un-nested conditionals, and secondly, it is concerned in ways of completing sets of conditionals. These completions, such as rational closure do not concern us here.

We first consider the axiomatization that led Kraus et al. to consider preferential models.

Kraus, Lehmann and Magidor’s proposed axiomatizations (1990) of consequence relations capture a much larger set of models than pre-orders over worlds or models of an underlying propositional language. They consider partial orders or total pre-orders on states labeled by worlds. These two possibilities are called P, and R respectively. These axiomatizations gave rise to a new model theory, which we present below. For completeness we give the axiomatization they first proposed.

Definition: 14 ( (Kraus et al. 1990)) A consequence relation |∼ over a language L_{P} 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.

Definition: 15 A preferential consequence model over a language L_{P} is a triple ⟨W, l, ≺⟩, where W is a set of states, l : W ↦ 2^{P} assigns a world to each state, and ≺ is a strict partial order on W satisfying the condition that for every α, there is an element y that is minimal among the states x, such that l(x) ⊧ α, or there is no state whose label models α.

They then get the following representation theorem:

1 Theorem due to: (Kraus et al. 1990) A consequence relation is a preferential consequence relation if and only if it is the consequence relation defined by some preferential model.

We now show that we can capture all preferential consequence relations using circumscription.

Theorem: 16 Every preferential consequence relation, over a finite propositional language L\overline{P}, is captured by conjoining a formula β ∈ L_{\overline{P} ∪\overline{P′}}, and minimizing a finite set of formulas Γ ⊂ L_{\overline{P} ∪\overline{P′}}, where \overline{P′} is a finite set of new propositional letters.

There is a finite set of formulas Γ in L_{\overline{P} ∪\overline{P′}}, and a formula β ∈ L_{\overline{P} ∪\overline{P′}}, such that for all formulas γ, δ ∈ L\overline{P},

γ |∼ δ if and only if Circ(γ ∧ β; Γ) ⊢ δ

Proof: We note there are only a finite number of preferential consequence relations over a finite language, as there are only a finite number of inequivalent formulas.

Thus for finite languages we have the finite model property. That is, every preferential consequence relation over a finite set of propositional letters has a finite model.

Further we have a recursive bound f on the number of states in a preferential model, in terms of the number of propositional letters.

For a given preferential consequence relation, R, there is a preferential model R = ⟨X, ≤, l⟩ where X, the number of states is finite, and the labeling function l, maps states to valuations of a finite language. The number of states mapped to any particular valuation 𝔄 is bounded by X. As X is the size of the model, the number of states mapped to any particular valuation 𝔄 is bounded by the function f.

Let us call this bound n = h(∥P ∥), for a given propositional language P.

We introduce ⌈log_{2}n⌉ new propositional letters. They will act as labels for for valuations, allowing valuations that agree over L\overline{P} to appear in more than one place in the partial order. As there are 2^{m} assignments to m letters there are n valuations over the extended language that have the same assignment to letters in L\overline{P}.

We showed that every preferential consequence relation was modeled by a preferential model where every valuation occurred as a label no more than n times. Thus this preferential consequence relation can be modeled by a preferential model over the extended language, where every valuation occurs at most once.

Thus we have reduced the problem to characterizing a partial order where no models appear twice as labels. This is equivalent to specifying a partial order over a finite set of valuations.

We then note that we can characterize the valuations that do not appear in the partial order by a formula ¬β′. If the formula we adjoin is β′, then our conclusions will always come from the partial order.

Finally we have to characterize the partial order. We do this by listing is filters, Γ, and minimizing these. As we proved earlier this characterizes minimal entailment, and the number of filters is finite, as the partial order is finite. Thus we have extracted a formula β′ that we conjoin, and a finite set of formulas that we minimize.

Finally we need show that this conjoining and minimizing give the correct results. We consider the minimal states of an arbitrary formulas β, and their labels 𝔄_{i}, i ∈ I. We consider the corresponding models in our expanded language, 𝔅_{i}, i ∈ I. The labels 𝔄_{i}, and the models 𝔅_{i}, have the same valuations over L\overline{P} by construction. Furthermore, the models 𝔅_{i}, i ∈ I are the minimal models of β in the expanded partial order by construction. Thus entailment in the minimal models co-incides.

This theorem is close in spirit to a result of van Benthem (1987), where he shows that domain circumscription of unary predicates has the same general theory as unnested minimal conditional logic.

Van Benthem looks at domain circumscription, a form of circumscription where models of a first order theory are ordered by the sub-model relation. He shows that the admissible rules of conditional logic, essentially the admissible rules of P above, are related to the valid inferences in circumscription in the following way. A rule \frac{α_{1}>β_{1},... ,α_{n}>β_{n}}{ϕ>ψ} is admissible exactly when, for any substitution δ of propositional letters by formulas of the monadic predicate logic with identity, and every formula χ of such a language, χ, δ(α_{i}) ⊧_{domain} δ(β_{i}) for all i ≤ n, then χ, δ(ϕ) ⊧_{domain} δ(ψ), where ⊧_{domain} is the entailment relation induced by domain circumscription, essentially truth in the minimal models under the sub-model relation.

The difference between this result and ours lies in where we allow modifications. Van Benthem considers all theories of a certain syntactic form, that can be created by a substitution, while we consider all circumscription policies. His use of an extra condition χ parallels our use of β.

2.4.1 Discussion

The previous theorem is in strong contrast to Kraus, Lehmann and Magidor’s statement that

(pp. 169) (Kraus et al. 1990) The framework of preferential models, therefore, has an expressive power that cannot be captured by negation as failure, circumscription, default logic or auto-epistemic logic.

We have shown that circumscription can capture all preferential models over finite languages. The restriction to finite languages is not a severe restriction, as Kraus et al. make the assumption of compactness.

The construction in the proof above essentially uses the introduction of new propositional letters. This is common in circumscription—often abs are introduced. The role of the letters we introduce is more subtle. They point to incompletenesses in the partial order of models. That is, they show that we consider more than one partial order of models possible.

2.5 Conclusion

We have shown that minimizing a certain formula corresponds, in minimal models semantics, to stating that the set of models that satisfy a formula is a filter 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 connectives.

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.

Finally we have shown that circumscription is as expressive as preferential consequence relations, in contrast to previous claims.

Conditional Circumscription

Summary

Circumscription is a form of non-monotonic reasoning, introduced by McCarthy (1977) as a way of characterizing defaults using second order logic. The semantics of circumscription are defined as truth in the minimal models under a pre-order on models. In the case of domain circumscription the pre-order was the sub-model relation. McCarthy (1980, 1986) also considered other forms of circumscription. Formula circumscription 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.

However, the way in which formula circumscription describes defaults is not compositional. If we have one pre-order on models that is a strengthening of another pre-order, it does not follow that a circumscription policy that gives the first can be extended to a circumscription policy for the second. We introduce a new form of circumscription policy, conditional circumscription, that has this property.

This new form of circumscription captures natural defaults succinctly. We show that conditional circumscription has useful expressive power by employing it in an example from reasoning about action. We capture the intuition that when minimizing the changes an action makes, only situations that agree on all fluents should be compared.

3.1 Introduction

McCarthy’s circumscription (1977) 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 or worlds in this order as our current beliefs. McCarthy’s original suggestion was to order models based on the size of their domain, preferring sub-models, analogously to mathematical induction. He later extended this to minimizing the extension of a predicate, and then of an arbitrary open formula.

Recently, the author, in chapter 2 of this thesis (Costello 1996b) has shown that propositional formula circumscription can capture all pre-orders on models over finite languages, and further that it can capture all preferential consequence relations in the sense of Kraus et al. (1990). However, once we have shown that formula circumscription is expressive enough, it does not immediately follow that there is no need for more elaborate formalisms, such as prioritized circumscription (McCarthy 1986), Lifschitz (1985), pointwise circumscription (Lifschitz 1986b), or generalized prioritized circumscription Grosof(1991). We have only shown that it is expressive enough statically. It seems reasonable that we should ask for some sort of compositionality. If we wish to refine our pre-order we should be able to do this by adding defaults. We show that even in simple cases formula circumscription is not compositional. We then introduce a form of circumscription that obeys a strong compositionality principle— every finite sequence of progressively stronger pre-orders can be captured by a finite sequence of policies ordered by inclusion.

Finally, we attempt to justify our new form of circumscription on epistemic grounds. We consider a natural problem in reasoning about action—temporal projection. Many previous attempts at characterizing this default fell victim to the infamous Yale Shooting Problem (Hanks and McDermott 1986). We show that adding the condition that situations should only be compared if they agree on all properties overcomes this difficulty.

This is a novel solution to the problem, different from previous approaches. Previous approaches were based on a notion of causality (Baker 1991, Lifschitz 1987, Haugh 1987, Stein and Morgenstern 1994), temporal minimization (Shoham 1986b, Lin 1991, Lin and Shoham 1991, Sandewall 1994, Lin and Shoham 1995), or on what some call a monotonic completion (Reiter 1991, Schubert 1990, Pednault 1989). It has most similarity to those solutions (Winslett 1988, Kartha and Lifschitz 1995) based on minimal change but differs in how it explains what is the underlying fault of a naive minimal change approach.

3.2 Logical Background

Historically, domain circumscription was the earliest form of circumscription. It was introduced in (McCarthy 1977). It was studied by Davis (1980), and further investigated by Etherington and 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 as suggested by Reiter (1987), 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.

McCarthy (1980) introduced a new form of circumscription predicate circumscription. 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.

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

deKleer and Konolige prove (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.

3.3 Compositionality

3.3.1 Motivation

We now look at some cases where, although circumscription characterizes our defaults, it does not do so in a compositional way. This failure motivates our introduction conditional circumscription , which allows us to represent defaults compositionally.

Our motivating example for conditional circumscription concerns a certain Tarzan. He has recently met his lovely partner Jane. As a result of this he is very much in love.

Based on this information we can make certain assumptions. It is much more likely that Tarzan will be happy than sad, if he is with Jane, and it is much more likely that Tarzan will be without Jane, given that he is sad. Clearly we can represent this state of affairs as a preference on models. We draw out our preference on models by adding links from one valuation to another when the lower is strictly more preferred. We call this pre-order ≤_{1}.

[figure: ¬Happy, Jane; Happy, ¬Jane; Happy, Jane; ¬Happy, ¬Jane]

So far, so good. But now, because of a bias towards logical reasoning we try to capture these defaults using circumscription. Sadly, as we see next, defaults of this type are not naturally represented using circumscription.

This is because the pre-order for the two defaults, ≤_{1} is not the union of the pre-orders for each of the individual defaults. We would like to compose pre-orders by union, by unioning the circumscription policies, however, classic circumscription leads us to represent certain defaults in a way that prevents this.

We now consider conditional circumscription. It is based on the notion that a preference can be stated by saying that a predicate should be minimized only when a certain condition is met. In the above examples, we would minimize ¬Happy, when Jane was the case, and minimize Jane when ¬Happy was the case.

3.3.2 Conditional Circumscription

Like classic circumscription, conditional circumscription expresses the non-monotonic consequences of a theory by a second order sentence. What is changed is the way in which circumscription policies are specified. A conditional circumscription policy is a set of ordered pairs of formulas. We say the first formula is minimized, when the second formula is the case.

Semantics

We can define the semantics of conditional circumscription in terms of minimal models. A conditional circumscription policy is a set of pairs of formulas. The first formula in a pair is called the condition, and the second the minimized formula. We say two valuations 𝔄 and 𝔅 are in the relation ≤ if the whenever a condition is true in both valuations, the minimized formula is true in 𝔅 if it is true in 𝔄. The consequences of circumscription of a theory A are the sentences true in all minimal models of A under this pre-order ≤.

We can write this more formally as follows.

Definition: 16 ( ≤_{( \frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn})}) Given a propositional language L\overline{P}, where \overline{P} is the set of propositional letters, and a conditional circumscription policy, C = (\frac{γ_{1}}{δ_{1}} , …, \frac{γ_{n}}{δ_{n}}), where γ_{i}, δ_{i} ∈ L\overline{P}, we define the pre-order on valuations ≤_{( \frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn})} such that, if 𝔄 and 𝔅 are two valuations over the letters \overline{P}, then

𝔄 ≤_{( \frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn})} 𝔅 if
( 𝔄[δ_{i}] = 1 and 𝔅[δ_{i}] = 1) and ∀i ≤ n.𝔄[γ_{i}] = 1 implies 𝔅[γ_{i}] = 1

Conditional Circumscription Sentence

We can express these consequences as a second order sentence^{1}.

Definition: 17 (Circ_{C}) If (\frac{γ_{1}}{δ_{1}} , \frac{γ_{2}}{δ_{2}} ) is a pair of pairs of formulas of L_{\{P_{1},... ,P_{n}\}}, then we define the circumscription of a sentence α ∈ L_{\{P_{1},... ,P_{n}\}} minimizing γ_{1}, γ_{2} when δ_{1}, δ_{2} written Circ_{C}(α; \frac{γ_{1}}{δ_{1}} , \frac{γ_{2}}{δ_{2}} ) as follows.

α ∧ ∀ϕ_{1}, … ϕ_{n} \begin{matrix}[α̃ ∧ (δ_{1} ∧ δ̃_{1} ∧ γ̃_{1} ≤ γ_{1}) ∧ (δ_{2} ∧ δ̃_{2} ∧ γ̃_{2} ≤ γ_{2})] → \\ (δ_{1} ∧ δ̃_{1} ∧ γ_{1} ≤ γ̃_{1}) ∧ (δ_{2} ∧ δ̃_{2} ∧ γ_{2} ≤ γ̃_{2}) \end{matrix}

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

Theorem: 17 Given a finitely axiomatizable theory A over a finite propositional language language L\overline{P}, a conditional circumscription policy, C = (\frac{γ_{1}}{δ_{1}} , …, \frac{γ_{n}}{δ_{n}}), where δ_{i}, γ_{i} ∈ L\overline{P}, then for every γ ∈ L\overline{P},

Circ_{C}(A; \frac{γ_{1}}{δ_{1}} , …, \frac{γ_{n}}{δ_{n}}) ⊧ γ

if and only if γ is true in all minimal models of A in the pre-order ≤_{\frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn}}.

1For notational simplicity we look at the case where we minimize two conditional formulas. The extension to n formulas is the natural one.

Proof:

We show the two propositions imply each other. We first note that both propositions imply that 𝔄 is a model of A. We then show the other conjuncts of both are inter-derivable. We assume that α is an axiomatization of A, and that there are n propositional letters in \overline{P}, denoted P_{1}, …, P_{n}. We also use the notation that a tilded formula denotes the substitution of ϕ_{i}s for the propositional letters.

Minimal_{≤^{Γ}↓_{A}}𝔄 ≡

∀𝔅.𝔅 ⊧ A ∧ (𝔅 ≤_{C_{\frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn}}} 𝔄) → (𝔄 ≤_{C_{\frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn}}} 𝔅) ≡ ∀𝔅.𝔅 ⊧ A ∧ (∀i ≤ n.(𝔅[δ_{i}] ∧ 𝔄[δ_{i}]) ∧ (𝔅[γ] → 𝔄[γ])) →

(∀i ≤ n.(𝔅[δ_{i}] ∧ 𝔄[δ_{i}]) ∧ (𝔄[γ] → 𝔅[γ])) ≡

∀ψ_{1}, …, ψ_{n}.[α[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}]∧

∀i ≤ n.(δ_{i} ∧ δ_{i}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}]) ∧ γ_{i}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}] ≤ γ_{i}] →
∀i ≤ n.(δ_{i} ∧ δ_{i}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}]) ∧ γ_{i} ≤ γ_{i}[ψ_{1}/P_{1}, …, ψ_{n}/P_{n}]) ≡

∀ψ_{1}, …, ψ_{n}.[α̃ ∧ ∀i ≤ n.(δ_{i} ∧ δ′_{i}) ∧ γ′_{i} ≤ γ_{i}] → ∀i ≤ n.(δ_{i} ∧ δ′_{i}) ∧ γ_{i} ≤ γ′_{i})

The first equivalence follows from the definition of Minimal. The second follows from the definition of ≤_{C_{\frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn}}}. 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 sentence is the second conjunct in the definition of circumscription.

Given the results of the previous chapter, it is clear that every conditional propositional circumscription can be captured by a regular propositional circumscription policy.

Theorem: 18 Let C = (\frac{γ_{1}}{δ_{1}} , …, \frac{γ_{n}}{δ_{n}}) be a set of pairs of formulas from L\overline{P}, a finite propositional language. Then, there exists a set of formulas Σ, such that

Circ_{C}(A; \frac{γ_{1}}{δ_{1}} , …, \frac{γ_{n}}{δ_{n}}) ≡ Circ(A; Σ)

Proof: Both circumscription correspond to partial orders on valuations. All partial orders are captured by regular circumscription, thus the backward direction is established. As regular circumscription is a special case of conditional circumscription, (when all the δs are valid), the forward direction is immediate.

However, just because two systems have the same expressive power does not mean that both are equally useful, or both are equally easy to use.

3.3.3 Compositionality and Elaboration Tolerance

Elaboration tolerance is a phrase introduced by McCarthy to capture the notion that certain theories are more easily modified, while others are more brittle. The less brittle a theory is, the more easily it can be adapted to slightly different situations, the more elaboration tolerant the theory is. Obviously the simplest case of a modification is conjoining new information. Thus a theory that can capture a large variety of new phenomena by conjoining new information is more elaboration tolerant that one that can not.

Elaboration tolerance can mean a great deal of different things to different people, but in this case, we say that a circumscriptive formalism for expressing defaults is elaboration tolerant, if when we add a new default, we can do so by adding something to the circumscription policy.

We now formally show that in this example circumscription is not elaboration tolerant in this regard, but that conditional circumscription is.

Example: 2 The expression of the default, “if Tarzan is with Jane, then he is usually happy” is expressed in circumscription, by minimizing ¬Happy ∧Jane, holding Jane fixed. We recall that fixing a formula can be achieved by minimizing both it and its negation.

Every other circumscription policy that has the same results, specifies the same pre-order. Holding Jane fixed is necessary. The other possible reading, minimizing Happy ∨ Jane^{2}, would conclude that being Happy and with Jane was more likely

2A referee suggested minimizing ab, with the axiom ¬Happy ∧ ¬ab → ¬Jane, which amounts to minimizing Happy ∨ Jane. This does not capture the default that Tarzan is more often Happy than sad, when he is with Jane.

than any other state. This is not what we intend, Tarzan might spend very little time with Jane, as he often needs to save jungle animals. On the other hand, given that Happy ≢ Jane, we do not wish to assume he is not with Jane.

We call the following pre-order ≤_{2}:

¬Happy, Jane Happy, Jane Happy, ¬Jane ¬Happy, ¬Jane

If α and γ are sentences of L_{{Happy,Jane}}, then

Circ(α; ¬Happy ∧ Jane, Jane, ¬Jane) ⊧ γ if and only if α ⊧_{≤_{2}} γ

Example: 3 The expression of the default, “if Tarzan is not happy, then he is usually not with Jane” is expressed in circumscription, by minimizing ¬Happy ∧ Jane, with Happy fixed.

We call this pre-order ≤_{3}:

¬Happy, Jane ¬Happy, ¬Jane Happy, ¬Jane Happy, Jane

If α and γ are sentences of L_{{Happy,Jane}}, then

Circ(α; ¬Happy ∧ Jane, ¬Happy, Happy) ⊧ γ if and only if α ⊧_{≤_{3}} γ Proposition: 19 The union of the two circumscription policies, minimizing ¬Happy ∧ Jane, holding Happy fixed, and minimizing ¬Happy ∧ Jane, holding Jane fixed, yields a trivial circumscription, namely the identity transformation on theories. The union of these two policies is minimizing ¬Happy ∧ Jane, holding Happy and Jane fixed.

If α and γ are sentences of L_{{Happy,Jane}}, then

Circ(α; ¬Happy ∧ Jane, ¬Jane, Jane, ¬Happy, Happy) ⊧ γ if and only if α ⊧ γ

Proof: We have held all propositions fixed, thus no valuation is comparable to any other.

To make the previous arguments more precise, we now note that any circumscription policy that generated the pre-order ≤_{2}, must have as minimized formulas the filters of ≤_{2}. Similarly, any policy that generates the order ≤_{3} will have the filters of ≤. However, it is immediate that the only pre-order that that has the filters of ≤_{2} and the filters of ≤_{3} as a basis is the discrete pre-order.

We now consider how we would write these defaults in conditional circumscription. Naturally, we could use the same defaults exactly, as conditional circumscription subsumes standard circumscription. However, we claim our intuition is that these defaults have a conditional property, namely that they should only be applied in certain cases.

Example: 4 The expression of the default, “if Tarzan is with Jane, then he is usually Happy” is expressed in conditional circumscription, by minimizing ¬Happy, when Jane is the case.

If α and γ are sentences of L_{{Happy,Jane}}, then

Circ_{C}(α; \frac{¬Happy}{Jane}) ⊧ γ if and only if α ⊧_{≤_{2}} γ

Note that the same pre-order on valuations could be generated by minimizing ¬Happy fixing Jane but this would capture the defaults that “if Tarzan is with Jane, then he is usually Happy” and “if Tarzan is with not Jane, then he is usually Happy”.

Example: 5 The expression of the default, “if Tarzan is not happy, then he is usually not with Jane” is expressed in conditional circumscription, by minimizing Jane, when ¬Happy is the case.

If α and γ are sentences of L_{{Happy,Jane}}, then

Circ_{C}(α; \frac{Jane}{¬Happy}) ⊧ γ if and only if α ⊧_{≤_{3}} γ

We now show that the union of these two defaults produces the correct result. This is to be compared with the previous case, where the union of the standard circumscription policies produced an unintuitive result.

Proposition: 20 The union of the two circumscription policies, minimizing Jane, when ¬Happy is the case, and minimizing ¬Happy, when Jane is the case yields the same results as the policy of minimizing ¬Jane ∧ Happy, Jane ∨ Happy, and Jane ∧ Happy.

If α and γ are sentences of L_{{Happy,Jane}}, then

Circ_{C}(α; \frac{¬Happy}{Jane} , \frac{Jane}{¬Happy}) ⊧ γ if and only if α ⊧_{≤_{1}} γ

Proof: Both policies correspond to the pre-order where ¬Jane ∧ Happy is related to no other state, and Jane ∧ ¬Happy is less preferred to the remaining two states.

Thus we have shown that in this example, we can represent defaults compositionally using conditional circumscription. The question now is, “Can we in general achieve compositionality?”

The next theorem shows that the answer is yes.

Theorem: 21 Given n pre-orders ≤_{i}, i ≤ n, on valuations of a finite propositional language L\overline{P}, such that ≤_{i}⊂≤_{j} when i ≤ j then there are n sets of conditional circumscription policies Γ_{i}, i ≤ n, such that ≤_{i}=≤^{Γ_{i}} and Γ_{i} ⊂ Γ_{j} when i ≤ j.

Proof: We can generate the pre-order ≤ by specifying one link at a time. We denote an axiomatization of the theory of a valuation 𝔄 as T_{𝔄}. This is where we use finiteness. If 𝔄 ≤ 𝔅, then we have \frac{T_{𝔄}}{T_{𝔄}∨T_{𝔅}} as a policy. If we choose Γ_{i} in this way, it is clear that Γ_{i} ⊂ Γ_{j} when i ≤ j, as in this case the pre-order has fewer links.

Thus in a precise sense, conditional circumscription allows us to specify defaults in an elaboration tolerant way. If we express our defaults using conditional circumscription, then we can add new defaults by adding new conditional circumscription instances to our policy.

It should be noted that in all this work we have looked at sequences of defaults that have strengthened the pre-order on models. There are natural sequences of defaults that do not have this property, but these questions lie outside the scope of this presentation. Here we consider only sequences of defaults that strengthen the preference relations.

3.4 First Order Case

We have defined conditional circumscription just for the propositional case. Here we state the definitions for the first order case. The only notable change is that the extension of the minimized formulas are compared with respect to subset inclusion, where before we compared their truth value with respect to implication.

Definition: 18 (⊧_{≤}) If ≤ is a pre-order on valuations of a first order language L, and α and γ are sentences in L, we say

α ⊧_{≤} γ

if γ is true in all the minimal models of α with respect to the pre-order ≤.

3.4.1 Semantics

We define the semantics of conditional circumscription in terms of minimal models. A conditional circumscription policy is a set of pairs of formulas of a first order language L. The first formula in a pair is called the condition, and the second the minimized formula. We say two L-structures 𝔐 and 𝔑 are in the relation ≤ if they have the same domain, and whenever a condition holds in both structures, the extension of the minimized formula in 𝔑 is a superset of the extension of that formula in 𝔐 The consequences of circumscription of a theory A are the sentences true in all minimal models of A under this pre-order ≤.

We can write this more formally as follows.

Definition: 19 ( ≤_{( \frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn})}) Given a first order language L, where P is the set of predicate letters, and a conditional circumscription policy, C = (\frac{γ_{1}}{δ_{1}} , …, \frac{γ_{n}}{δ_{n}}), where γ_{i}, δ_{i} are formulas in L, we define the pre-order on L-structures ≤_{( \frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn})} as follows. We use 𝔐[γ_{i}] to denote the extension of γ_{i} in 𝔐, considered as a set of tuples. If 𝔐 and 𝔑 are two L-structures, with assignments to all variables in L, and M and N their domains, then

𝔐 ≤_{C} 𝔑 iff \begin{matrix}M = N \\ 𝔐 ⊧ δ_{i} and 𝔑 ⊧ δ_{i} and 𝔐[γ_{i}] ⊆ 𝔑[γ_{i}] \end{matrix}

3.4.2 Conditional Circumscription Sentence

We can express these consequences as a second order sentence^{3}.

Definition: 20 (Circ_{C}) If (\frac{γ_{1}}{δ_{1}} , \frac{γ_{2}}{δ_{2}} ) is a pair of pairs of formulas of a first order language L, then we define the circumscription of a sentence α ∈ L minimizing γ_{1}, γ_{2} when δ_{1}, δ_{2} written Circ_{C}(α; \frac{γ_{1}}{δ_{1}} , \frac{γ_{2}}{δ_{2}} ) as follows.

α ∧ ∀ϕ_{1}, … ϕ_{n}

[ \begin{matrix}α̃ ∧ (∀x̄_{1}.((δ_{1} ∧ δ̃_{1})∧ \\ (∀ȳ_{1}.(γ̃_{1} ≤ γ_{1})))) ∧ (∀x̄_{2}.((δ_{2} ∧ δ̃_{2}) ∧ (∀ȳ_{2}.(γ̃_{2} ≤ γ_{2})))) \end{matrix} ] →

(∀x̄_{1}.((δ_{1} ∧ δ̃_{1}) ∧ (∀ȳ_{1}.(γ_{1} ≤ γ̃_{1}))))∧ (∀x̄_{2}.((δ_{2} ∧ δ̃_{2}) ∧ (∀ȳ_{2}.(γ_{2} ≤ γ̃_{2}))))

3For notational simplicity we look at the case where we minimize two conditional formulas, in a language without functions or constants. The extension to n formulas is the natural one.

We use α̃ etc. to denote the formula, α[ϕ_{1}/P_{1}, … ϕ_{n}/P_{n}], that is the replacement of the n predicates P_{i} by variables ϕ_{i}, that agree in arity and sort. x̄_{1} and x̄_{2} are the tuples of free variables occurring in δ_{1} and δ_{2} respectively, and ȳ_{1} and ȳ_{2} are the tuples of free variables occurring in γ_{1} or γ_{2}, and not occurring in δ_{1} or δ_{2} respectively.

It is important to note that the same variables may occur both in δ and γ, thus the universal quantifier over x̄_{1} in the above formula may bind variables in γ_{1}.

The proof that the semantics and syntactic definitions agree is essentially the same as the propositional case.

3.5 The Projection Problem

3.5.1 The Problem

To reason about change we clearly need to represent what changes after an action is completed. What is not so immediately obvious is that we also need to specify what does not change after an action. The simplest way to specify what changes and what does not would be to write each set of changes down. However this seems wasteful, and worse, seems likely to introduce inconsistencies. It seems clear that just specifying what changes is sufficient—everything else doesn’t change. We can generate the properties that do not change from the list of properties that do change. If we do this we are guaranteed that our lists will be consistent. Moreover, usually fewer things change than don’t change, and thus we will have much less to specify.

The idea that we need specify just the positive instances of change has given rise to a problem: How do we generate all the instances of properties that stay the same? This problem is known as the frame problem.

McCarthy’s original proposal to solve the frame problem was to minimize the change from one situation to the next. He did this by minimizing a predicate ab(a, f, s), which captured the notion that the fluent f changed when the action a was executed in situations s.

∀afs.¬ab(a, f, s) → (holds(f, s) ≡ holds(f, result(a, s)))  (3.1)

However, when this minimization is done, sometimes situations that differ on what properties hold are compared. This is like comparing apples and oranges, when we count changes, we should at least start from situations that agree on all properties. If they do not agree on all properties, they will naturally behave differently, and thus should not be compared.

Using this insight we look at how we can simply use circumscription to do temporal projection. We minimize the amount of change between situations, only comparing situations that agree on all fluents. This default is easily expressed using conditional circumscription.

3.5.2 The Situation Calculus

To look at reasoning about change we need a logical language to represent time, events, and the properties that hold in the world. We propose to use the situation calculus, a formalism for reasoning about events in the world. The paper that introduced situations (McCarthy and Hayes 1969) defined them as follows, “A situation s is the complete state of the universe at an instant of time”. The basic mechanism used in the calculus to define a new situation is the result function,

s′ = result(e, s).

In this formula s is a situation, and e is an event and s′ is a new situation that results when e occurs. The most common type of event is an action. The differences between events and actions has not yet been fully clarified. A function or predicate of a situation is called a fluent.

3.5.3 The Language of the Situation Calculus

The situation calculus of order n, L_{sit}^{n}, is a language of n^{th} order logic with equality, with three disjoint sorts: fluent names, actions, and situations^{4}. It contains exactly two predicate constants, holds, and ab in addition to equality, one function constant result(a, s) which returns a situation, and one situation constant SO, plus a set of fluent constants \overline{f}, and a set of action constants \overline{a}. When we wish to specify the action and fluent constants we write L_{sit}^{n}(\overline{f}, \overline{a}).

4We use s with primes and indices to range over situations, and a and f to range over actions and fluent names, and g to range over unary predicates of fluents.

3.6 Projection with Circumscription

Previous attempts by Shoham (1986b), Lin and Shoham (1991), Lifschitz (1986b), Lifschitz et al. (1995), Sandewall (1989a) and others (Haugh 1987, Reiter 1991, Pednault 1989) have the problem that they either map satisfiable theories to unsatisfiable theories, or they do not allow arbitrary theories—they restrict themselves to a very restricted class of sentences.

In a later chapter we give examples of theories which Shoham (1986b) and Lin and Shoham (1991) map to falsity, but which have natural interpretations. We note that this shows that their encoding of the semantic criterion they propose is inadequate for this case. We also consider why Lifschitz and Sandewall’s methods are restricted to theories which can be expressed as the conjunction of two sentences, one of which contains only situation constants, and the other which contains only variable situation terms.

Our solution does not have these problems, it is applicable to arbitrary theories. It minimizes the change between pairs of situations linked by an action. The novelty is that it only compares situations that agree on all fluents. It does not make sense to compare the amount of change between a situation where the gun is loaded when you shoot, and a situation where the gun is not loaded.

Therefore we write 𝔐 ≤ 𝔑 when, if we use 𝔐[P] to denote the interpretation of P in 𝔑, for every s,

⟨f′, s⟩ ∈ 𝔐[holds] iff ⟨f′, s⟩ ∈ 𝔑[holds] and ⟨a, f, s⟩ ∈ 𝔐[ab] implies ⟨a, f, s⟩ ∈ 𝔑[ab].

An equivalence, like the left hand side of the above is not immediately expressible in conditional circumscription. However, we can change an equivalence into a proposition, by using an auxiliary predicate variable g. ∀x.a(x) ≡ b(x) is equivalent to ∃g.(∀x.a(x) ≡ g(x)) ∧ (∀x.b(x) ≡ g(x)). This is now in the form of a conjunction of guard conditions, and can thus be expressed by conditional circumscription.

This is expressible in conditional circumscription as, \frac{ab(a, f, s)}{∀f.holds(f, s) ≡ g(f)}, where the g is a free predicate variable.

Definition: 21 (⊧_{proj}) Given a finitely axiomatizable theory A in the language of the situation calculus, we say that γ is a consequence of the temporal projection of the theory A, written A ⊧_{proj} γ when γ is entailed by the following circumscription.

Circ_{C}(A; \frac{ab(a, f, s)}{∀f′.holds(f′, s) ≡ g(f′)})

This seems simple, and also it seems to capture our intuitions. We now test this approach by looking at a few examples.

3.6.1 Examples

We look at the oldest canard of all, the Yale Shooting Problem.

The Yale Shooting Problem

The Yale Shooting Problem (YSP) is the problem of correctly predicting what happens in the following scenario. An individual named Fred is known to be alive, and a gun is known to be loaded initially. We know that shooting causes an individual to be not alive if the gun is loaded. We then want to infer that Fred will be dead after we wait, then shoot. In some solutions to the frame problem there are multiple minimal models, some where the gun becomes unloaded during the wait action, some where the shoot action kills Fred.

We axiomatize the Yale Shooting Problem as follows:

∀s.holds(loaded, s) → ¬holds(alive, result(shoot, s))  (3.2)

holds(alive, SO) ∧ holds(loaded, SO)  (3.3)

We now need unique name axioms for fluents, situations and actions, using the notation of Baker (1991).

UNA[alive, loaded] ∧ UNA[wait, shoot] ∧ UNA[result, SO]  (3.4)

The sentence that we should infer is:

¬holds(alive, result(shoot, result(wait, SO))))

Proposition: 22 If the theory A is the conjunction of 3.1, 3.2, 3.3, and the unique names axioms, over the language L_{sit}^{1}({loaded, alive}, {wait, shoot}) then

A ⊧_{proj} ¬holds(alive, result(shoot, result(wait, SO))))

Proof:^{5} We instantiate into the circumscription schema for the predicate holds′ with

λf s.if s = SO ∨ s = result(wait, SO) then true else if

s = result(shoot, result(wait, SO)) then f = loaded else holds(f, s)

Essentially, we instantiate into the circumscription schema with the intended interpretation.

5This has been mechanically verified using the PVS system (Owre et al. 1992), a higher order theorem prover developed at SRI.

The Walking Yale Shooting Problem

Some solutions to the frame problem have difficulty with domain constraints e.g. Lifschitz’s Formal Theories of Action (1987). An example of a domain constraint is that if one is walking then one is alive. We can write this as:

∀s.holds(walking, s) → holds(alive, s)  (3.5)

In this example we would like to derive that if Fred was walking initially then he will not be walking after the shoot, wait, load sequence. We state Fred was walking initially as follows:

holds(walking, SO)  (3.6)

We now need unique name axioms for fluents, situations and actions.

UNA[alive, loaded, walking] ∧ UNA[wait, shoot] ∧ UNA[result, SO] (3.7)

Proposition: 23 If A is the conjunction of 3.2 3.1, 3.3 3.5 and 3.6 and the unique names axioms over the language L_{sit}^{1} ({loaded, walking, alive}, {wait, shoot}) then

A ⊧_{proj} ¬holds(walking, result(shoot, result(wait, SO))))

Also

A ⊧_{proj} ¬holds(alive, result(shoot, result(wait, SO))))

Proof: We instantiate into the circumscription schema for the predicate holds′ with

λf s.if s = SO ∨ s = result(wait, SO) then true else if

s = result(shoot, result(wait, SO)) then f = loaded else holds(f, s)

3.6.2 Chronological Ignorance

Chronological ignorance was suggested by Shoham in his thesis (1986b). He suggested that change be put off for as long as possible. We look at an example motivated by Sandewall (1994), of a case where this is not intuitive.

Example: 6 We have an action of getting on a ferry, if ferry has already left then this action produces no change. Initially we do not know whether the ferry has left or not. Chronological ignorance will then prefer to think that we have missed the ferry.

We take as our language situation calculus, with the actions wait, and the fluents, onferry, and ferrypresent.

We can axiomatize this as follows:

¬holds(onferry, SO)  (3.8)
∀s.holds(ferrypresent, s) → (holds(onferry, result(board, s))  (3.9)

UNA[ferrypresent, onferry] ∧ UNA[result, SO]  (3.10)

We then have,

3.8, 3.9, 3.10 ⊧_{proj} holds(onferry, result(board, SO)) ≡ holds(ferrypresent, SO),

but not,

3.8, 3.9, 3.10 ⊧_{proj} holds(onferry, result(board, SO)

We can restate this with full information about the initial conditions if we wish, by introducing an under-specified wait action, that either waits one minute, or one hour. We imagine we have an alarm clock, that we set, and then we doze off. Our alarm clock is a little flaky, so it either rings after an hour or after a minute. In this case chronological ignorance will prefer that the wait action waits the longer time, so that we miss the boat.

Example: 7 We take as our language situation calculus, with the actions wait, and board, and the fluents, onferry, and ferrypresent, minute, and hour. The fluents minute and hour represent the fact that our alarm clock rang after a minute or an hour.

We then have the axioms:

(∀s.holds(ferrypresent, s) ∧ ¬holds(minute, s) →

(holds(ferrypresent, result(wait, s)) ∧ holds(minute, result(wait, s))))∨ (∀s.holds(ferrypresent, s) ∧ ¬holds(hour, s) →

(¬holds(ferrypresent, result(wait, s)) ∧ holds(hour, result(wait, s))))

(3.11)

Our timer cannot be set to both a minute and an hour.

∀s.¬(holds(minute, s) ∧ holds(hour, s))  (3.12)

And we have our initial conditions.

holds(ferrypresent, SO) ∧ ¬holds(onferry, SO)∧  (3.13)

¬holds(minute, SO) ∧ ¬holds(hour, SO)

UNA[ferrypresent, onferry, hour, minute] ∧ UNA[result, SO] ∧ UNA[wait, board] (3.14)

We then have,

3.13, 3.11, 3.9, 3.12, 3.14 ⊧_{proj} holds(onferry, result(board, result(wait, SO))) ≡ holds(ferrypresent, result(wait, SO)),

but not,

3.13, 3.11, 3.9, 3.12, 3.14 ⊧_{proj} holds(onferry, result(board, result(wait, SO))

Thus our solution correctly captures both of these problems.

3.6.3 Discussion

The proofs of the two Yale Shooting Problems above are rather simple. We instantiate into the circumscription schema for the predicate holds′ with

λf s.if s = SO ∨ s = result(wait, SO) then true else if  (3.15)
s = result(shoot, result(wait, SO)) then f = loaded else holds(f, s) (3.16)

A major advantage of this approach is that when we specify the new value of holds to be instantiated into the circumscription schema, we need only specify it at the situations up to the situation we are interested in. Every where else we can let it be equal to the predicate holds. As we only compare situations where holds and holds′ are equal, there is no difficulty in showing that there are less abnormalities in the future—either the situations agree, and thus there are equal abnormalities, or they do not agree, and are thus incomparable.

It should be noted that this approach does not have difficulties with disjunctions of observations and effect axioms. It never maps satisfiable universal theories to unsatisfiable theories. It can deal with non-determinism, as long as all outcomes are incomparable with respect to amount of change.

This approach is natural, and easily computed. It of course suffers from the problem that it can only do temporal projection. Later, in chapter 6, we look at causal reasoning, and problems that cannot be solved by pure projection.

3.7 Conclusion

We have shown that although formula circumscription can capture all pre-orders, it cannot do so compositionally. We introduce a new form of circumscription that allows defaults of the form, minimize γ when δ is the case. This form of circumscription has the same expressive power as formula circumscription, but it is compositional, in that every sequence of stronger pre-orders can be captured by a sequence of conditional policies, ordered by inclusion.

Finally, we showed that the method is natural, by exhibiting a simple solution to the problem of temporal projection, a classic test of non-monotonic reasoning systems. We tested this solution by mechanically verifying the classic examples, using a higher order theorem prover.

Domain Formula Circumscription

Summary

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. They are not an extension of domain circumscription—both are incomparable in expressive power.

We introduce a new form of circumscription that allows models that differ on domains to be compared. It thus extends both domain and predicate circumscription. It removes the artificial constraint that predicate and formula circumscription impose, and thus gives more intuitive semantics.

4.1 Introduction

Circumscription was introduced by 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. Mc-Carthy 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(see 8.1.6). Later forms never changed the possible domains Lifschitz(1985) of the theory^{1}—if the theory had a model with domain U, then the circumscribed theory would have a model of domain U.

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

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

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 37). 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 theory 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.

1This is only true if minimal models exist. However, we gloss over this point, as we are only interested in the case where minimal models exist.

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 10,12,24) of new defaults, that can be simply captured by the new theory, but cannot be captured by previous forms of circumscription.

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

4.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 (1980), and further investigated by Etherington and Mercer (1987).

Domain circumscription tries to capture the intuition that as few objects exist as possible. It attempts to carry out something like domain closure (Reiter 1987), 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.

2We use ϕ for unary predicate variables, ψ for predicate variables of arbitrary arity, β, γ, δ for formulas, 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.

Definition: 22 (Closed_{L}(ϕ)) 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.

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

Definition: 23 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: 24 The domain circumscription of a 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: 25 For a given language L and two L-structures, 𝔐 and 𝔑, we say that 𝔐 ≤_{domain} 𝔑, if and only if 𝔐 is a sub-model of 𝔑.

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

Bird(T weety) ∧ P enguin(Opus),  (4.1)
∀x.P enguin(x) → Bird(x).  (4.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 of (Lifschitz 1985) of removing second order quantifiers. We do this by instantiating the quantifier ∀ϕ by λx.x = T weety ∨ x = Opus.

2 Theorem due to: (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.

4.1.2 Predicate Circumscription

McCarthy introduced a new form of circumscription predicate circumscription (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: 26 ( ≤, and < 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 (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: 27 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:

Circ_{P} (α; P_{1}, P_{2}) ≡ α ∧ ∀ψ_{1}, ψ_{2}.¬ [α[ψ_{1}/P_{1}, ψ_{2}/P_{2}] ∧ ψ_{1}, ψ_{2} < P_{1}, P_{2}]

where ψ_{1} and ψ_{2} are predicate variables equal in arity to P_{1} and P_{2}.

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: 28 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 a \overline{P} -minimal model of α if and only if no other model of α is a \overline{P} -sub-model of 𝔐.

3 Theorem due to: (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 (1985).

Example: 9 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

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

4.1.3 Formula Circumscription

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 (1980).

Definition: 29 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 ψ_{1}.

We now introduce the semantics for formula circumscription.

Definition: 30 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}. We use ∥𝔐∥ to denote the domain of 𝔐. 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}.

4 Theorem due to: (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, and Circ_{F} (α; γ_{1}, …, γ_{n}; Z) ⊢ β then β is true in every γ_{1}, … γ_{n}; Z-minimal model of α.

4.1.4 Second Order Circumscription

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

DeKleer and Konolige prove (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: 31 (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: 32 (≤_{Γ}) 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.

4.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.

4.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: 33 (≤_{Γ;Δ} ) 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 set 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: 24 ≤_{Γ;Δ} is a pre-order.

Proof: This follow immediately from the transitivity and reflexivity of ⊂ and ⊃.

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

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

Lemma: 25 Let L be a first order language, Γ, Δ be two finite sets of formulas in L, and let 𝔑 be an L-structure. Let ∥𝔑∥ denote the cardinality of the domain of 𝔑, and B denote the domain of B for any 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, and whose domain is included in (B ∩ C) ∪ X, where X is a countable set. This is possible as our language 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.

𝔐[ϕ] ⊆ 𝔒[ϕ], as 𝔐 is an elementary sub-model. However, 𝔒[ϕ] ⊊ 𝔑[ϕ], by our assumption. Thus, 𝔐[ϕ] ⊊ 𝔑[ϕ], as required.

𝔑[ψ] ⊊ 𝔒[ψ], thus 𝔑[ψ] ⊆ 𝔒[ψ] ∩ (𝔑 ∩ 𝔒), as the elements must be in both models. Thus 𝔑[ψ] ⊊ 𝔐[ψ], as we can choose to have sufficient extra elements in 𝔐 to ensure the inequality.

4.2.2 Syntactic Form

We now need to introduce a condition analogous to the Closed_{L} condition(see page 56) 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: 34 ( 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 also add that the domains of the sorts in our theory must be countable. Finally we add that there are an infinite number of objects not in any of these predicates— these are the objects that we will be free to use to create alternate models.

Definition: 35 (inf) Let L be a first order language. We define inf(L) to be the sentence in the second order logic, that states that the extension of every sort in L is countable, and that there are an 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, x′. \begin{matrix}∀t.ζ(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))) \\ ∧∀ϕ.ϕ(x) ∧ ∀y.ϕ(y) → ϕ(ζ(y)) → ∀y.ϕ(y) \end{matrix}

The second order logic of Henkin, 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 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: 36 (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.

Example: 10 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}(α; λx; x; ) gives,

P (B) ∧ P (C) ∧ inf ∧ ∀ϕ.[P (B) ∧ P (C) ∧ ϕ(B) ∧ ϕ(C)∧
∀x.ϕ(x) → S(x)] → ∀x.ϕ(x) ≡ S(x)].

If we instantiate ϕ = λx.x = B ∨ x = C, we get

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

We now give an example where we vary the domain.

Example: 11 (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. We wish to minimize

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

and fix 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, as the intent is to provide witnesses rather than prevent crime.

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.

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))

4.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 vary the domain this no longer applies.

Example: 12 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; ) ≡ (∀x.P enguin(x) ≡ x = Opus)
Circ_{D}(α; ; ¬P enguin) ≡ (Joe ≠ T weety∧
(∀x.¬P enguin(x) ≡ x = T weety ∨ x = Joe))

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

Proof: Immediate from the example above.

Lemma: 27 Let L be a first order language, and 𝔐,𝔑 and 𝔒 L-structures. Let Φ, Ψ be finite sets of formulas in L.

If 𝔐 is less than 𝔑 in some pre-order on structures ≤_{Φ,Ψ}, then there is a model 𝔒 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 an L-structure 𝔐 as A. 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 can be extended to an elementarily embedding by adding a countable number of objects.

We now notice that this model 𝔒 is ≤_{Φ,Ψ} than 𝔑, 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: 28 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 27 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: 29 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: 30 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 (1977).

Proposition: 31 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: 32 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 ¬γ.

4.3 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 (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 (1958) and one due to Feferman (1974).

Definition: 37 (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: 38 (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 any conservative extension of A_{1}.

Theorem: 33 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: 34 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}).

4.4 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.

Cofinal Circumscription

Summary

Circumscription characterizes the non-monotonic consequences of a theory, as the sentences true in the minimal models of that theory under a pre-order. However, sometimes minimal models do not exist. 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 first look at what reasonable epistemic states are, in terms of pre-orders on models. We propose classes of models that are dense ideals of the pre-order. We then look at some properties of these choices, 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.

5.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 5.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 sentence is minimized, or made true of as few things as possible. The consequences of this minimization can be defined in terms of their 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 set of minimal models are the models for 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 1986b). 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 all sufficiently close worlds. 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, Shoham considered all possible preferences. He also considered using model preferences on other languages. An advantage of this proposal is that new preferences are allowed, (however no new preferences are gained in the propositional case (Costello 1996c)) 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.

5.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 these criticisms 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.

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

5.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 close value d to c we can always find a value of δ such that |x − e| < δ → |f(x) − c| < |d − 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 three cases in particular. The first example illustrates the need for a characterization of those properties that are true in a limit.

Example: 13 We assume we have a theory A, the real field, with an extra constant a, and another sentence,

a < 1.

We want to know what is true as a approaches the real number 1 from below. We have the usual relation < on real numbers. As an axiom we have a < 1, which states that a is less than 1.

We use the notation Circ(A; Γ) as in McCarthy(McCarthy 1986) to denote the result of circumscribing the theory A, minimizing the formulas Γ. To characterize the properties we wish to minimize the relation λy.y < x. We notice that

Circ(A; λy.y < x)

is not satisfiable, as there is no minimal model. For every choice of a, we can find a preferred model, one where the value of a is between our old choice and 1.

Our next 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 the computer is sufficiently fast—money is no object. The question is how we characterize the last assumption, that computer time is arbitrarily small.

Example: 14 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 is c. The question is whether a + b + c < t. We wish to minimize λx.x < c with the restriction that c > 0. Note that

Circ(T ∧ c > 0; λx.x < c)

is not satisfiable, as before there is 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: 15 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.

Now, as before, we wish to minimize ϵ. There are no minimal models.

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

5.2 Reasonable States of Belief

We now look at the question of what are the reasonable states of belief, given that we have some facts we consider true, and some ordering on states of the world that represents likelihood. We consider two conditions that we claim any reasonable state of belief should obey.

The first possible criterion we consider is that we 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. Models that are minimal in our ordering should always be included in our final class of models. The following propositions will all delimit the reasonable models, with respect to an ordering ≤, and a set of beliefs A.

Proposition: 35 (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: 39 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, M, and a pre-order ≤, then the class of models we select M′ should be dense with respect to ≤. This is the first criterion on states of belief that we propose.

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

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.

Definition: 40 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

Proposition: 37 (Ideal) Given a notion of ≤ on states of the world, and a class of states of the world M that are possible, the reasonable epistemic states should be an ideal of M with respect to ≤.

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.

We now question whether this notion of reasonable beliefs has certain consistency properties. We first note that the set of reasonable beliefs is closed under logical consequence from finite subsets.

Lemma: 38 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: 39 For a first order language L, and a consistent theory A stated in L, and a preference on L structures ≤, there is a non-empty class of models, M, that is the theory of the sentences true in any dense ideal of ≤↓_{A}.

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 there is a finite subset Γ′ = {γ_{1}, …, γ_{n}}, of Γ such that Γ′ ⊧ ϕ. Let a dense ideal that entails γ_{i} be denoted I_{i}. Then, by the above lemma, the intersection I′ = ⋂_{i≤n} I_{i} is a dense ideal. Further, every γ_{i} ∈ Γ′ is true in I′. Thus, ϕ is true in I′, and thus it is in Γ, as Γ is the set of all sentences true in some dense ideal. Thus the Γ 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.

We might strengthen our postulates by choosing the sentences true in any definable dense ideal, rather than true in some arbitrary dense ideal. We consider the consequences of this decision in the next section.

The next question we ask, is whether this choice is reasonable. As our first consideration we ask does this idea obey the structural rules suggested by Gabbay, and the rule Or suggested by Kraus, Lehmann and Magidor. We introduced this approach earlier in chapter 2.

Definition: 41 Let ⟨S, l, ≺⟩ be preferential model. If α is a formula, we shall say that some s ∈ S satisfies α if and only if l(s) ⊧ α. The set of all states that satisfy α will be denoted ∥α∥. We say a set of states models a formula, if every state in the set satisfies the formula.

A set of states is definable if it is the intersection of a set of sets of states, of the form α_{i}, for some index set I, that is, {∥α_{i}∥ |i ∈ I}.

A set of states S is an ideal if it is downwards closed, s ∈ S ∧ s′ ≺ s → s′ ∈ S. A set of states S′ is dense in a preferential model,⟨S, l, ≺⟩, with respect to another

set S′′, if ∀s ∈ S′′∃s′ ∈ S′′ ∩ S′.s′ ≺ s.

We say α ideally_{1} entails β in a model ⟨S, l, ≺⟩ if there exists a definable dense ideal of ≺_{↓∥α∥} that models β.

We say α ideally_{2} entails β in a model ⟨S, l, ≺⟩ if there exists a dense ideal of ≺_{↓∥α∥} that models β.

Theorem: 40 Ideal_{1} entailment is a preferential consequence relation.

Proof: We need to check each rule.

ID is immediate, as every α state models α.

LLE is immediate as if α ≡ β then the α states are exactly the β states.

RW is true as satisfaction on a set of states is defined classically.

Cut and CM are true as if a definable dense ideal I of ∥α∥ is included in ∥β∥, then I is a definable dense ideal of ∥β∥.

Or is true as a definable dense ideal of ∥α∨β∥ is included in some definable dense ideal of ∥α∥ and ∥β∥.

Theorem: 41 Ideal_{2} entailment is a preferential consequence relation.

Proof: We need to check each rule.

ID is immediate, as every α state models α.

LLE is immediate as if α ≡ β then the α states are exactly the β states.

RW is true as satisfaction on a set of states is defined classically.

Cut and CM are true as if a dense ideal I of ∥α∥ is included in ∥β∥, then I is a dense ideal of ∥β∥.

Or is true as a dense ideal of ∥α ∨ β∥ is included in some dense ideal of ∥α∥ and ∥β∥.

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

Definition: 42 A consequence relation Γ |∼ γ is consistency preserving exactly when, if Γ is consistent, then every γ, such that Γ |∼ γ, is consistent.

Theorem: 42 Ideal_{1} entailment is consistency preserving. Ideal_{2} entailment is consistency preserving.

Proof: This follows the analysis of theorem 39, and the fact that Ideal_{1} entailment is strictly weaker than Ideal_{2} entailment.

5.3 Advantages and Disadvantages

We have produced two suggestions as ways that minimal model semantics could be modified so that it would be consistency preserving. We now look a the special case where we maximize domains, as a way of sharpening our instincts as to what is the more natural of the two proposed solutions.

We now look at an analogue of domain circumscription, which was introduced in McCarthy(McCarthy 1977). Domain circumscription minimizes the domain. It captures the assumption that as few objects exist as possible. In some cases this is a reasonable assumption, however, at other times we wish to be more profligate. Sometimes the correct default to make is that as many objects as possible exist.

Domain circumscription is analogous to mathematical induction. It states that the objects that exist are the smallest set satisfying the given conditions. This notion is widely used in metamathematical definitions—the set of terms and the set of formulae of a language are defined as the smallest set closed under certain operations.

We now introduce a operation on theories that is analogous to algebraic closure. Taking the algebraic closure of a field, or the real closure of an ordered field is a natural operation. The metamathematical dual of this is taking the model completion of a theory.

Definition: 43 (model completion) Let A, A^{∗} be L-theories. A^{∗} is a model completion of A if and only if,

• Every model of A is embeddable in every model of A^{∗} and vice-versa; • A∗ is model complete;

• If 𝔄 ⊧ A, then A^{∗} ∪ Diagram(𝔄) is complete.

The last clause is related to the uniqueness of the algebraic closure. In many cases we do not want completeness. Induction is most normally used to give a unique set, but domain circumscription often does not give a unique model. In the same way we do not want want uniqueness in this case. Therefore we define the weaker notion, of model companion, a theory which satisfies the first two notions above. Luckily, a theory has at most one model companion (Robinson 1963). However, it is not guaranteed to have a model companion.

We now give some mathematical examples of model companions, and then we consider some more common-sense notions.

5.3.1 Examples

\begin{matrix}Example: 16 \\ • \end{matrix} Every field has a model completion, the corresponding algebraically closed field.

• The model completion of an ordered field, is the real closed field.

• The model companion of a formally real fields is the real closed field, but we note that this is not unique, and hence is not a model completion.

• The model completion of any boolean algebra is an atom-less boolean algebra.

• Algebraically closed fields of fixed characteristic have no model companion.

We now look at some common-sense examples.

Example: 17 Baker (1991) suggests adding an existence of situation axiom to the situation calculus. This states that a situation of every type exists. If we consider the fragment of the situation calculus which contains fluents, and not situation constants or the result function, adding an existence of situations axiom corresponds to taking the model companion of the theory.

Example: 18 It is often natural to consider what objects are possible. In this case we wish add all the objects that could possibly exist. McCarthy’s first example of domain circumscription was that in the missionaries and cannibals problem (Amarel 1968). Here, we wish to assume there is no bridge. It is easy to see another attitude to this problem might want to consider the possibility of a bridge. Adding these objects is the same as taking the model companion.

Example: 19 If we wish to consider worst possible cases in planning we should add all possible other agents that might disrupt us. If we consider this problem from the standpoint of process algebra it is clear why we should take the algebraic closure or model companion in this case.

We now look at a way of constructing model companions. We see that it corresponds to adding all the Σ_{1} sentences to A that do not imply Π_{1} sentences not implied by A. We show that this in general is as good a way of making model companions as we can find.

Definition: 44 (existentially closed) A theory A is existentially closed exactly when if 𝔄 is a model of A, and ∃x.ϕ is a Σ_{1} sentence such that 𝔄 ⊧ ∃x.ϕ then for all 𝔅, models of A such that 𝔄 ⊇ 𝔅, 𝔅 ⊧ ∃x.ϕ.

Fact: 43 Note the direction if 𝔄 is a model of A, and 𝔄 ⊧ ∃x.ϕ then for all 𝔅, models of A such that 𝔄 ⊆ 𝔅, 𝔅 ⊧ ∃x.ϕ, is trivial as existentials are preserved under super-models.

We now refer to a theory by Keisler (1978).

Theorem: 44 (Keisler (1978) ) Let A be an inductive theory. If the class of all existentially closed models of A is elementary, then a model is a countable existentially closed model of A if and only if it is a model companion.

Thus, the model companions companion can be characterized, in this case, as the result of adding all existential Σ_{1} sentences that do not entail a Π_{1} sentence that is not already entailed by A. Alternately it can be characterized as the intersection of the theories that are maximal with respect to Σ_{1} sentences. We recall that the class of models characterized by Σ_{1} sentences, relative to a theory A, are those classes closed under superstructures. Thus we can rephrase the above theorem as, if the class of all existentially closed models of A is elementary, then the model companion is the theory of the smallest class of models that is a definable dense ideal of the pre-order generated by the super model relation.

We further note that in a strong sense the above result is the best possible characterization.

Theorem: 45 (Eklof and Sabbagh (1971)) A has a model companion if and only if the class of all existentially closed models of A is elementary.

Thus, our first form of circumscription, ideal_{1} entailment, when applied to maximizing domains, constructs the model companion, if it exists. We now see that it is a rather weak notion, in that it adds only existentials, and thus is local in a very strong sense.

This should be compared to McCarthy’s circumscription which, when applied to Robinson arithmetic, produces the theory of true arithmetic, a theory that is not r.e., and which is not even arithmetical. Thus, circumscription adds sentences of arbitrary quantifier nesting, while ideal_{1} entailment adds only existential sentences.

It might seem strange that minimizing the domain of Robinson arithmetic, using ideal_{1} entailment, should produce a weaker theory than minimizing the domain using ideal_{2} entailment, as in both cases the pre-order has a unique minimal model, the model of true arithmetic. However, the strongest theory that is closed under submodels, is by necessity, axiomatized by existentials, relative to Robinson arithmetic, while the theory of true arithmetic is not.

We therefore choose as our natural consequence relation for circumscription that a sentence is true in some dense ideal, ideal_{2} entailment. We now show that it agrees with McCarthy’s definition in all cases where minimal models exist.

Proposition: 46 If there exist minimal models, with respect to ≤, that are ≤ than every model in M, then the theory of the minimal models of M is the set of sentences Γ = {ϕ|∃I.I ⊧ ϕ and I is a dense ideal }.

Proof:

The minimal models are a dense ideal. There are also the smallest dense ideal. Therefore the theory of the minimal models is the set Γ.

Thus, ideal_{2} entailment co-incides exactly with circumscription when enough minimal models exist. We note that it does not co-incide with circumscription in all cases where circumscription returns a satisfiable theory.

5.4 Second Order Characterizations

Now that we have chosen to use ideal_{2} 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.

5.4.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 the 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 46. 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. Thus by making this change we ensure that the semantics are always defined.

We call our new version Cofinal Circumscription.

Semantics of Cofinal Circumscription

We will redefine the semantics so that they do not assume minimal model 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}}, be the maximized formulas.

Definition: 45 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: 46 (⊧_{≤_{Φ,Ψ}^{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 its smaller models satisfy ϕ.

A ⊧_{≤_{Φ,Ψ}^{Cofinal}} ϕ =^{def}  (5.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: 47 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.

5.4.2 Formal Systems

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: 47 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 γ = α → β 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 γ, that is, (γ^{ϕ_{1}})^{ϕ_{2}}.

Definition: 48 ((Z, S) <_{Φ,Ψ} (Z′, S′)) Given a sorted second order language L, and two finite sets of formulas in L, Φ, Ψ, we define the following notation:

(Z, S) ≤_{Φ,Ψ} (Z′, S′) ≡
∀\overline{x_{1}}.ϕ_{1}^{S}(\overline{x_{1}}) → ϕ_{1}[Z/Z′]^{S′}(\overline{x_{1}})∧
… ∧ ∀\overline{x_{n}}.ϕ_{n}^{S}(\overline{x_{n}}) → ϕ[Z/Z′]^{S′}(\overline{x_{n}}))
∧ ∀\overline{y_{1}}.ψ_{1}^{S′}(\overline{y_{1}}) ← ψ_{1}[Z/Z′]^{S′}(\overline{y_{1}})∧
… ∧ ∀\overline{y_{o}}.ψ_{n}^{S}(\overline{y_{o}}) ← ψ[Z/Z′]^{S′}(\overline{y_{o}}))

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 Φ = {ϕ_{i}|i ≤ n} and Ψ = \{ψ_{i}|i ≤ o\}, 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: 49 (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: 50 (inf) We define inf(L) to be the sentence that states that the extension of every sort in L is countable, and that there are an 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, x′. \begin{matrix}∀t.ζ(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))) \\ ∧ ∀ϕ.ϕ(x) ∧ ∀y.ϕ(y) → ϕ(ζ(y)) → ∀y.ϕ(y) \end{matrix}

Definition: 51 (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:

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}]

Lemma: 48 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: 49 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 pre-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 can be extended to an elementarily embedding by adding a countable number of objects.

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: 50 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

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

Proof:

Lemma 48 shows that ≤_{Φ,Ψ} exactly captures ≤_{Φ,Ψ}^{Cofinal}. Lemma 49 shows that for first order consequences we need only consider models that add a countable new set of objects. Cofinal circumscription adds a countable set using inf, thus this lemma applies, and the two definitions agree.

We again stress that it is necessary that the circumscription be a schema. If we rewrote it as with a second order quantifier, we would allow instantiations that were not first order definable. However, second order logic is not compact, and thus lemma 47 does not apply. In fact circumscription defined using second order quantification maps satisfiable theories to unsatisfiable theories.

5.4.3 Comparison with Other Work

The idea of using entailment in all minimal models as a model for non-monotonic reasoning was introduced by McCarthy (1977). He used it to give semantics to circumscription. Lewis, earlier, in a slightly different field, noticed that problems arose if we made the assumption that there was a minimal model, or in his terms a closest possible world. Bossu and Siegel did not make this assumption, but their minimality criterion was very restrictive. They considered only the case where all predicates are minimized. Shoham (1986b) generalized the preferences that are allowed but argued that sufficiently minimal models were not intuitive.

We claim that cofinal sentences are intuitive and the obvious choice for circumscription. We show that the semantics of circumscription can be redefined to consider cofinal sentences, the sentences true in some dense ideal, rather than the sentences true in minimal models. Our formal system is not particularly more complicated than regular circumscription.

5.4.4 Conclusions

We have introduced a new semantics for circumscription. It has one new principal feature—it does not assume a minimal model, rather it looks for sentences true in some 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 non-existent 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. As assuming minimal models is a strong and unnecessary assumption we claim that moving to variants defined in terms of cofinal sentences is the correct choice.

The Frame Problem

Summary

The frame problem—representing the default that the only effects of actions are those mentioned—is a central problem in knowledge representation. This default can be captured, using circumscription, by minimizing the set of change formula that are true, where a change formula is a formula that states that, under certain circumstances, an event causes a fluent to change its value. This approach handles domain constraints and arbitrary disjunctions correctly, unlike previous proposals. It applies a single circumscription policy to the entire theory, rather than use ad-hoc methods that depend on applying several circumscriptions or splitting up the theory before circumscription is applied.

The consequences of the circumscription formula can be calculated using a higher order theorem prover. The correctness of the approach on the standard examples has been verified in this way.

We give intuitive examples that our solution correctly models, that are modeled by no other proposed solution. The benefit of this solution over previous attempts is that it uses an intuitive idea, minimizing effects, that has been widely accepted by the community since STRIPS. Furthermore, it applies to arbitrary theories, not just to particular syntactic forms, thus showing that it is not a special case solution.

6.0.5 Frame Axioms

As we mentioned earlier, a certain problem arises when we formalize domains in this language. Assume there is an axiom that states what happens to the location of a block when an action move is performed. If another property, colour, is added, the axiom which described what effect the action had on the location does not give us any information on what happens to the new fluent colour. The usual intent is that the new fluent remains unchanged by the action, but this is not always the case. To specify that the colour of the block does not change we must write:

∀x c s.holds(colour(x, c), s) → holds(colour(x, c), result(move(x, l), s))

To express all the fluents that do not change, an axiom would be needed for each action/fluent pair. These axioms stating that fluents do not change are called frame axioms. Having to specify all this lack of change seems extravagant, and more importantly it seems unnecessary to have to write these out individually. It seems that it should be possible to generate these frame axioms automatically. The frame problem is the problem of characterizing these frame axioms.

6.0.6 Non-monotonic Logic

We cannot hope that classical logic will generate the frame axioms for us, as classical logic is monotonic and will not infer any sentence that might be denied by an additional fact. Thus we will have to use a logic without this property, a non-monotonic logic.

Non-monotonic logics are logics which can make default assumptions which can be withdrawn later. We are looking at an assumption, “the tendency of facts to endure over time” (Hanks and McDermott 1986). This seems to be exactly the sort of problem at which non-monotonic reasoning should excel.

6.0.7 What a solution should generate

Ideally our non-monotonic logic should generate all of the frame axioms. If we look at an action that has preconditions, such as

∀x l s.holds(movable(x), s) → holds(at(x, l), result(move(x, l), s))

we should get the frame axiom:

∀x l s. ¬holds(movable(x), s) → (holds(at(x, l), s) ≡ holds(at(x, l), result(move(x, l), s)))

We should have a frame axiom whenever there is no action whose preconditions are met that changes the fluent. We can write this as

If there is no action, all of whose preconditions are met, that changes the fluent f then the value of the fluent f should remain the same.

This is a statement of the common sense law of inertia. If this is to generate enough frame axioms, we must assume that actions have as few effects as possible. Therefore we must look at how we represent the effects of actions.

If an action a causes a fluent f to be false when the set of fluents P are all true, and the fluents N are all false, then we write:

∀s. ⋀_{f_{i}∈P} holds(f_{i}, s) ∧ ⋀_{f_{j}∈N} ¬holds(f_{j}, s) → ¬holds(f, result(a, s))

This does not tell us whether the action a changed f, as f could have been false initially, i.e. in N. The sentence that tells us just the negative changes that the action a makes, is:

∀s. ⋀_{f_{i}∈P} holds(f_{i}, s) ∧ ⋀_{f_{j}∈N} ¬holds(f_{j}, s) ∧ holds(f, s) → ¬holds(f, result(a, s))

Every sentence of this form tell us about a particular change that an action causes. If we want to assume that actions have as few effects as possible, we must have as few of these sentences true as possible. If we have a minimal set of these change sentences, then the additional fact that all changes are describable in this way we will generate all the frame axioms we need.

6.1 A Natural Solution

We consider a certain subset of the formulas of our language, namely those that imply a change occurred. These we call change formula. We consider the following as our definition of a change formula:

Definition: 52 (change formula) A change formula is a formula in the language L_{sit}^{2}(\overline{f}, \overline{a}) that is an instance of the following schemas:

∀s. ⋀_{f_{i}∈P} holds(f_{i}, s) ∧ ⋀_{f_{j}∈N} ¬holds(f_{j}, s) ∧ holds(f, s) → ¬holds(f, result(a, s)),

∀s. ⋀_{f_{i}∈P} holds(f_{i}, s) ∧ ⋀_{f_{j}∈N} ¬holds(f_{j}, s) ∧ ¬holds(f, s) → holds(f, result(a, s)),

where f is an element of \overline{f}, P and N are subsets of \overline{f}, and A is an element of \overline{a}.

We note that the axioms that described change which we considered earlier had this form. Further, we note that the fluents, and actions in these formulas may have free variables. Therefore, the formula,

∀s.holds(movable(x), s) ∧ ¬holds(at(x, l), s) →
holds(at(x, l), result(move(x, l), s))

is a change formula.

We now define ab_{1} and ab_{2} as syntactic sugar, so that conjunctions of abs correspond to instances of change formulas. More correctly, every change formula is equivalent to a conjunction of abs.

The change formulas defined above contain two disjoint sets of fluents, P and N. Rather than deal with two sets, we can consider just the case where P is the complement of N. We then only need to consider one set. We use a second order predicate variable to capture this set. We lose no expressive power by this, as every change formula is equivalent to a (possibly infinite)^{1} conjunction of these formulas. We do however gain simplicity by eliminating one of the sets of fluents, which allows for simpler reasoning.

ab_{1}(a, f, g) ≡^{def}

∀s.(∀f′.g(f′) ≡ holds(f′, s)) ∧ holds(f, s) → ¬holds(f, result(a, s)),

ab_{2}(a, f, g) ≡^{def}

∀s.(∀f′.g(f′) ≡ holds(f′, s)) ∧ ¬holds(f, s) → holds(f, result(a, s)).

(6.1)

Now that we have written our change formula as instantiations of a pair of second order logic sentences we can minimize all change formulas by minimizing these sentences.

We can now our Common Sense Law of Inertia as a second order sentence in terms of the shorthands ab_{1} and ab_{2},

∀a f s.holds(f, result(a, s)) ≡
(∀g.¬[ab_{1}(g, f, a) ∧ (∀f′.g(f′) ≡ holds(f′, s)] ∧ holds(f, s))∨
(∃g′.ab_{2}(g′, f, a) ∧ ∀f′.g′(f′) ≡ holds(f′, s))).

We have written this in the form of explanation closure. In this form it is obvious what the role of ab_{1} and ab_{2} are. They encode the preconditions for an action causing a change.

This sentence can be greatly simplified however. Its content is that change is deterministic. Thus we can simplify it to,

∀a f_{1} s s′. (∀f.holds(f, s) ≡ holds(f, s′)) ∧ holds(f_{1}, result(a, s)) → holds(f_{1}, result(a, s′)).  (6.2)

This says that if situations agree on all fluents then they behave in the same way. We now need unique name axioms for fluents and actions and our function sit,

UNA[\overline{f}] ∧ UNA[\overline{a}] ∧ UNA[sit].  (6.3)

1The fact that these conjunctions might need to infinite is not of concern, as we are going to minimize the abs not use them to represent particular change formulas.

We have introduced a function sit here, which maps sets of fluents to situations. This exists to guarantee that the domain of situation will be large enough. Circumscription does not compare structures that have different domains, thus in the absence of an assertion that there are more than one situation, our solution will have models with only one situation.

Definition: 53 (⊧_{frame}) The consequences of a problem theory A under the frame assumption, written ⊧_{frame}, are the consequences of,

Circ ( A ∧ 6.2 ∧ 6.3; ab_{1}, ab_{2} ) .

Theorem: 51 The function induced by ⊧_{frame} solves the frame problem.

Proof:

There is no model of the theory A with fewer changes caused by actions. There is no change except in the case that an action caused the change by virtue of 6.2. Thus the only changes are those that are implied by statements that actions change certain fluents when preconditions are met. But this is exactly the statement of the frame problem.

It is important to note that we implicitly used domain formula circumscription here. This is the role that the function sit plays. It expands the domain so that we avoid the models with small domains that would otherwise cause problems.

6.2 Baker’s Solution

We now present a solution to the frame problem proposed by Baker (1991). We show that our new solution differs from Baker’s solution in certain examples. We also show how his existence of situations assumption naturally arises from our minimization.

Baker suggested that the ab introduced by Hanks and McDermott (1986) be minimized, but that the function symbol result and the constant SO be varied instead of the predicate symbol holds.

∀a f s.¬ab(a, f, s) → holds(f, s) ≡ holds(f, result(a, s))  (6.4)

Baker’s first suggestion was to add an existence of situations axiom monotonically. Later he suggests that the existence of situation axioms can be generated non-monotonically. Baker suggests adding a new predicate absit(g). He adds an axiom defining how sit behaves:

∀g.¬absit(g) → ∀f.g(f) ≡ holds(f, sit(g))  (6.5)

He adds unique names axioms, our axiom 6.3. We now have the tools to define Baker’s solution.

Definition: 54 ⊧_{Baker} Given a problem description T in the language L_{sit}^{1}, let the consequences of the problem description T under Baker’s system, written ⊧_{Baker} be the consequences of,

Circ(T ∧ 6.4 ∧ 6.5 ∧ 6.2 ∧ 6.3; absit)∧
Circ(T ∧ 6.4 ∧ 6.5 ∧ 6.2 ∧ 6.3; ab, absit, ¬absit).

We note that we have added the axiom that change is deterministic. As Kartha (1994) has shown that Baker’s solution does not deal correctly with non-determinism, we feel this is justified.

This solution seems to give the intuitive results. Strong evidence for this is that Kartha has shown that Baker’s solution agrees with several semantic frameworks developed by Gelfond and Lifschitz (1992, 1993), Kartha (1994, 1995), Baral and Gelfond (to appear)and others, called A, AR etc. for certain restrictions of problem descriptions. Kartha (1993) also shows that A agrees with various other procedural ways of generating frame axioms proposed by Reiter (1991), Pednault (1989), Schubert (1990) and others. Thus he shows that the procedural ways agree with Baker’s solution for this restricted set of theories.

This solution does not agree with the solution we presented earlier. The main difference seems to be that if we have disjunctions of domain constraints and effect axioms, Baker’s solution will prefer to make the domain constraint false, and thus assert the effect axiom, while our approach will have models where the domain constraint is true, and the effect axiom false as well as the model Baker’s solution gives. We feel this is more natural, as there seems no justification for minimizing domain constraints with more priority than effect axioms. It seems that because Baker minimizes absit first, it is minimized with higher priority.

Example: 20 If your Grandmother could ever be truly happy, passing your exams

would do it. Let T be the theory,

(∃s.holds(Happy, s)) → (∀s.holds(Happy, result(P ass, s))).

Note this is equivalent to a domain constraint disjoined with an effect axiom.

( ∀s.¬holds(Happy, s)) ∨ (∀s.holds(Happy, result(P ass, s))).

Then,

T ⊧_{Baker} (∃s.holds(Happy, s)),
T ⊧_{Baker} (∀s.holds(Happy, result(P ass, s))),
T |̸=_{frame} ∃s.holds(Happy, s),
T |̸=_{frame} (∀s.holds(Happy, result(P ass, s))).

We find our interpretation more likely, as we consider it possible that our grandmother may never be truly happy.

However, for a large class of theories, Baker’s solution agrees with this solution. If we take theories with domain closure for fluents, that do not have disjunctions of domain constraints and effect axioms, we get the same results.

Theorem: 52 Let A be a theory consisting of disjunctions of compatible effect axioms (i.e change formulas that do not imply a domain constraint) and observations(sentences without situation variables), and a set of domain constraints (sentences with one universally quantified situation term), then, if ϕ ∈ L_{sit}^{1} then,

A ⊧_{frame} ϕ if and only if A ⊧_{Baker} ϕ

Proof:

A domain constraint, ∀s.ψ(s), is equivalent to a pair of change formulas, ∀s.¬ψ(s) → holds(f, result(a, s)), and ∀s.¬ψ(s) → ¬holds(f, result(a, s)). If minimizing the domain constraints—Baker’s existence of situations does not imply any change formulas, then we may minimize absit first, without affecting the result.

6.3 Other Solutions

6.3.1 Monotonic Solutions

This solution has benefits over the so-called monotonic solutions to the frame problem. They currently cannot deal with arbitrary domain constraints. However, every domain constraint is equivalent to a pair of effect axioms. Note that a domain constraint ∀s.ϕ(s) is equivalent to the conjunction of two effect formulas, ∀s.¬ϕ(s) → holds(F, result(A, s)) and ∀s.¬ϕ(s) → ¬holds(F, result(A, s)). Thus, these solutions do not deal correctly with domains axiomatized entirely by effect axioms. However, even when the axiomatization does not contain effect axiom that imply a domain constraint there are still problems. In particular, approaches that posit a scheme of induction over situations cannot model certain domains.

We first consider a simple problem in reasoning about change, When we describe examples, we give a story, and then a set of axioms that we claim model the story. We do not use loaded phrases like “loaded” as our fluent names, as the examples we give are not, and should not be, dependent on what the fluents actually represent. We claim that any interpretation of the fluents should give the results we predict. We do give stories however, as an intuition pump as to what the theories might be applied. In each example we will use the satisfaction relation ⊧_{frame}, so that each example can be taken as a partial description of this relation.

We have one action, wait. After carry out a wait action, we notice that the Moon is not made of green cheese. We further believe that if the Moon is not made of green cheese, then there is no way to make it into green cheese. From these facts, and the frame assumption we would like to infer the Moon was not made of green cheese originally.

We have one action making our hero walk a mile. After walking a mile we notice that he is hungry. We know that if you are not hungry and you walk a mile, then you will be hungry. We infer that our hero may or may not have been hungry originally.

Example: 21 The first example concerns reasoning backwards in time. For simplicity we consider a language with only one action A, and one fluent-name F. We are told that F holds at the second situation, result(A, S0). We are also told a frame axiom, namely that if F holds, then it holds after we do A. Thus our two axioms are:

holds(F, result(A, S0))

∀s.holds(F, s) → holds(F, result(A, S0))

(6.6)

We consider that a conclusion that should be drawn from this theory, if we assume the Law of Inertia is:

6.6 ⊧_{frame} ∀s.holds(F, s)  (6.7)

We have another axiom:

∀s.¬holds(F, s) → holds(F, result(A, s))  (6.8)

We consider that the non-monotonic conclusions of this axiom, and the first should be:

6.6, 6.8 ⊧_{frame} ∀s.holds(F, result(A, s))  (6.9)

Thus these two theories have distinct consequences.

In general, if we are given a theory, which has a model where there is no change, we claim that the Law of Inertia should choose the theory of that model as our non-monotonic conclusions.

Several researchers have proposed solving the frame problem by succinctly writing down the frame axioms.

Normally effect axioms are written in the form:

∀s.ϕ_{A}^{+}(s) → holds(F, result(A, s))

∀s.ϕ_{A}^{−}(s) → ¬holds(F, result(A, s))

They noted that effect axioms can be written down in the form:

∀as.holds(F, result(a, s)) ← (a = A_{1} ∧ ϕ_{A_{1}}^{+}(s))∨ ; ⋮ ; ∨(a = A_{k} ∧ ϕ_{A_{k}}^{+}(s))∨ ; holds(F, s) ∧ ¬(a = A_{1} ∧ ¬ϕ_{A_{1}}^{−}(s))∧ ; ⋮ ; ¬(a = A_{n} ∧ ¬ϕ_{A_{n}}^{−}(s))

They noticed the solution to the frame problem was to turn the → into an equivalence. Given a set of effect axioms, one for each fluent F, we define the explanation closure of this set of effect axioms to be the set of sentences that result from turning → into ≡. Thus the above sentence would become:

∀as.holds(F, result(a, s)) ≡ (a = A_{1} ∧ ϕ_{A_{1}}^{+}(s))∨ ; ⋮ ; ∨(a = A_{k} ∧ ϕ_{A_{k}}^{+}(s))∨ ; holds(F, s) ∧ ¬(a = A_{1} ∧ ¬ϕ_{A_{1}}^{−}(s))∧ ; ⋮ ; ¬(a = A_{n} ∧ ¬ϕ_{A_{n}}^{−}(s))

Given a theory T, we write Exp(T) for the theory we get by explanation closure. Given a theory T and a sentence ϕ we write T ⊧_{mon} ϕ if and only if, Exp(T) ⊧ ϕ.

Lemma: 53 6.6 ⊧_{mon} 6.7

6.6, 6.8 ⊧_{mon} 6.9

Proof: By conversion into the form for explanation closure.

Induction

Reiter has proposed adding an axiom of induction over situations. This axiom restricts the models of the situation calculus to just those models that have as their situations, S0, and the situations reachable from it by a finite number of actions. We can write this as:

∀ϕ.ϕ(S0) ∧ (∀a s.ϕ(s) → ϕ(result(a, s))) → ∀s.ϕ(s)  (6.10)

We reject this axiom as if we add it to situation calculus theories, it conflates theories that we think should be treated differently. We saw in the previous example that the theory 6.6,had a different result from the theory 6.6 and 6.8. However, if induction 6.10 is added to these two theories we get the same theory. Lemma: 54

6.6, 6.10 ≡ 6.6, 6.10, 6.8  (6.11)

Proof: We note we can derive 6.8 by instantiating ¬holds(F, s) → holds(F, result(A, s)) for ϕ in 6.10. The first conjunct of the left hand side is the case as we know that holds(F, result(A, S0)). The second conjunct follows as we know that either holds(F, s) or ¬holds(F, s). In either case we can derive holds(F, result(A, s)).

Given a consequence relation ⊧′, if ⊧ is first order validity, we denote the rule \frac{⊧ ϕ ≡ ψ, ϕ ⊧′ χ}{ψ ⊧′ χ} as (LLE) for Left Logical Equivalence.

Definition: 55 (⊧_{Reiter}) We define the consequence relation Reiter proposes as follows. Given a set of sentences T, that contains the induction axiom 6.6, then if T′ is T − 6.10, we define

T ⊧_{Reiter} ϕ ⟺ Exp(T′) ∧ 6.10 ⊧ ϕ

Theorem: 55 ⊧_{Reiter} is not closed under (LLE).

Proof: By lemma 6.11, 6.6, 6.10 ≡ 6.6, 6.10, 6.8, but by lemma 53, 6.6 has different consequences than 6.6, 6.8. Thus logically equivalent sets of sentences have different consequences.

Thus Reiter’s suggestion of adding induction contradicts our examples, thus we reject the addition of induction.

A similar complaint can be made against the recently proposed action languages (Giunchiglia et al. 1995) that take functions defined on sequences of actions as their models, rather than functions on sets of fluents.

6.3.2 Hand-crafted Second Order Axioms

Lin (1991), and Lin and Shoham (1992), and Lin and Reiter (1994), have proposed solutions to the frame problem that use a hand-crafted second order sentence, rather than a circumscription policy. This solution can also be seen as the result of quantifying over a circumscription. This solution maps satisfiable theories to contradiction. This occurs in simple theories using only disjunction of effect axioms. Neither Baker’s nor my method becomes inconsistent in these cases.

Lin and Shoham’s approach

Lin and Shoham in (1991, 1995) suggest a different approach to formalizing change. They assume a language L_{sit}^{2} + ab(a, f, s) + holds′(f, s)^{2}. They only consider theories of a very restricted form.

2This is a slight simplification. They also consider a predicate symbol frame(f), which is used to express to which fluents inertia is applied. Lifschitz discusses this at length in (Lifschitz 1991).

They also use formula circumscription, which we change to predicate circumscription by considering their shorthand ab as a predicate symbol.

The theories they consider are theories that can be axiomatized by domain constraints, that is formulas, whose sole predicate symbol is holds, with exactly one situation term, a situation variable that is universally quantified, and by effect axioms, as we defined earlier.

Rather than restrict ourselves to theories of that sort we consider arbitrary (finitely axiomatizable) theories stated in L_{sit}^{1}.

Lin and Shoham use the following formula in defining their consequence relation:

∀f.(holds(f, s) ≡ holds′(f, s))  (6.12)

We now state the unique names axioms Lin and Shoham use. If the fluent names are exactly f_{1}, …, f_{n} and the actions are a_{1}, …, a_{l} then

UNA[f_{1}, …, f_{n}] ∧ UNA[a_{1}, …, a_{l}] ∧ UNA[SO, result]  (6.13)

We add domain closure for fluents and actions. If the fluent names are exactly f_{1}, …, f_{n} and the actions are a_{1}, …, a_{l} then:

∀f.(f = f_{1}) ∨ … ∨ (f = f_{n})  (6.14)
∀a.(a = a_{1}) ∨ … ∨ (a = a_{k})  (6.15)

Their definition of ab is as follows. Note that this has the variable s free:

∀a f.¬ab(a, f, s) → (holds(f, s) ≡ holds(f, result(a, s)))  (6.16)

Definition: 56 If Li is the conjunction of the sentences 6.12, 6.13 6.14 and 6.15 and 6.16, and T is a finitely axiomatizable theory of L_{sit}^{1}, and ϕ is a sentence in L_{sit}^{1} then the consequences of the problem description T in Lin and Shoham’s system, written ⊧_{Lin}, as defined as follows:

T ⊧_{Lin} ϕ ≡ ∀s.Circ(T ∧ Li; ab(a, f, s); holds)) ⊧ ϕ

We again stress that Lin and Shoham only proved that this method was correct when applied to theories of a very restricted form. In (Lin and Shoham 1995) they argued that what they hoped was that this would be a basis for developing theories of action that allow a broader class of reasoning.

The following is a simple example of a theory, which Lin’s systems map to falsity, while Baker’s and our solution handle correctly. Our next example concerns a disjunction of actions. We have an exclusive disjunction of two effect axioms.

We have a secretary. She never comes to work on Monday, Wednesday or Friday. She also comes to work every Tuesday or every Thursday, but not both. Our action is next, which brings us to the next work day. If we have fluents for each day, and a fluent atwork, we would expect two models, one where the days pass in the normal way, and the secretary is atwork only on Tuesdays, the other where she is atwork only on Thursdays.

Example: 22 We have six fluents, F_{1} to F_{5} represent the days of the week, while F_{w} is being at work, and one action A. We have the axioms^{3}:

∀s.holds(F_{1}, s) → holds(F_{2}, result(A, s)) ∧ ¬holds(F_{1}, result(A, s)),
∀s.holds(F_{2}, s) → holds(F_{3}, result(A, s)) ∧ ¬holds(F_{2}, result(A, s)),
∀s.holds(F_{3}, s) → holds(F_{4}, result(A, s)) ∧ ¬holds(F_{3}, result(A, s)),
∀s.holds(F_{4}, s) → holds(F_{5}, result(A, s)) ∧ ¬holds(F_{4}, result(A, s)),
∀s.holds(F_{5}, s) → holds(F_{1}, result(A, s)) ∧ ¬holds(F_{5}, result(A, s)),
∀s.holds(F_{5}, s) ∨ holds(F_{2}, s) ∨ holds(F_{4}, s) → ¬holds(F_{w}, result(A, s)),
(∀s.holds(F_{2}, s) → holds(F_{w}, result(A, s)))⊕
(∀s.holds(F_{4}, s) → holds(F_{w}, result(A, s))),
∀f.holds(f, SO) ≡ f = F_{1}.

(6.17)

The models we expect include the sentence:

6.17 ⊧_{frame} (∀s.holds(F_{w}, s) ≡ ∃s′.s = result(A, s′) ∧ holds(F_{4}, s′))∨ (∀s.holds(F_{w}, s) ≡ ∃s′.s = result(A, s′) ∧ holds(F_{2}, s′)) (6.18)

3⊕ represents exclusive disjunction

The interpretation of F_{1} to F_{5} is the days of the week, and the interpretation of F_{w} is atwork in the story we told.

Theorem: 56 Lin and Shoham’s solution to the frame problem maps example 22 to falsity.

6.17 ⊧_{Lin} ⊥

Proof: We instantiate twice into the outermost universal quantifier, once with S0, the other with result(wait, result(wait, S0)), namely Monday and Wednesday. In the first case when we circumscribe we deduce that she did not work Tuesday, in the second case we deduce she did not work Thursday. This contradicts the fact we know she works one of those days.

The reason things have gone wrong here is that we have tried to minimize locally at a particular situation, when our minimizations have can have global effects. We might hope to see all these global effects passed through in the form of a change at the situation at which we are minimizing. This example is crafted so that the problematic situations are already completely specified by the axioms. Thus the information that needs to be passed through, whether the secretary went to work on Tuesday, cannot be seen from the fact she is not at work on Wednesday.

The example only contains a exclusive disjunction, and presents no problem for our intuitions. It therefore seems that Lin and Shoham’s solution is simply not tolerant of disjunction in any form.

6.3.3 Why we need disjunction

Lin has suggested that circumscriptive approaches give unintuitive effects in the presence of disjunction by ruling out the third case. As the example holds even for problems with exclusive disjunction, this argument does not seem compelling

Certain researchers have argued, in personal communication, against the counterexamples listed above, claiming that the formalisms were never intended to deal with disjunction. I would claim that that is perhaps the main point of these examples. If formalisms cannot deal with disjunction, then they are not capable of dealing with the vast majority^{4} of all logical sentences. They are no longer general logical formalisms, rather they are treatments of very special cases.

Sandewall’s systems (1989a, 1989b, 1994) are based on filter preferential entailment. Lifschitz and Kartha (1995) bases their system on nested abnormality theories. Both these formalisms have the property that they necessarily divide the theory the are non-monotonically completing into subsets, based on some syntactic property. In particular they divide observations from causal rules or effect axioms. However, if a causal rule is disjoined with and effect axiom this cannot be achieved.

Preferential Entailment

Sandewall uses the term filter preferential entailment to denote a type of semantic entailment. He imagines a case where we have a theory divided into two parts, Γ and Γ_{0}. He divides the theory into two sets of sentences, so he can apply a selection function to one set, and then conjoin the other set to get the final theory. If ζ is a selection function, that is it maps a set of models to a subset of those models, then the non-monotonic consequences of Γ and Γ_{0} are Γ ∪ ζ(Γ_{0}).

Nested Abnormality Theories

Lifschitz in (1995) suggest a very similar idea to Sandewall’s. Rather than describing the idea in semantic terms, Lifschitz uses the notation of circumscription.

He divides his theory into several parts. To each part he applies a circumscription. He does this uniformly by defining the predicate ab, of an appropriate arity to be predicate to be minimized. All predicates are varied by default. The novel idea that he adds is that he allows these theories to nest, and so the result of a circumscription can itself be circumscribed.

4Logic without disjunction either reduces to conjunction being the only connective, or implication or negation as the only connective, both of which are essentially trivial. Any two of the connectives ∧ → and ¬ can define all the other connectives.

A Counterexample

Our next example uses disjunction again. This time, rather than a disjunction of effect axioms, we use the disjunction of an effect axiom with a fact about the world.

We walk into a room. The light is on. Therefore we know that, either walking into the room causes the light to turn on, or the light was on initially.

Example: 23 We have action A and one fluent F. We have the axioms:

holds(F, S0) ∨ ∀s.holds(F, result(A, s))  (6.19)

We would like to infer that walking into a room does not turn the light on:

6.19 ⊧_{frame} holds(F, S0) ∧ ¬∀s.holds(F, result(A, s))

If we are told that the light was not on initially, we should assume that walking into the room turns the light on.

6.19, ¬holds(F, S0) ⊧_{frame} ∀s.holds(F, result(A, s))

Our example 23 gives a natural problem where we need to disjoin information of these two types. Neither Sandewall’s or Lifschitz’s methodology is applicable to this natural class of problems.

Theorem: 57 Sandewall’s system cannot model example 23

Proof: The sentence 6.19 is neither an observation nor a causal rule and thus fits into neither of the classes of formulae Sandewall treats.

Theorem: 58 Any nested abnormality theory that divides effect axioms from sentences involving closed situation terms cannot model 6.19.

Proof: Immediate from the form of 6.19.

Definition: 57 In theories of action, restricted monotonicity can be defined as follows. Let P be the set of sentences of L_{sit} which have only closed situation terms, that is which do not contain situation variables. A theory of action stated in L_{sit}^{1}, and a consequence relation ⊧_{frame}, satisfy the restricted monotonicity condition, if for every subsets p, q of the set P , such that p ⊂ q and every theory T it is the case that,

{ϕ|T, p ⊧_{frame} ϕ} ⊂ {ϕ|T, q ⊧_{frame} ϕ}

Theorem: 59 ⊧_{frame} denies restricted monotonicity.

Proof: Let p be ∅ and q be ¬holds(F, S0), and T be 6.19, then we know that

6.19 ⊧_{frame} holds(F, S0)

From the example 23. From monotonicity we know that:

6.19, ¬holds(F, S0) ⊧_{frame} ¬holds(F, S0)

As 6.19, ¬holds(F, S0) has a model, we know that:

6.19, ¬holds(F, S0) |̸=_{frame} holds(F, S0).

Therefore, we do not have a ⊂ relationship. .

6.4 Examples

The standard examples against which any solution to the frame problem must be tested are the Yale Shooting Problem, (YSP), the YSP with ramifications, and the Stanford Murder Mystery, an explanation problem, essentially the YSP where we reason backwards in time.

6.4.1 The Yale Shooting Problem

The Yale Shooting Problem (YSP) is the problem of correctly predicting what happens in the following scenario. An individual named Fred is known to be alive, and a gun is known to be loaded initially. We know that shooting causes an individual to be not alive if the gun is loaded. We then want to infer that Fred will be dead after we wait, then shoot. In some solutions to the frame problem there are multiple minimal models, some where the gun becomes unloaded during the wait action, some where the shoot action kills Fred.

We axiomatize the Yale shooting problem as follows:

∀s.holds(loaded, s) → ¬holds(alive, result(shoot, s)),  (6.20)

holds(alive, SO) ∧ holds(loaded, SO).  (6.21)

The sentence that we should infer is:

¬holds(alive, result(shoot, result(wait, SO))).

Theorem: 60 We note that the if the theory T is the conjunction of 6.20 and 6.21, and unique names axioms for fluent and actions, over the language L_{sit}^{1}({loaded, alive}, {wait, shoot}) then

T ⊧_{frame} ¬holds(alive, result(shoot, result(wait, SO)))).

Proof: We instantiate the circumscription schema with the following values.

holds(f, s) =^{def} if ∃g.s = sit(g) then g(f) else holds(f, s)

result(a, s) =^{def} if ∃g.s = sit(g) then ( if g(loaded) ∧ g(alive) ∧ a = shoot then sit(λf.g(f) ∧ f ≠ alive) else s) else result(a, s)

SO =^{def} sit(λf.f = loaded ∨ f = alive)

We then simplify to derive,

∀a f s. (holds(f, result(a, s)) ≢ holds(f, s)) ≡ (holds(loaded, s) ∧ holds(alive, s) ∧ a = shoot ∧ f = alive)

Note that our final result does not assume that there are only four situations, nor that there are exactly as many situations as set of fluents. The only restriction in the size of the domain of situations is that it is greater than the number of sets of fluents.

6.4.2 The Walking Yale Shooting Problem

Some solutions to the frame problem have difficulty with domain constraints e.g. Lifschitz’s Formal Theories of Action (1987). An example of a domain constraint is that if one is walking then one is alive. We can write this as,

∀s.holds(walking, s) → holds(alive, s).  (6.22)

In this example we would like to derive that if Fred was walking initially then he will not be walking after the wait, shoot sequence. We state Fred was walking initially as follows,

holds(walking, SO).  (6.23)

Theorem: 61 We note that the if T is the conjunction of 6.20 6.21 6.22 and 6.23,and unique names axioms for fluent and actions, over the language L_{sit}^{1} ({loaded, walking, alive}, {wait, shoot}) then

T ⊧_{frame} ¬holds(walking, result(shoot, result(wait, SO)))).

Also

T ⊧_{frame} ¬holds(alive, result(shoot, result(wait, SO)))).

CHAPTER 6. THE FRAME PROBLEM 118

Proof: We instantiate the circumscription schema with the following values. holds(f, s) =^{def} if ∃g.s = sit(g) then g(f) else holds(f, s)

result(a, s) =^{def} if ∃g.s = sit(g) then ( if g(loaded) ∧ g(alive) ∧ a = shoot then sit(λf.g(f) ∧ f ≠ alive ∧ f ≠ walking) else s) else result(a, s)

SO =^{def} sit(λf.f = loaded ∨ f = alive)

We then simplify to derive, ∀a f s. (holds(f, result(a, s)) ≢ holds(f, s)) ≡ (holds(loaded, s) ∧ holds(alive, s) ∧ a = shoot∧ (f = alive ∨ f = walking))

6.4.3 Explanation

We now consider reasoning backwards in time. If we know that after waiting and shooting that Fred was dead, and that he was alive initially, we should derive that the gun must have been loaded initially,

holds(alive, SO) ∧ ¬holds(alive, result(shoot, result(wait, SO)))). (6.24)

The sentence that we should infer is:

holds(loaded, SO).  (6.25)

Theorem: 62 We note that the if the theory T is the conjunction of 6.20 and 6.24,and unique names axioms for fluent and actions, over the language L_{sit}^{1}({loaded, alive}, {wait, shoot}) then

T ⊧_{frame} holds(loaded, SO).

Proof: We instantiate the circumscription schema with the following values.

holds(f, s) =^{def} if ∃g.s = sit(g) then g(f) else holds(f, s)

result(a, s) =^{def} if ∃g.s = sit(g) then if g(loaded) ∧ g(alive) ∧ a = shoot then sit(λf.g(f) ∧ f ≠ alive) else s) else result(a, s)

SO =^{def} sit(λf.f = loaded ∨ f = alive)

We then simplify to derive,

∀a f s. (holds(f, result(a, s)) ≢ holds(f, s)) ≡ (holds(loaded, s) ∧ holds(alive, s) ∧ a = shoot ∧ f = alive)

These three problems have been mechanically verified using a higher order theorem prover, the PVS system (Owre et al. 1992), developed at SRI.

6.5 Advantages

One of the main advantages of this method from the point of view of theorem proving, is that a finite domain of situations can be used to find the minimal models. In the Yale Shooting example above, we can use the model with four situations. In some examples, we shall need to use more.

6.6 Other Work

The first set of solutions to the frame problem, which proposed preferring change that happened as late in time as possible, were by Lifschitz (1986b), Shoham (1986a, 1986b, 1987b, 1987a, 1988b, 1988a, 1988, 1987c), and Kautz (1986, 1985). These solutions are now grouped under the heading of chronological minimization, a term suggested by Shoham. It is worthwhile noting that these solutions did not change the basic default, the preference was still to assume that change happened as few times as possible, but a preference between defaults at different times was expressed. These solutions all suffered from the flaw that they only worked correctly when predicting the future—temporal projection—the standard example of when they fail is when we are told some fact about the future that we would not have predicted. This was pointed out early on by Lifschitz and Ginsberg.

The next set of solutions was those based on “causal” minimization. Haugh and Lifschitz introduced formalisms with a “causes” predicate that captured the notion that “in the intended model, all changes in the values of fluents are caused by actions, whereas in other models this is not the case” (Lifschitz 1987). The main drawbacks of this approach are that it does not allow us to write our axioms in the unrestricted situation calculus, rather we must use the “causes” predicate when it is appropriate. Because of this restriction it is not clear how to add domain constraints or ramifications to this formalism. These points were expressed by Baker (1991). The major advance of these theories from the present author’s point of view is that they rejected minimizing the total amount of change, and rather minimized causality.

The next important solution was proposed by Baker (1991). His method is more robust than many other methods—it deals correctly with reasoning backwards in time and reasoning about domain constraints. He suggested returning to the idea that the total amount of change is minimized. Baker claims that because the abnormality predicate takes a situational argument, the meanings of situations should be held constant across models that are compared. He claims that varying the function result that picks out the situation after an action is performed, rather than varying what fluents hold at each situation, captures this intuition.

In order for his method to work it is necessary to add an existence of situations axiom, that states that every possible combination of properties holdsat some point in time. Baker does not justify this from intuition, but rather states that it is needed to make the formalism work. We have shown that this axiom comes about naturally as a result of minimizing change axioms.

Lin and Shoham (1991, 1992) suggested a solution that again returned to minimizing the total amount of change, but they suggested that this should be minimized one situation at a time. Their solution can be explained as follows. For every situation, and possible set of fluents that could hold at that situation, they calculate what the minimal amount of change between that situation and its successors could be. They then add the conditional that if those fluents held at the situation, then the successors will be exactly those that have minimal differences. This approach was extended by Lin and Reiter (1994). The major drawback with this approach is that it can become inconsistent when we are given disjunctive information. However, Lin and Shoham show that it behaves correctly for a limited class of theories, essentially those where what holdsin the initial situation uniquely determines what is holdsin all later situations.

Kartha and Lifschitz (1995) based on the work of Winslett (1988), also suggested that a solution could be achieved by considering change one situation at a time. The disadvantages to this work are that it involves changing the language of situation calculus quite drastically. It also is based on circumscribing parts of the theory, and thus treats the theory as if it had extra internal structure. No semantics are given for this extra internal structure. As we saw earlier, this proposal cannot deal with disjunctions of effect axioms and observations.

In addition to the work that has used non-monotonic logics, Gelfond and Lifschitz have suggested using logic programming, and have introduced various languages A etc., that have a computational interpretation. Lifschitz (1993), and Kartha and Lifschitz (1994), and Giunchiglia et al. (1995) have extended these languages moving away from the computational aspects towards a minimal model paradigm. They give no semantics to their statements about change, and thus it is difficult to evaluate what their theory says about change. Gelfond and Baral (to appear) have extended A in the direction of logic programming, while McCain and Turner (1995) have looked more closely at the declarative interpretation of the sentences of A and at how domain constraints can imply preconditions, an issue we have not addressed.

Monotonic descriptions of the frame axioms have also been developed by Reiter (1991), Pednault (1989), Schubert (1990), and originally Hass (1986). These methods of generating the frame axioms worked on the syntactic form of the theory. As we mentioned earlier they cannot handle ramifications, and thus cannot handle effect axioms that are incompatible

6.7 Caveats

The methodology this paper proposes for reasoning about change is by no means ideal. In particular it does not address the problems that arise when we reason about non-determinism, concurrent action, strategies, or the qualification problem.

6.8 Conclusion

We present a simple solution to the frame problem that adds only a statement of determinism and unique names axioms to the problem statement. Our solution can be defined using nothing more than standard circumscription. Like McCarthy’s original proposal it varies holds, but rather than minimize the amount of change, it minimizes the amount of change formulas.

It applies a single circumscription policy to the entire theory. In this it is superior to the suggestions of Baker, and Kartha and Lifschitz. It correctly handles disjunctions, differing from all previous approaches on certain examples. On these examples our solution gives the intuitive results.

Conclusion

Finally we conclude, with a recap of the goals, the problems that were faced, and the new ideas and achievements of this thesis.

7.1 Goals

The goal of this thesis was to develop non-monotonic reasoning, based around the notion of preference, so that it could usefully be used to describe defaults. Several hurdles stood in our way. These difficulties ranged from broad methodological quandaries—we did not know how to describe certain defaults, to specific technical problems with certain non-monotonic systems—the failure of consistency preservation in circumscription.

In order to more clearly delineate the achievements of this thesis, the various problems that needed to be addressed before we applied a non-monotonic system to defaults in the common sense world are recapitulated.

7.1.1 Consistency Preservation

Many non-monotonic systems, such as circumscription map satisfiable theories to unsatisfiable theories. Some researchers, such as Shoham (1986b), claimed that this was natural, even beneficial. I strongly disagree with this attitude. Inconsistency results in the total loss of all information. It should be avoided at all costs, if there is a reasonable way to do this.

Kraus, Lehman and Magidor suggested considering one smooth orders on worlds. This has the advantage that it ensures consistency preservation, as long as all worlds are ordered. However, it has one major drawback. There is no reason to think that the natural pre-orders that we will come across in the world will be smooth. Thus, insisting on smoothness seems an arbitrary restriction.

The answer to this conundrum is simple however. Smoothness is a by-product of looking at the world in a particular way. If we look at the sentences true in some dense ideal, or alternately, the models of the sentences true in all cofinal models, then we can always find a smooth order that would give the same results.

Perhaps, the smallest definable set of models that contain a dense ideal, is not as obvious or natural a solution as the set of minimal models. Perhaps it is more natural. Dense ideals are a very reasonable characterization of those states of belief that are rational, given a particular order. It we believe a state possible, should we not believe all more likely states possible? If we discount a world, should we not believe that there is a more likely world than it? We should only reject a world as unlikely in the face of a possible alternative. This is exactly the property of density. Choosing the smallest definable set, is the natural way of looking for the most aggressive attitude that we can take in jumping to conclusions.

In short, the smallest definable set of models that contain a dense ideal, is a natural and concise description of how to provide consistency preserving reasoning, without all of the strange epistemological baggage that smoothness properties entail.

7.1.2 Naturality

Semantics should be natural. This of course is a movable feast, everyone has their own ideas about what is most natural, and in particular an author always finds his ideas natural. However, even given this, there are certain properties that do seem more common in more natural systems.

The first of these is that arbitrary restrictions are suspect at best. Every clause in a definition should have some epistemic grounding.

Another sign that a system is natural is simplicity. The more simple a system, the more likely that it will correspond to our intuitions. Though it is not of course obvious a-priori, it seems that humans are most comfortable with relatively simple mathematical structures.

The final test for naturality that I propose, is mathematical sophistication. This might seem to run counter to the test of simplicity, however, the richness of a mathematical structure is often evidence that it is an important and powerful way of approaching reasoning.

7.1.3 Domains and Equality

Propositional logic has no problems with equality or with domains. Neither occur in its semantics. This advantage is lost however when we move to first order logic. We are then forced to address the issues that domains raise. Much of the work in non-monotonic consequence relations, and in auto-epistemic logic ignores these issues by staying focussed on the propositional case. This is not a long term solution.

Equality should be treated as just another predicate. Special restrictions on how equality should be used are very un-natural. In the same way, there is no epistemic justification for assuming a particular fixed domain. Perhaps the simplest way to express my mistrust of the idea of fixing the domain to be some Herbrand universe, is to point out that this reduces the problem back to the propositional case.

Treating the domain and equality as normal predicates implies that we ensure our semantics do not make unnecessary assumptions about the equality of terms, nor about the cardinality of the domain. Circumscription originally did not allow models with domains of different cardinality to be compared. It is necessary to drop this assumption to gain a reasonable treatment of the first order case.

7.1.4 Contingent Defaults

Defaults are often very naturally expressed as a binary notion. We often think of a default as being of the form “if … is the case, then usually … ”. This should be contrasted with “usually if … then … ”, which is not the same idea at all.

These propositions have very different meanings, at least when the left hand side is usually false. The first then means that in that unusual situation, it so happens that the seconds conditions is the case. The other proposition says that an implication is usually the case. The canonical example of penguins and flying make this eminently clear. It seems reasonable to believe that usually a bird flies or is not a penguin. In fact we would probably assent to the stronger belief that usually birds fly, without the other disjunct. However, we do not assent to usually penguins fly.

Thus a goal of this thesis is to allow us to easily represent information of this kind.

7.1.5 Expressive power

No logic can be said to be truly useful unless a sound and complete semantics for it are understood. Circumscription has long had a semantics—truth in minimal models. However, the expressive power of circumscription was unknown. Other systems, like non-monotonic consequence relations have semantics that are subtly different from circumscriptions semantics. This thesis attempts to answer why this is the case, and to explain why these formalisms differ, and why they seem alike.

7.2 Summary

Rather than tackle each problem piecemeal, we started from the intuition that defaults could be naturally captured by orders on models of the world.

We then looked at the first order case. Circumscription was modified, so that it could represent preferences between models that differed on their domains. It was then shown that we could look at the smallest definable set of models that contain a dense filter, rather than the minimal models. This set always exists, and thus allows us to defined circumscription so that is always preserves consistency.

We can represent defaults in an elaboration tolerant way, by stating exactly when they are applicable.

After showing that previous solutions were inadequate, an analysis of why this was the case was presented with properties that every solution must satisfy. This gives a natural solution to the frame problem. A mechanical verification that the solution was correct on the standard examples was performed.

Overall non-monotonic reasoning, based around the idea of preference was developed. The range and power of the systems introduced was precisely characterized, and it was shown that they overcame the problems that beset earlier approaches.

Change was used as the major domain for showcasing the results.

Appendix

8.1 Other Modifications of Circumscription

8.1.1 Hintikka

Hintikka (1988) suggests model minimization as an alternative to domain circumscription. Rather than prefer one model to another when the second is a sub-model 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 (1994) calls this variable domain circumscription. Doherty, Lukaszewicz and Szalas (1996) suggest an extension, general domain circumscription, where subsets of the predicates functions and constants are allowed to vary.

8.1.2 Bossu and Siegel

Bossu and 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.

8.1.3 Shoham

Shoham (1988b) 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, Makinson 1994) and others, an area outside the remit of this paper.

8.1.4 Rathmann, Winslett and Manasse

Rathmann, Winslett and 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. (1994), but then the original ideas of Goguen and Burstall’s (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.

8.1.5 Other Suggestions

Minker and Perlis (1984) suggest protected circumscription, which modifies circumscription in an analogous way to allowing predicates to be varied. 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 (1989) 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 (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 work. Besnard, Moinard, and Mercer (1989) stress the importance of the extra expressive power that full circumscription gives over non-recursive circumscription.

Lifschitz (1986a) 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 regular circumscription (Lifschitz 1989).

8.1.6 Nested Abnormality Theories

Lifschitz (1995) suggests a formalism, which he calls Nested Abnormality Theories. He uses this to capture the domain closure assumption. The domain closure assumption is the assumption that every object is represented by a ground term.

McCarthy (1980) suggests that domain circumscription can be captured by predicate circumscription by the following method. He introduces a new unary predicate All. He then adds that all constants are true of this predicate, and that for all n-ary function constants,

∀x_{1}, …, x_{n}.All(x_{1}) ∧ … ∧ All(x_{n}) → All(f(x_{1}, …, x_{n})).

Then the theory, with these additions is circumscribed, minimizing All. The final result is got by conjoining ∀x.All(x) to the result of the circumscription.

This is not the same as domain circumscription, in fact, it is a purely monotonic operation.

Definition: 58 (⊧_{all}) We say a sentence α in a first order language L models a sentence γ ∈ L under all-domain circumscription exactly when,

[Circ(α ∧ C ∧ F; All) ∧ ∀x.All(x)] ⊧ γ,

where C is the sentence that states all constants in L are true of All and F is the sentence that states, for all n-ary function constants,

∀x_{1}, …, x_{n}.All(x_{1}) ∧ … ∧ All(x_{n}) → All(f(x_{1}, …, x_{n})).

Proposition: 63 If L is a first order language and α and γ are sentences in L, then

α ⊧_{all} γ if and only if α ∧ CF ⊧ γ,

where CF is the following sentence:

∀ϕ. ⋀_{c∈C} γ(c) ∧ ⋀_{f^{n}∈F} ∀x_{1}, …, x_{n}.ϕ(x_{1}) ∧ …

∧ϕ(x_{n}) → ϕ(f(x_{1}, …, x_{n})) → ∀x.ϕ(x)

Proof: The two second order formulas are inter-derivable by movement of quantifiers. .

Proposition: 64 All-domain circumscription is not equivalent to domain circumscription.

Proof: Let L be the first order language with one unary predicate P, and a constant B. Let α be the sentence ∃x_{1} x_{2}.x_{1} ≠ x_{2}.

DomCirc(α) ≡ ∃x_{1} x_{2}.x_{1} ≠ x_{2} ∧ ∀x_{1}x_{2}x_{3}.x_{1} = x_{2} ∨ x_{1} = x_{3} ∨ x_{2} = x_{3}

α ⊧_{all} ⊥

.

Thus all-circumscription does not capture domain circumscription. This is also an argument against Lifschitz’s use of Nested Abnormality Theories, as he uses allcircumscription as one of his examples as to the utility of his approach. As allcircumscription is monotonic, this approach does not seem to hold much promise.

When we introduced domain formula circumscription, we only looked at the domain. The other question that remains, is how do we treat equality. We now show that it has naturally been captured by the modification we have made.

8.2 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.

8.2.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: 24 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.

8.2.2 Etherington, Mercer and Reiter

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.

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

6 Theorem due to: (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.

8.2.3 McCarthy’s Suggestion

We look at McCarthy’s suggestion (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: 59 (McCarthy Equality Theory) Given a first order language L = ⟨{P_{1}^{b(1)}, …, P_{n}^{b(n)}}, {f_{1}^{a(1)}, …, f_{m}^{a(m)}}, {c_{1}, …, c_{o}}⟩, where the P s are predicates, and the fs 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}. \begin{matrix}⋀_{j=1}^{k} e(x_{j}, y_{j}) → \\ P_{i}(x_{1}, …, x_{k}) ≡ P_{i}(y_{1}, …, y_{k}) \end{matrix}

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

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

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

8.2.4 Lifschitz

Lifschitz (1984) describes a different approach using true equality rather than a new predicate e. His method has been substantially extended by 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 numbers of this approach function much like the countable extra 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.

Bibliography

Allen, J. F., and H. A. Kautz. 1985. A model of naive temporal reasoning. In J. R. Hobbes and R. C. Moore (Eds.), Formal Theories of the Commonsense World, 251–268. Ablex Publishing Corporation.

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

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

Baker, A. B. 1991. Nonmonotonic reasoning in the framework of situation calculus. Artificial Intelligence 49:5–23.

Baral, C., M. Gelfond, and A. Provetti. to appear. Reasoning about actions: Laws, Observations and Hypotheses. Journal of Logic Programming.

Barwise, J. 1978. Handbook of Mathematical Logic. North Holland.

Benthem, J. v. 1987. Semantics Parallels in Natural Language and Computation. In H. Ebbinhaus, J. Fernandez-Prida, M. Garrido, D. Lascar, and M. R. Artalejo (Eds.), Logic Colloquium ’87, Vol. 129 of Studies in Logic, 331–375. North Holland.

Besnard, P., Y. Moinard, and R. E. Mercer. 1989. The Importance of Open and Recursive Circumscription. Artificial Intelligence 39(2).

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

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

Costello, T. 1996b. Non-monotonicity and Change. PhD thesis, Stanford University.

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

Craig, and Vaught. 1958. Finite axiomatizability using additional predicates. Journal of Symbolic Logic 23:289–308.

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

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

Doherty, P., W. Lukaszewicz, and A. Szalas. 1996. General Domain Circumscription and its First-Order Reduction. Technical Report LiTH-IDA-R-01, Linköping University, January.

Eklof, P., and G. Sabbagh. 1971. Model completions and modules. Ann. Math Logic 2:251–295.

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

Etherington, D. W., R. E. Mercer, and R. Reiter. 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, 102–148. American Mathematical Society.

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.

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

Gärdenfors, P. 1988. Knowledge in Flux. Cambridge, UK: Cambridge University Press.

Gärdenfors, P., and D. Makinson. 1988. Revisions of knowledge systems using epistemic entrenchment. In M. Y. Vardi (Ed.), Proceedings of the Second Conference on Theoretical Aspects of Reasoning About Knowledge, 83–95, Monterey, California, March. Morgan Kaufmann.

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

Gelfond, M., and V. Lifschitz. 1992. Representing Actions in Extended Logic Programming. In K. Apt (Ed.), LOGIC PROGRAMMING: Proceedings of the 1992 Joint International Conference and Symposium, 559–573. MIT Press, November.

Gelfond, M., and V. Lifschitz. 1993. Representing Actions and Change by Logic Programs. Journal of Logic Programming 17:301–322.

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.

Ginsberg, M. L. 1987. Readings in Non-monotonic Reasoning. Morgan Kaufmann.

Giunchiglia, E., G. N. Kartha, and V. Lifschitz. 1995. Actions with Indirect Effects. Working notes of AAAI spring symposium series on extending theories of action.

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

Grosof, B. 1991. Generalizing prioritization. In J. Allen, R. Fikes, and E. Sandewall (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Second International Conference, 289–300, Sa Mateo, California, April 22-25. Morgan Kaufmann.

Hanks, S., and D. McDermott. 1986. Default reasoning, nonmonotonic logics and the frame problem. In Proc. National Conference on Artificial Intelligence (AAAI ’86), 328–333, Philadelphia.

Hass, A. R. 1986. The Case for Domain Specific Frame Axioms. In F. M. Brown (Ed.), The Frame Problem in Artificial Inteligence, 343–348. Morgan Kaufmann.

Haugh, B. A. 1987. Simple causal minimizations for temporal persisitence and projection. In Proc. National Conference on Artificial Intelligence (AAAI ’87), 218–233, Seattle, WA.

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

Kartha, G. N. 1993. Soundness and completeness theorems for three formalizations of action. In Proc. Thirteenth International Joint Conference on Artificial Intelligence (IJCAI ’93), 724–729.

Kartha, G. N. 1994. Two counterexamples related to Baker’s approach to the frame problem. Artificial Intelligence 69(1–2):379–391.

Kartha, G. N., and V. Lifschitz. 1994. Actions with indirect effects. In J. Doyle, E. Sandewall, and P. Torasso (Eds.), Principles of Knowledge Representation and Reasoning: Proc. Fourth International Conference (KR ’94). San Francisco, CA: Morgan Kaufmann.

Kartha, G. N., and V. Lifschitz. 1995. A simple formalization of actions using circumscription. In Proc. Thirteenth International Joint Conference on Artificial Intelligence (IJCAI ’95).

Kautz, H. 1986. A logic of persistence. In Proc. National Conference on Artificial Intelligence (AAAI ’86), 401–405.

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

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. 1984. Some Results on Circumscription. In First Workshop on Nonmonotonic Reasoning, 151–164, Stanford University, August.

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

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

Lifschitz, V. 1986b. Pointwise circumscription: a preliminary report. In Proc. National Conference on Artificial Intelligence (AAAI ’86), 406–410, Philadelphia.

Lifschitz, V. 1987. Formal Theories of Action. In F. Brown (Ed.), The Frame Problem in Artificial Intelligence, 121–127. Morgan Kaufmann.

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

Lifschitz, V. 1991. Frames in the Space of Situations. Artificial Intelligence 46(3):365–376.

Lifschitz, V. 1993. A Language for Describing Actions. In Working Papers of Commonsense ’93, 103–113.

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

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

Lin, F. 1991. A Study of Nonmonotonic Reasoning. PhD thesis, Stanford University.

Lin, F., and R. Reiter. 1994. State Constraints Revisited. Journal of Logic and Computation 4(5):655–678.

Lin, F., and Y. Shoham. 1991. Provably correct theories of action (preliminary report). In Proc. National Conference on Artificial Intelligence (AAAI ’91), 349– 354.

Lin, F., and Y. Shoham. 1992. Concurrent actions in the situation calculus. In Proc. National Conference on Artificial Intelligence (AAAI ’92), 590–595.

Lin, F., and Y. Shoham. 1995. Provably Correct Theories of Action. Journal of the ACM 42(2):293–320.

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, and Sandewall (Eds.), Non-Monotonic Reasoning. Lecture Notes in Artificial Intelligence 346, Springer-Verlag, January.

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

McCain, N., and H. Turner. 1995. A causal theory of ramifications and qualifications. In Proc. Thirteenth International Joint Conference on Artificial Intelligence (IJCAI ’95), 1978–1984.

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.

Minker, J., and D. Perlis. 1984. Protected circumscription. Proc Workshop on Non-Monotonic Reasoning 337–343.

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

Owre, S., J. Rushby, and N. Shankar. 1992. PVS: A prototype verification system. In Automated Deduction–CADE-11, Vol. 607 of Lecture Notes in Artificial Intelligence, 748–752.

Pednault, E. 1989. ADL: Exploring the middle ground between STRIPS and the situation calculus. In Proc. First International Conference on Principles of Knowledge Representation and Reasoning (KR ’89), 324–332.

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

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

Perlis, D., and J. Minker. 1986. Completeness Results for Circumscription. Artificial Intelligence 28:29–42.

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

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

Rathmann, P. K., M. Winslett, and M. Manasse. 1990. Equality and circumscription. Technical Report 1615, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, Illinois.

Reiter, R. 1987. Nonmonotonic reasoning. Annual Reviews of Computer Science 147–188.

Reiter, R. 1991. The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. In V. Lifschitz (Ed.), Artificial Intelligence and Mathematical Theory of Computation, 359–380. Academic Press.

Robinson, A. 1963. Introduction to Model Theory. Amsterdam: North-Holland.

Sandewall, E. 1989a. Filter preferential entailment for the logic of actions in almost continuous worlds. In Proc. Eleventh International Joint Conference on Artificial Intelligence (IJCAI ’89), 894–899, Detriot MI.

Sandewall, E. 1989b. The Semantics of Non-Monotonic Entailment defined using partial Interpretations. In Reinfrank, de Kleer, Ginsberg, and Sandewall (Eds.), Non-Monotonic Reasoning, 74–99. Lecture Notes in Artificial Intelligence 346, Springer-Verlag, January.

Sandewall, E. 1994. Features and Fluents. Oxford University Press.

Schubert, L. 1990. Monotonic solution of the frame problem in the situation calculus: An efficient method for worlds with fully specified actions. In H. E. Kyburg, R. P. Loui, and G. N. Carlson (Eds.), Knowledge Representation and Defeasible Reasoning, Vol. Volume 5 of Studies in Cognitive Systems, 23–67. Dordrecht / Boston / London: Kluwer Academic Publishers.

Shoham, Y. 1986a. Chronological Ignorance: Time, Nonmonotonicity, Necessity and Causal Theories. In Proc. National Conference on Artificial Intelligence (AAAI ’86), 389–393.

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

Shoham, Y. 1987a. Nonmonotonic logics: meaning and utility. In Proc. Tenth International Joint Conference on Artificial Intelligence (IJCAI ’87), San Mateo, CA. Morgan Kaufmann.

Shoham, Y. 1987b. A semantical approach to nonmonotonic logics. In Proc. 2nd IEEE Symp. on Logic in Computer Science, 275–279. Reprinted in (Ginsberg 1987).

Shoham, Y. 1987c. Temporal Logics in AI: Semantical and Ontological Considerations. Artificial Intelligence 33(1):89–104.

Shoham, Y. 1988a. Chronological Ignorance: Experiments in Nonmonotonic Temporal Reasoning. Artificial Intelligence 36:271–331.

Shoham, Y. 1988b. Reasoning about Change. Cambridge, USA: MIT Press.

Shoham, Y., and D. McDermott. 1988. Problems in Formal Temporal Reasoning. Artificial Intelligence 36(1):49–62.

Stalnaker, R. 1968. A Theory of Conditionals. Vol. 2 of American Philosophical Quarterly Monograph Series (Nicholas Rescher, ed. Oxford: Blackwell. 98–112.

Stein, L. A., and L. Morgenstern. 1994. Motivated action theory: a formal theory of causal reasoning. Artificial Intelligence 71(1):1–42.

Veltman, F. 1986. Logics for conditionals. PhD thesis, Filosofisch Institut, Universiteit van Amsterdam.

Winslett, M. 1988. Reasoning about action using a possible models approach. In Proc. National Conference on Artificial Intelligence (AAAI ’88), 89–93.

Definition Index

(Z, S) <_{Φ,Ψ} (Z′, S′), 92 T_{𝔄}, 42 𝔐 ≤_{γ_{1},...γ_{n};Z} 𝔑, 62 <, 59 CL_{L}^{{ϕ_{1},... ,ϕ_{o}}}, 65 Circ(α; γ_{1}, γ_{2}), 16 Circ_{C}(α; \frac{γ_{1}}{δ_{1}} , \frac{γ_{2}}{δ_{2}} ), 36 Circ_{L}(A; Ψ; Φ), 93 Circ_{P} (α; P_{1}, P_{2}), 60 Circ_{L\overline{P}}, 17 Circ_{re}, 73 Closed_{L}(ϕ), 57, 93 DomCirc_{L}(α), 57 L_{ω_{1},\overline{P}}^{2} , 24 L_{sit}^{n}, 45 L_{ω_{1},\overline{P}}, 24 f, 45 γ_{1}, … γ_{n}; Z-minimal, 62 γ_{1}, … γ_{n}; Z-sub-model, 62 ⟨W, l, ≺⟩, 27 ≤, 16, 59 ≤^{Γ}, 17 ≤_{Γ;Δ}, 64 ≤_{domain}, 58 𝔄[γ], 17 ⊧_{Baker}, 103 ⊧_{Reiter}, 109 ⊧_{≤}, 42 ⊧_{all}, 131 ⊧_{frame}, 102 ⊧_{proj}, 47 ⊧_{≤_{Φ,Ψ}^{Cofinal}}, 90 |∼, 26 \overline{P} -minimal model, 60 α̃, 16 a, 45 ab_{1}, 100 ab_{2}, 100 g, 45 inf, 66 s, 45 result, 44 CM, 26 Cut, 26 ID, 26 LLE, 26 Or, 26 P, 26 RW, 26

⟨W, l, ≺⟩, 27 ≤^{Γ;\overline{P′}}, 22 ≤_{( \frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn})}, 36 ≤_{D×D′}, 22 𝔐[P] , 46 𝔐 ≤ 𝔑, 46 \overline{P} -sub-model, 60 Circ_{F} (α; γ_{1}, γ_{2}; P_{1}), 61 InfCirc(α; γ_{1}, γ_{2}), 24

Baker Entailment, 103 basis, 15

change formula, 100 circumscription

all, 131 cofinal, 93 conditional

first order, 43 propositional, 36

domain, 57

formula, 67 formula, 61

propositional, 24 predicate, 60 second order, 62

cofinal entailment, 91 cofinal preference, 90 conservative extension, 73 consistency preserving, 84

dense, 81 downwards closed, 82 existentially closed, 87

family, 14 filter, 14 frame entailment, 102 function closure, 57, 93

relative, 65

ideal, 14 Ideal_{1} entailment, 83 Ideal_{2} entailment, 83 inf, 93

Lin entailment, 110

McCarthy Equality Theory, 135 Min preference, 63 Min/Max preference, 64 Minimal, 15 minimal entailment, 42 model completion, 85

partial order, 14 pre-order, 13 preference conditional, 36, 43 preference domain , 58 preferential consequence model, 27 product of pre-orders, 22

Reiter entailment, 109 relativization, 57, 91 restricted monotonicity, 115 restriction, 15

temporal projection, 47

Concept Index

action, 44 auto-epistemic logic, 6

change, 5 Chronological ignorance, 50 circumscription, 7

all, 131, 132 auto, 130 conditional, 31, 34–36, 38, 40–43,

45–47 domain, 11, 28, 31, 33, 54, 56–59,

72, 132 formula, 55, 63, 64, 66, 67, 69, 70,

72 formula, 11, 16, 54 non-recursive, 130, 131 pointwise, 131 predicate, 54 protected, 130 r.e., 73 structural, 130 variable, 130

closed world assumption, 6 cofinal, 96 compositional, 34 conditional logic, 6 conservative extension, 55 convention

communication, 2 storage, 3

counterfactual, 6, 12

default logic, 6 domain

closure, 56 domain closure, 33 domain closure assumption, 131

Elaboration tolerance, 38 elaboration tolerance, 3, 9, 42 equality of closed terms, 133 expressive power, 13

filter, 19 finitely axiomatizable, 72 fluent, 44 frame, 5

groundedness, 6

incomplete information, 2 induction, 7 infinite languages, 11 introspection, 6 L-structure, 58, 70 languages

infinite, 13

mathematical induction, 54 McCarthy Equality Theory, 135 Minimal, 15, 18, 37 model minimization, 128 model theory, 4

negation as failure, 6 Nested Abnormality Theories, 131, 132 non-monotonic consequence, 6

policy, 2 pre-order

discrete, 13, 22 finite, 13, 22

pre-order on valuations, 19 pre-orders on valuations, 11 preference, 4 preferential consequence relations, 11,

13 probability

streamlined, 4 theory, 7

PVS, 48, 119

qualification, 5

recursively enumerable, 73 reduct, 58 reflexive, 8 reflexivity, 17 relativization, 57, 72 restricted monotonicity, 115 restriction, 15 result, 44

situation, 44

situation calculus, 45

smoothness, 8 sub-model, 31, 58

temporal projection, 47

transitive, 8 transitivity, 17 typical, 2

unique names assumption, 134 unless, 6

varied, 16, 22, 60 constant, 34 function, 34

well-founded, 8

Yale Shooting Problem, 32, 47

Symbol Index

T_{𝔄}, 42 ; ⊧_{≤_{2}}, 39 ; ⊧_{≤_{3}}, 39 ; A, 47, 48, 55, 73 ; Axiom(ϕ), 56 ; B, 15 ; C, 55 ; CL_{L}^{\{ϕ_{1},... ,ϕ_{o}\}}, 65 ; Circ_{C}, 36, 47 ; Closed_{L}(ϕ), 56 ; D, 13 ; D′, 15 ; Exp(T), 107 ; F_{1}, 112 ; F_{w}, 112 ; I, 14, 28 ; K, 56 ; L, 56 ; L_{sit}^{1}, 48 ; L_{ω_{1},\overline{P}}^{2} , 24 ; L_{ω_{1},\overline{P}}, 24 ; L_{ω_{1}}, 23 ; L\overline{P}, 17–23, 25, 27, 28, 36, 37, 41 ; M, 43 ; Minimal_{≤}, 15 N, 43

P, 18, 60 P_{n}, 20 Q, 18 R, 27 S, 56 U, 55, 56 UNA, 48 W, 27 X, 27 Γ, 17 Σ, 37 χ, 29 ≅, 23 ↓, 37 f, 45, 52, 56 \frac{γ}{δ}, 36 holds, 46 holds′, 52 β, 17, 26 δ, 16, 29 γ, 16, 26 ψ, 16, 60 ⟨d, d′⟩, 22 ⌈log_{2}n⌉, 28 ≤, 14, 16, 35 ≤^{Γ;\overline{P′}}, 22 ≤_{1}, 34 ≤_{2}, 39 ≤_{3}, 39 ≤_{d}, 23 ≤_{f}, 23 ≤_{( \frac{γ_{1}}{δ_{1}} ,..., \frac{γn}{δn})}, 36 ≤_{↓D′}, 15 ≦, 14 ≲, 13 F, 15 M, 27 𝔄, 17 𝔅, 17 ℭ, 17 𝔐, 46, 58 𝔑, 46, 58 ⊧_{Baker}, 103, 105 ⊧_{Lin}, 111 ⊧_{Reiter}, 109 ⊧_{all}, 132 ⊧_{domain}, 29 ⊧_{frame}, 102, 103, 105, 111, 114–117,

119 ⊧_{mon}, 107 ⊧_{proj}, 48, 51 ⊧_{≤_{Φ,Ψ}^{Cofinal}}, 91, 95 |∼, 26 ω, 20 \overline{P}, 17, 134 \overline{a}, 46 \overline{f}, 46 \overline{x_{1}}, 92 \overline{x_{n}}, 92 \overline{x}, 60 \overline{y_{1}}, 92 \overline{y_{o}}, 92 \overline{y}, 60 \overline{S}, 20 ≺, 27 result, 52 SO, 46, 52 α̃, 36 ×, 22 ⊢, 59 ζ, 56, 63 a, 45, 56 ab, 46 b, 56 b_{i,j}, 15 c, 56 d, 13 d′, 13 e, 136 g, 45, 47 h, 28 i, 14, 22 inf, 66 j, 14 l(x), 27 m, 15 n, 15, 28, 60 s, 45, 52 t, 57 x, 15 y, 15 AR, 103 A, 103 F_{i}, 14 I, 14 M, 20 M′, 20 R, 27 S, 20 P, 26 R, 26 F, 14 M, 82, 89 F, 63, 106, 107, 114, 132 Δ, 56, 63–65, 70–73, 147 Γ, 17–25, 27, 28, 37, 41, 42, 56, 62–65,

70–73, 79, 83, 84, 89, 113, 147, 148, 151, 152

Φ, 70, 90–95, 147, 152 Ψ, 70, 90–95, 147, 152 α, 16–18, 24, 26, 27, 29, 36, 37, 39–

44, 57–64, 67–74, 83, 84, 91, 92, 129–136, 147, 148, 152

β, 17, 18, 26–29, 56, 57, 62, 83, 84, 91,

92, 151 δ, 16, 27, 29, 36–38, 43, 44, 52, 56, 59,

60, 67, 78, 147, 148, 151, 152

γ, 16–22, 24–27, 36, 37, 39–44, 47, 52,

56, 57, 59–64, 67, 70–72, 83, 84, 91, 92, 130–132, 147, 148, 151, 152

ϕ, 6, 29, 36, 37, 43, 44, 56–59, 65–68, 82, 83, 87, 89–94, 105, 107–110, 115, 132, 147, 151 ψ, 17, 18, 24, 29, 37, 56, 60, 61, 63, 65, 67, 68, 90, 92, 105, 108, 151 f, 27, 28, 44, 45, 56, 57, 63, 65, 68, 93,

99, 100, 129, 135, 136, 147, 151 𝔄, 17–19, 22, 24, 28, 35–37, 42, 76, 81,

86, 87, 90, 93, 94, 147, 151, 152 𝔅, 17–19, 22, 24, 28, 35–37, 42, 87, 90,

93, 94, 152 ℭ, 17, 18, 90, 94, 152 𝔐, 43, 46, 58, 60, 62–65, 70, 71, 129, 130, 147, 148, 152 𝔑, 43, 46, 58, 60, 62–65, 70, 129, 130,

147, 148, 152 𝔒, 65, 70

ab , 102, 103, 109 absit , 103–105 alive, 47–49, 116–119

holds, 44, 46–52, 98–101, 103–112, 114– 119, 121, 122, 151

loaded, 47–49, 52, 116–119

result, 44–52, 98–118, 147, 152

shoot, 47–49, 52, 116–119 sit , 103 SO , 46, 48–52, 102, 110, 111, 116–119,

152

wait, 48–52, 116–119

Name Index

McDermott, 6

Amarel, 56, 87 Arima, 136

Baker, 33, 48, 86, 102, 103, 120 Baral, 121 Besnard, 131 Bossu, 95, 128 Boutilier, 9 Burstall, 130

Craig, 73

Davis, 33, 56, 78 deKleer, 15, 34, 62 Doherty, 128 Doyle, 6

Eklof, 88 Etherington, 33, 56, 78, 134

Feferman, 73 Frankel, 55

Gärdenfors, 12 Gödel, 136 Gabbay, 12, 129 Gelfond, 80, 103, 121 Ginsberg, 120 Giunchiglia, 109, 121 Goguen, 130 Grosof, 32

Hanks, 32, 98, 102

Hass, 122

Haugh, 33, 46, 120 Hayes, 45, 80 Henkin, 66 Herbrand, 125, 136 Hintikka, 128

Kartha, 33, 103, 109, 113, 121

Kautz, 120 Keisler, 87 Kleene, 73 Konolige, 15, 34, 62 Kraus, 11, 13, 26, 27, 77, 89, 124, 129

Lehman, 124

Lehmann, 26, 27, 129 Lewis, 9, 12, 77, 95 Lifschitz, 15, 32, 33, 46, 49, 55, 61, 62,

77, 80, 89, 103, 109, 113, 114, 117, 120, 121, 131, 132, 136

Lin, 33, 46, 109, 111, 121 Lorenz, 128 Lukaszewicz, 128

Magidor, 26, 27, 124, 129 Makinson, 12, 77, 129 Manasse, 129, 130 McCain, 122 McCarthy, ii, iv, 7, 9, 11–13, 16, 22,

31–33, 38, 45, 55, 56, 59–61, 72, 75–77, 79, 80, 85, 95, 131, 135

McDermott, 32, 102 Mercer, 33, 56, 131, 134 Minker, 130 Mints, ii, iv Moinard, 131 Moore, 6 Morgenstern, 33 Mott, 130

Patterson, iv Peano, 55 Pednault, 33, 46, 103, 122 Perlis, 130

Rabinov, 80 Ramsey, 12 Rathmann, 129, 130 Reiter, 33, 46, 56, 103, 109, 121, 122,

133, 134 Robinson, 86, 88 Rushby, 48, 119

Sabbagh, 88 Sandewall, 33, 46, 50, 113, 114 Schubert, 103, 122 Shankar, 48, 119 Shoham, 12, 46, 50, 95, 109, 111, 120,

121, 123, 129 Shubert, 33 Siegel, 95, 128 Stalnaker, 12 Stein, 33 Szalas, 128

Turner, 122

van Benthem, ii, iv, 28, 70, 94

Vaught, 73 Veltman, 26

Winslett, 33, 121, 129, 130

Zermelo, 55