USEFUL COUNTERFACTUALS AND APPROXIMATE THEORIES

Tom Costello and John McCarthy ^{∗}

Computer Science Department Stanford University Stanford, CA 94305

email: {costello,jmc}@cs.stanford.edu

Abstract

Counterfactual conditional sentences can be useful in artificial intelligence. In particular, they allow reasoners to learn from experiences that they did not quite have. The truth of a counterfactual and the conclusions that can be drawn from a counterfactual are theory dependent, and different theories are useful in different circumstances. A simple class of useful counterfactuals involves a change of one component of a point in a space provided with a Cartesian product structure. We call these Cartesian counterfactuals. Cartesian counterfactuals can be modeled by assignment and contents functions as in program semantics.

Introduction

(1): “If there had been another car coming over the hill when you passed that car, there would have been a head-on collision.”

is a useful counterfactual conditional sentence. The driver will estimate how long passing took and how much time he would have had if another car had been coming over the hill. If he regards the sentence as true, he will be more cautious about passing in the future. If he regards it as false, it will be because he thinks he had plenty of time to complete the maneuver and get back in the right lane. Notice that if the driver regarded the sentence merely as a material implication with false antecedent, believing it would not be a reason to change his driving habits.

In general, a counterfactual conditional sentence (counterfactual for short) is a sentence

p implies q,

in which the antecedent p is false. If implies is taken to be the ordinary mathematical logical implication ⊃, then all counterfactuals are true. However, in ordinary life, it is often useful to consider certain counterfactuals, as in the above example (1), being possibly false and therefore conveying information when they are true. (1) may be a useful counterfactual, because it permits the driver to learn from an experience he didn’t quite have. We claim that counterfactuals are useful in AI and we shall want robots to use them in their internal reasoning, as well as when communicating.

We will use ≻ to represent counterfactual implication, so that (1) may be written

Another car was coming when you passed ≻ there was a head-on collision.

While counterfactuals are used in daily life, they have been most studied in philosophy. The main philosophical goal has been to assign semantics to these sentences. The Lewis/Stalnaker (Sta68; ST70) approach is the leading one. David Lewis ((Lew73)) defines the truth of a counterfactual using the notion of possible worlds. He posits that possible worlds are ordered by comparative possibility. He then regards p ≻ q as true provided q is true in the nearest possible worlds where p is true. He gives no way of judging the closeness of worlds save that of considering the counterfactuals. Thus it seems difficult to evaluate the truth of any particular counterfactual based on other evidence. Lewis is not worried by this problem, because he is interested in a philosophical basis for counterfactuals, and not in actually calculating the truth of any particular counterfactual.

The most straightforward and possibly the most useful counterfactuals are what we call Cartesian counterfactuals. A situation is described by the values of a number of parameters, and the premise of the counterfactual is that one of the parameters has a different value than in the actual situation, and the other parameters have the same values. In (1), the parameter describing whether another car was coming over the hill is changed, and the driver’s behavior is implicitly unchanged. The passenger computes that a collision would result.

The truth of the counterfactual depends on the particular representation of situations as points in a Cartesian product space. Such representations arise in theories of the world. The useful theories for representing counterfactuals (and for many other purposes) are not complete theories of the world, i.e. the states of the spaces do not correspond to complete states of nature. We call them approximate theories.

∗This research has been partly supported by ARPA contract no. USC 621915, the ARPA/Rome Laboratory planning initiative under grant (ONR) N00014-94-1-0775 and ARPA/AFOSR under (AFOSR) F49620-97-1-0207.

If there are two systems that propagate changes in two different ways, they may give different truth values to some p ≻ q. This corresponds to the idea that we can choose different co-ordinate systems for the same space. In this case the counterfactual has no definite meaning apart from the co-ordinate frame. Indeed in some theories the counterfactual may not have a meaning at all. We see the world through the lenses of theories/frames and so must our robots.

Cartesian counterfactuals are not the only useful counterfactuals. Another straightforward case involves a metric on states, choosing the closest states as the most likely. This brings us closer to Lewis’s notion of counterfactual. What distinguishes our treatment of counterfactuals is how we describe this metric. Rather than describe it in terms of instances of counterfactuals, we describe the metric directly, e.g. a co-ordinate frame.

Useful Counterfactuals

For AI purposes we ask what kinds of counterfactuals are useful to humans, as they are also likely to be the kinds useful to computer programs. Concentrating on useful counterfactuals may also have some philosophical benefits. Here are some examples.

1. The head-on collision example of the introduction.

2. Two ski instructors see a pupil fall on a course. One says “If he had bent his knees more, he would not have fallen”. The other disagrees and claims “If he had put his weight on his downhill ski, he would not have fallen”. This example is from (McC79a).

3. Our ski instructors could view the world in a different way, and both assent to the counterfactual, “if he had two more lessons he would not have fallen”.

4. If Caesar had been in charge in Korea, he would have used nuclear weapons. If Caesar had been in charge in Korea, he would have used catapults. Different theoretical structures give different counterfactuals.

5. If I had brandished a gun, the muggers would have run away. Each of these counterfactuals tell us something about

how the world works. We can use this advice in future, if we find ourselves in a similar situation. This points to counterfactuals being useful for learning. They allow us to learn from situations that did not happen, like the car crash we discussed earlier. The notion that the counterfactual is applicable in similar situations is important. If we are to use a counterfactual to predict in a new situation s, there must be a precise test, whether or not the new situation s is sufficiently similar to the current situation. This test is given by our approximate theory. If the new situation s is a model of the approximate theory, then the counterfactual is applicable.

Learning

A chess program, playing over a game, can reason counterfactually — “If Spassky had played this move, he would have beaten Fischer.” The program can learn from this. It is important, if we are to use counterfactuals for learning that we can recognize that they are sometimes false. In the above example we can imagine the response that “If there was another car it would have been visible in time for me to avoid it”. This new counterfactual can be true or false.

The performance of learning algorithms improves when they have more examples. Counterfactuals are one way to collect more examples than can be found by direct experience. Sometimes it is much wiser to hear about a data point than to experience it.

Prediction in similar circumstances

In so far as our knowledge of the world is incomplete, new sentences can tell us more about the world. Every counterfactual we are told gives us more information about how the world would be, if things were only slightly different, relative to some unstated approximate theory. This information can later be used if we find ourselves in a situation with only a small number of differences between it and the present, so that the approximate theory is applicable to both. The counterfactual

“If there was one more book in that box you would not have been able to lift it.”

tell us that in future situations, that satisfy the unstated theory the speaker considers, boxes with more books in them will be too heavy to lift. This differs from the learning we considered earlier, as this is inferring a universal from a counterfactual, rather than using the counterfactual as an instance in a learning algorithm.

If the approximate theory is unstated, to use this counterfactual we need to infer what theory was used. A natural default to use here is to assume that the speaker is using the same theory that you find appropriate to describe the situation.

The reason that we can apply counterfactuals in other situations is because the theories on which they are based are approximate. The truth of the counterfactual only depends on certain features of the situation, and when these features re-occur the same inference may be made. In a later section we give an example of where we can derive new facts, that do not mention counterfactuals, from a counterfactual. In our skiing domain, we show that we can derive a fact about the world (that a certain slope is a turn), from the truth of a counterfactual, (“if he had put his weight on his downhill ski, he would not have fallen”).

Counterfactuals are useful for other purposes in AI. Ginsberg (Gin86) suggests that they are useful for planning. They also are closely related to the notion of causality.

Examples

Cartesian counterfactuals involve a counterfactual sentence, a theory, a frame, and a world/point in the frame. The sentence is interpreted by the theory, relative to the frame. We move through the frame, from the current world, to a new point in the frame.

Numerical Example

Example: 1 We consider a Cartesian space of four components, x, y, z, w. The theory provides a coordinate system for the space. We are interested in the distance from a point to the origin:

s = \sqrt{x^{2} + y^{2} + z^{2} + w^{2}}

This sentence is our approximate theory.

Now consider the point (1, 2, 1, 2). This will act as our current world. We ask whether,

y = 3 ≻ s = 7.  (2)

Our Cartesian structure implies that x, z and w hold their particular values 1, 1, 2. Therefore we have

s = \sqrt{1 + 9 + 1 + 4}, s = \sqrt{15}, s ≠ 7.

Therefore 2 is an example of an untrue counterfactual. The counterfactual “if y were 3 then s would be \sqrt{15}” is true, i.e. y = 3 ≻ s = \sqrt{15}

This example has all the essential elements of Cartesian counterfactuals. We have a Cartesian space, whose points are the models of the approximate theory and whose structure is given by the co-ordinates. Each of these co-ordinates in this example is the value of a variable. To find the truth value of a counterfactual we change the co-ordinate as specified by the left hand side and evaluate the right hand side.

The co-ordinate frame we chose here, that each of the variables, x, y, z, w were independent^{1}, is not the only possible frame. We could have chosen any linear transformation of those variables. One possibility is,

x′ = x + y, y, z, w

Our initial state has the following values.

x′ = 3, y = 2, z = 1, w = 2

Given this co-ordinate system, the counterfactual y = 3 ≻ s = \sqrt{14} is true, while this was false in the previous frame.

Thus we can have different co-ordinate systems, and these different systems give rise to different sets of true counterfactuals. Thus we have identified three factors which influence the truth of a counterfactual:

1. The space of possible states.

2. The co-ordinate frame on the space of possible states.

3. The current state.

Formalization of Skiing Examples

We now look at an axiomatization that formalizes some examples of counterfactuals in a skiing domain. We sketch a formalization of skiing, which includes both some facts about lessons, and some facts about what happens when you ski. The formalization uses the situation calculus introduced in (MH69).

The analysis is designed to highlight several points.

1. Co-ordinate frames give a simple way of defining semantics for counterfactuals.

2. Different frames are appropriate for different points of view.

3. Different frames can lead to different counterfactuals.

We wish to consider four counterfactuals. The first two are from our previously mentioned two ski instructors. Before we consider the counterfactuals, we consider the following story.

Junior had 25 dollars. He went to a ski slope and spent his money on two cheap lessons, that cost 25 dollars. Cheap lessons teach you one skill each lesson, first bending your knees on bumps, then placing your weight on your downhill ski on turns. Expensive lessons cost twice as much, but teach two skills per lesson, in the same order. Thus, Junior learns to bend his knees. He then goes skiing, at a time picked out by situation 1, but when he comes to Slope4 he falls.

Slope4 is a turn, and according to our theory, unless you place your weight on your downhill ski on turns you fall. We also believe that unless you bend your knees on a bump you fall, and that these behaviors happen only if you have learned these skills.

Our first counterfactual states that ‘‘if he had actually bent his knees in situation 1 then he would not have fallen in the next situation”. This will be represented by the following counterfactual.

Actual(result(Bend, S1)) ≻ ¬holds(Fallen, Next(S1)) (3)

The other states that ‘‘if he had actually put his weight on the downhill ski in situation 1 then he would not have fallen in the next situation”. In our logical formalization this will be written.

Actual(result(Down, S1)) ≻ ¬holds(Fallen, Next(S1)) (4)

The difference can be resolved by finding out whether Slope4 has a bump or is a turn. As Slope4 is a turn, the first is false and the second is true. Here, the counterfactuals are evaluated in a co-ordinate frame where what Actually happens is independent. Thus, we can change the fact that he bent his knees, without changing any other co-ordinate, and thus infer that he does not fall.

1We use independent to mean that they are not interdefinable, rather than the use of independent in probability theory.

Both our instructors can agree that ‘‘if he had chosen more expensive lessons, then he would not have fallen”.

Choice = Expensive ≻ ¬holds(Fallen, Next(S1)) (5)

Here they choose to keep the number of lessons fixed, but make the lessons better.

Our hero does not assent to the above conditional. He knows that “if he chose the expensive lessons, he would not have had any lessons”, as he cannot afford it. Thus he believes that he would fall if he chose expensive lessons,

Choice = Expensive ≻ holds(Fallen, Next(S1)). (6)

Thus he still would not have learned the requisite skills. Expensive lessons cost more, so he would not have been able to take as many lessons.

The reason that the ski instructors differ from our hero on this conditional is that they allow the amount of money to vary, while our hero allows the actual situations to vary. They use different co-ordinate frames and thus get different results.

We give an axiomatization of part of this domain in the Appendix, and now present a set of co-ordinate frames that gives the results for the first two counterfactuals.

Co-ordinate frames for Skiing

With the axiomatization of the above story given in the Appendix we can now consider the first two counterfactuals. In each case we take an approximate theory, which will be some subset of the consequences of the axioms in the Appendix, and a co-ordinate frame. From the theory and the frame we judge the truth of the counterfactual. We show that choosing different approximate theories, or choosing different frames can lead to different choices.

We give the co-ordinate frame that the two instructors use. They choose what situations were actual, and what fluents held at the situation S1, and the type of Slope4 as their frame. Here tr is a truth value. The propositional functions in the frame are all instances of the following, where f, s and t range over fluents, situations, and types of slopes.

λs.Next(S1) = s, λtr.holds(f, S1) = tr,

λt.Typeslope4 = t

As their core approximate theory they take the axioms about the effects of various ski moves, 10, the axiom relating Next and Actual, 11, and the unique names and domain closure axioms and the frame axioms 13. As the current world, they choose the values,

Next(S1) = result(Falls, S1) Typeslope4 = Turn
¬holds(Fallen, S1)  holds(Skiingslope4, S1)

as they agree that Junior did fall on a slope with a bump, while skiing Slope4.

With this frame the following counterfactuals are false and true, respectively. Actual(result(Bend, S1)) ≻ ¬holds(Fallen, Next(S1)) Actual(result(Down, S1)) ≻ ¬holds(Fallen, Next(S1))

(7)

In contrast the counterfactual

Actual(result(Bend, S1)) ∧ Typeslope4 = Bump ≻

¬holds(Fallen, Next(S1)) (8)

is true. We prove these claims formally after introducing the necessary machinery in the next section.

State Vector Approach

In the previous section we claimed that certain counterfactuals were true, given some co-ordinate frames. We now give an axiomatization that allows us to formally prove these statements.

We can define Cartesian counterfactuals in terms of a state vector approach. This uses the assignment function a of (McC63). It also uses the c or contents function. The value of a variable x in a state vector ξ is c(x, ξ), while the state vector that is like ξ, save that x has been assigned the value v, is a(x, v, ξ). We can axiomatize a and c as follows.

\begin{matrix}∀x, v.ξ.c(x, a(x, v, ξ)) = v, \\ ∀x, y, v, ξ.x ≠ y → c(y, a(x, v, ξ)) = c(y, ξ) \end{matrix}

State vectors are usually thought to be sets of variables. Here, our state vectors will be sets of propositional functions and their values, that is, functions that return propositions. Our state vector does not have values for all propositional functions, just those in our co-ordinate frame. Thus, for our numerical example, the set of co-ordinate propositional functions is,

λn.x = n, λn.y = n, λn.z = n, λn.w = n

These give rise to a Cartesian product structure over the models of the approximate theory

s = \sqrt{x^{2} + y^{2} + z^{2} + w^{2}}.

We can assign a propositional function to a value using the a assignment function. We can determine the value of a propositional function in a state vector using c, the contents function.

We call the set of co-ordinate propositional functions our frame, and we assume that they are picked out using the predicate frame. We then have the rules,

∀x, v, ξ.frame(x) → c(x, a(x, v, ξ)) = v

∀x, y, v, ξ.frame(x) ∧ frame(y) ∧ x ≠ y →
c(y, a(x, v, ξ)) = c(y, ξ)

Rather than assume that there is only a single frame, we can make the frame an argument of c and a. This gives the axioms,

∀x, v, ξ, f.f(x) → c(x, a(x, v, ξ, f), f) = v

∀x, y, v, ξ, f.f(x) ∧ f(y) ∧ x ≠ y →
c(y, a(x, v, ξ, f), f) = c(y, ξ, f)

Our co-ordinate frame thus uniquely determines the values of the co-ordinate propositional functions. From these values, we can determine a theory, the set of sentences implied by the statements that the co-ordinate propositional functions have the values in the state vector.

Another way of considering this, is to use contexts, as proposed by (McC93). We can make our state vector ξ into a context by using a function makecontext (ξ, f, A). The definition of makecontext is, in terms of the frame and the approximate theory A,

ist(ϕ, makecontext(ξ, f, A)) if and only if
{x(n)|x ∈ f ∧ c(x, ξ, f) = n}, A ⊧ ϕ.

That is, ϕ is true in a state vector ξ, if it follows from the fact that the co-ordinate propositional functions have the values the state vector assigns them, relative to the approximate theory A. We use metatheoretic notation ⊧ here. We can move to a purely formal system by replacing A ⊧ ϕ by a sentence of second order logic, in the usual way. When we derive facts from counterfactuals, we will use a second order logic formalization.

Definition: 1 A counterfactual sentence ϕ ≻ ψ is true in a space, axiomatized by A, with a co-ordinate frame induced by a set of propositional functions S, at the point p, which is given by applying the functions S to the values T, if and only if,

ist(ψ, makecontext(a(g, n, ξ_{0}, f), f, A)),

where ξ_{o} is the state vector which assigns the propositional functions S the values T, and f is the predicate on propositional functions true of exactly S, and ϕ ≡ g(n), relative to A for some function g ∈ S and some argument of that function n.

We now consider our first example. We define our frame as follows.

∀var.f_{0}(var) ≡
var = (λn.x = n)∨
var = (λn.y = n)∨
var = (λn.z = n)∨
var = (λn.w = n)

We now define our initial state vector ξ_{0}.

c(λn.x = n, ξ_{0}, f_{0}) = 1,
c(λn.y = n, ξ_{0}, f_{0}) = 2,
c(λn.z = n, ξ_{0}, f_{0}) = 1,
c(λn.w = n, ξ_{0}, f_{0}) = 2

We need unique names axioms for formulas, which we define extensionally. There are some reasons why we would not do this, a discussion of this point can be found in (McC79b).

We then have that c(λn.x = n, a(λn.y = n , 3, ξ_{0}, f_{0}), f_{0}) = 1. We can derive this from the second property of a and c, and the fact that λn.x = n ≠ λn.y = n.

Further, we have the

\begin{matrix}ist(s = \sqrt{15}, \\ makecontext ( \begin{matrix}a(λn.y = n, 3, ξ_{0}, f_{0}), f_{0}, \\ s = \sqrt{x^{2} + y^{2} + z^{2} + w^{2}} \end{matrix} )) \end{matrix}

This follows as, x = 1, y = 3, z = 1, w = 2, s = \sqrt{x^{2} + y^{2} + z^{2} + w^{2}} ⊧ s = \sqrt{15}.

We have this set of sentences as our theory, as these are the formulas that result from applying the function λn.x = n etc. to their values, 1, etc. in the state vector. We may find it useful to write makecontext (a(λx.ϕ, n, ξ, f), f, A) as whatif_{A,ξ,f}(ϕ(n)), making the state vector implicit.

We now prove that the first two counterfactuals that we considered in our skiing story are true and false respectively.

Theorem: 1 The counterfactual Actual(result(Bend, S1)) ≻ ¬holds(Fallen, Next(S1)), is true, in the theory A axiomatized by the axioms about the effects of various ski moves, 10, the axiom relating Next and Actual 11, and the unique names axioms and the frame axioms 13, with the following frame,

λs.Next(S1) = s, λtr.holds(f, S1) = tr, λt.Typeslope4 = t

and the following current world,

Next(S1) = result(Falls, S1) Typeslope4 = Turn
¬holds(Fallen, S1)  holds(Skiingslope4, S1)

Proof: We use the first property of our assignment functions to derive that, in our new context c = makecontext(Actual(result(Bend, S1)), frame, A),

ist(Actual(result(Bend, S1)), c).

To prove this we need to show that Actual(result(Bend, S1)) is equivalent to the result of applying a function in the frame to a value. Also note that Next(S1) = result(Bend, S1), thus Actual(result(Bend, S1)) is equivalent to applying λs.Next(S1) = s to result(Bend, S1).

We use the second property of our assignment function a to derive that holds(Skiingslope4, S1). This follows as λtr.holds(Skiingslope4, S1) = tr is in the frame, and holds(Skiingslope4, S1) is true in our current world, so we have that its value persists. We also show that Typeslope4 = Turn in the same way.

We now use the effect axiom to derive that holds(Fallen, result(Bend, S1)). Finally the definition of Next, which is in the core theory gives us holds(Fallen, Next(S1)).

Theorem: 2 The counterfactual Actual(result(Down, S1)) ≻ ¬holds(Fallen, Next(S1)) is true, in the theory A axiomatized above, with the frame and current world specified above.

Proof: We use the first property of our assignment functions to derive that in our new context,

ist(Actual(result(Down, S1)), makecontext(Actual(result(Down, S1)), f, A)).

To prove this we need to show that Actual(result(Down, S1)) is equivalent to a function in the frame applied to some argument, which follows from the previous analysis.

We use the second property of our assignment functions to derive that holds(Skiingslope4, S1). This follows as holds(Skiingslope4, S1) is in the frame, and holds(Skiingslope4, S1) is true in our current world, so we have that its value persists. We can further show that Typeslope4 = Turn is true, as it is true in the core theory.

We now use the frame axiom 13 to derive that ¬holds(Fallen, result(Down, S1)), using the given fact that holds(Skiingslope4, S1) and Typeslope4 = Turn. Finally the definition of Next gives us ¬holds(Fallen, Next(S1)).

Deriving facts from Counterfactuals

In this section we show that we can derive facts that do not contain counterfactual implications, from counterfactuals.

We take as our theory, the axioms in the Appendix, save for the last axiom Typeslope4 = Turn. From the counterfactual, Actual(result(Down, S1)) ≻ ¬holds(Fallen, Next(S1)) we derive that, Typeslope4 = Turn. Theorem: 3 Let the theory A be axiomatized by the axioms in the Appendix save 12 and the counterfactual

Actual(result(Down, S1)) ≻ ¬holds(Fallen, Next(S1)),

judged relative to the approximate theory B axiomatized by the axioms about the effects of various ski moves, 10, the axiom relating Next and Actual 11, and the unique names axioms and the frame axioms 13. Let f(var) be defined as follows:

∀var.f(var) ≡ ∃s.var = λs.Next(S1) = s∨ ∃f.var = λtr.holds(f, S1) = tr

Then, A ⊧ Typeslope4 = Turn. We expand the definition of a counterfactual being true to get

ist(¬holds(Fallen, Next(S1)),

makecontext(a(λs.next(S1) = s,

result(Down, S1), f), f, A))

We instantiate into the definition ist(ϕ, makecontext(ξ, f, B)) if and only if

{x(n)|x ∈ f ∧ c(x, ζ, f) = n}, B ⊧ ϕ.

to get,

B, Next(S1) = result(Down, S1), ¬holds(Fallen, S1), holds(Skiingslope4, S1) ⊧

¬holds(Fallen, Next(S1))

This is a meta-theoretic statement, so we translate this into second order logic, by quantifying over predicates, functions and objects in the standard way.

∀Z̄.B[Z̄/Z̄′] ∧ Next′(S1′) = result′(Down′, S1′)∧

¬holds′(Fallen′, S1′)∧ holds′(Skiingslope4′, S1′) → ¬holds′(Fallen′, Next′(S1′)),

where Z̄ is the tuple of all constant symbols in the language, and Z̄′ is a tuple of variables, equal in type and arity to the constants in Z̄, we write variables in Z′ as Next′ etc.

This second order sentence captures the truth of the counterfactual. We can conjoin this with the other axioms in the theory A, and ask whether it implies, Typeslope4 = Turn in second order logic.

It does, as can be seen from instantiating the universally quantified variables, with their corresponding constants, except for Actual′ and Next′ which are instantiated by the predicate P true of the smallest set of situations satisfying the formulas below, and the partial function, Next′′(s) = result(a, s) ≡ P (result(a, s)), defined from P,

P (S0) ∧ P (result(Skislope4, S0))∧ P (result(Down, result(Skislope4, S0))) ∧∀s.s ≠ S0 ∧ s ≠ result(Skislope4, S0)∧

s ≠ (result(Down, result(Skislope4, S0)) ∧ P (s) → P (result(Wait, s))

The result of instantiating these terms, and noting that the left hand side is derivable from the theory A gives the sentence.

¬holds(Fallen, result(Down, S1))

However, we also have holds(Skiingslope4, s1), and the axiom,

∀s.Typeslope4 = Bump ∧ holds(Skiingslope4, s) → holds(Fallen, result(Down, s))

Instantiating this with S1 and simplifying gives Typeslope4 ≠ Bump. As we know by domain closure that Typeslope4 = Bump ∨ Typeslope4 = Turn, we have

Typeslope4 = Turn,

as required.

Conclusion

We have introduced a new approach to counterfactuals. Rather than ask what counterfactuals follow from other counterfactual assertions, we consider how counterfactuals arise from approximate theories, and co-ordinate frames.

We do not claim there is a single set of true counterfactuals. Rather, a counterfactual can only be judged relative to a background theory, and a choice of a “coordinate frame”.

The counterfactuals we consider are those that are useful to reasoners in the following sense. They allow the reasoner to gain information about how the world behaves, so that in future situations the reasoner can better predict what will happen.

A major novelty is the reification of the metric on worlds, or as we view it, the co-ordinate frame. Rather than suppose that there is one privileged co-ordinate frame we explicitly judge counterfactuals relative to a specific frame. The frame gives us information about the applicability of the counterfactual, and different frames are appropriate for different purposes.

References

M. L. Ginsberg. Counterfactuals. Artificial Intelligence, 30, 1986. D. K. Lewis. Counterfactuals. Harvard University Press, Cambridge, MA., 1973. J. McCarthy. Situations, Actions and Causal Laws. Technical Report Memo 2, Stanford University Artificial Intelligence Project, Stanford, CA, 1963. J. McCarthy. Ascribing mental qualities to machines. Technical Report STAN-CS-79-725, Stanford University, 1979. John McCarthy. First order theories of individual concepts and propositions. In Donald Michie, editor, Machine Intelligence, volume 9. Edinburgh University Press, Edinburgh, 1979. Reprinted in (McC90). John McCarthy. Formalization of common sense, papers by John McCarthy edited by V. Lifschitz. Ablex, 1990. John McCarthy. Notes on formalizing context. In Proc. Thirteenth International Joint Conference on Artificial Intelligence (IJCAI ’93), 1993. J. McCarthy and P. Hayes. Some Philosophical Problems From the Standpoint of Artificial Intelligence. In D. Michie, editor, Machine Intelligence 4, pages 463–502. Edinburgh University Press, Edinburgh, UK, 1969. J. Pinto and R. Reiter. Adding a time line to the situation calculus. In Second Symposium on Logical Formalizations of Commonsense Reasoning, pages 172– 177, 1993. R. Stalnaker and R. H. Thomason. A semantic analysis of conditional logic. Theoria, 36:23–42, 1970. R. Stalnaker. A Theory of Conditionals, volume 2 of American Philosophical Quarterly Monograph Series (Nicholas Rescher, ed., pages 98–112. Blackwell, Oxford, 1968.

Appendix

This Appendix presents a formalization of a skiing domain in the situation calculus. The major novelty of this domain is that it allows some reasoning about the actions of an agent. Normally, in the situation calculus all sequences of actions are considered. Here we look at what sequences would happen given some facts about our agents beliefs and some rules about how he acts. We include the notion of an actual time line picked out of the possible time lines in the situation calculus. This follows Reiter and Pinto (PR93). We enrich this with a Next partial function, that picks out the next actual situation.

We have five sorts, the usual situation, fluent and action sorts, plus sorts for terrain types and skills.

We have four actions Skislope4, Falls and Bend, Down, and Wait. We have fluents, Fallen, Skiingslope4, Learned(sk) for every skill sk. Our two skills are Bendknees and Downhillski.

We have the initially our hero has no knowledge of skiing.

¬holds(Learned(Bendknees), S0) ¬holds(Learned(Downhillski), S0) ¬holds(Fallen, S0) ¬holds(Skiingslope4, S0)

(9)

We now have some facts about what the actual time line is, given the state of the world, and the knowledge of our hero. If our hero sees a bump, and has learned to bend his knees, he will actually do so, otherwise he will actually fall. If he sees a turn, then he will put his weight on his downhill ski if he has learned to do that, otherwise he will actually fall. We also add that if he does the wrong thing, then he will fall, and add the results of falling etc.

∀s.Actual(result(Skislope4, s)) ∧ Typeslope4 = Bump ∧holds(Learned(Bendknees), s) →

Actual(result(Bend, result(Skislope4, s)))

∀s.Typeslope4 = Bump

∧¬holds(Learned(Bendknees), s) → Actual(result(Falls, result(Skislope4, s)))

∀s.Actual(result(Skislope4, s)) ∧ Typeslope4 = Turn ∧holds(Learned(Downhillski), s) →

Actual(result(Down, result(Skislope4, s)))

∀s.Typeslope4 = Turn∧

¬holds(Learned(Downhillski), s) → Actual(result(Falls, result(Skislope4, s)))

∀s.Typeslope4 = Turn ∧ holds(Skiingslope4, s) → holds(Fallen, result(Bend, s))

∀s.Typeslope4 = Bump ∧ holds(Skiingslope4, s) → holds(Fallen, result(Down, s)) ∀s.holds(Fallen, result(Falls, s)) Actual(S0) Actual(result(Skislope4, S0)) ∀as.s ≠ S0 ∧ s ≠ result(Skislope4, S0) → Actual(s) ≡ Actual(result(Wait, s))

(10)

We now state that after every actual situation there is a unique actual situation, that picked out by Next.

We take this to be the definition of a partial function Next, so that sentences containing Next are notations for sentences containing Actual.

∀s.result(a, s) = Next(s) ≡^{def} Actual(result(a, s)) (11)

We also add that Slope4 has a bump.

Typeslope4 = Bump  (12)

We also need to add unique names, domain closure, and frame axioms.

We have as our unique names axioms, fully unique names, except for the function Actual, the situation constant S1 and the constant Typeslope4.

We now add our frame axioms for each fluent.

∀a, s.holds(Skiingslope4, result(a, s)) ≡ a = Skislope4

∀s, a.a ≠ Falls ∧ (a = Bend → Typeslope4 ≠ Turn

∨¬holds(Skiingslope4, s))∧ (a = Down → Typeslope4 ≠ Bump∨

¬holds(Skiingslope4, s))

→ (holds(Fallen, s) ≡ holds(Fallen, result(a, s)))

∀s, f.f ≠ Skiingslope4 → holds(f, s) ≡ holds(f, result(Wait, s))

∀a, s, sk.holds(Learned(sk), s) ≡ holds(Learned(sk), result(a, s))

(13)

These are enough frame axioms to generate explanation closure axioms for every fluent.

Finally we add induction over situations, using the following schema.

ϕ(s0) ∧ (∀s, a.ϕ(s) → ϕ(result(a, s))) → ∀s.ϕ(s) (14)