Rules for Lifting

Consider a context $above\hbox{-}theory$, which expresses a static theory of the blocks world predicates $on$ and $above$. In reasoning about the predicates themselves it is convenient not to make them depend on situations or on a time parameter. However, we need to lift the results of $above\hbox{-}theory$ to outer contexts that do involve situations or times.

To describe $above\hbox{-}theory$, we may write informally

$above\hbox{-}theory:$

$$(\forall x y)(on(x,y)\supset above(x,y))$$ (2)

$$(\forall x y z)(above(x,y)\land above(y,z)\supset above(x,z))$$ (3)

$$\rm {etc.}$$

which stands for

$$c0:\quad\quad ist(above\hbox{-}theory,(\forall x y)(on(x,y)\supset above(x,y)))$$ (4)

$$\rm {etc.}$$

We want to apply $above\hbox{-}theory$ in a context $c$ in which $on$ and $above$ have a third argument denoting a situation. In the following formulas, we put the context in which the formula is true to the left followed by a colon. $c0$ denotes an outer context in which formulas not otherwise qualified are true. The next section has more about $c0$. Suppose that in context $c$ we have

$$c:\quad\quad\quad\quad (\forall x y s)(on(x,y,s) \equiv ist(c1(s),on(x,y))),$$ (5)

and

$$c:\quad\quad\quad\quad (\forall x y s)(above(x,y,s) \equiv ist(c1(s),above(x,y))),$$ (6)

$$\rm {etc.},$$

thus associating a context $c1(s)$ with each situation $s$. We also need

$$c0:\quad\quad\quad\quad ist(c,(\forall p\ s)(ist(above\hbox{-}theory,p)$$

$$\supset ist(c1(s),p))),$$ (7)

which abbreviates to

$$c:\quad\quad\quad\quad (\forall p\ s)(ist(above\hbox{-}theory,p)\supset ist(c1(s),p)),$$ (8)

and asserts that the facts of $above\hbox{-}theory$ all hold in the contexts associated with situations. Mike Genesereth points out that this necessarily involves quantifying into an $ist$. Now suppose we have the specific fact

$$c0:\quad\quad\quad\quad ist(c,on(A,B,S0))$$ (9)

asserting that block $A$ is on block $B$ in a specific situation $S0$, and we want to derive $ist(c,above(A,B,S0))$. We proceed as follows.

First use () to get

$$c:\quad\quad\quad\quad ist(c1(S0),on(A,B)).$$ (10)

Now we enter $c1(S0)$ and get

$$c1(S0):\quad\quad\quad\quad on(A,B).$$ (11)

From () and () we conclude

$$c:\quad\quad\quad\quad ist(c1(S0),(\forall x y)(on(x,y)\supset above(x,y))),$$ (12)

from which entering $c1(S0)$ gives

$$c1(S0):\quad\quad\quad\quad (\forall x y)(on(x,y)\supset above(x,y)).$$ (13)

() and () give

$$c1(S0):\quad\quad\quad\quad above(A,B),$$ (14)

holding in context $c1(S0)$. We can now either continue reasoning in $c1(S0)$ or leave $c1(S0)$ and get

$$c: \quad\quad\quad\quad ist(c1(S0),above(A,B))$$ (15)

and using ()

$$c:\quad\quad\quad\quad above(A,B,S0)$$ (16)

and finally

$$c0:\quad\quad\quad\quad ist(c,above(A,B,S0)).$$ (17)

In this derivation we used a function giving a context $c1(s)$ depending on the situation parameter $s$. Contexts depending on parameters will surely present problems requiring more study.

Besides that, the careful reader of the derivation will wonder what system of logic permits the manipulations involved, especially the substitution of sentences for variables followed by the immediate use of the results of the substitution. There are various systems that can be used, e.g. quasi-quotation as used in the Lisp or KIF, use of back-quotes, or the notation of [Buvac and Mason, 1993] or the ideas of [McCarthy, 1979b], but all have disadvantages. At present we are more attached to the derivation than to any specific logical system and consider preferable a system in which the above derivation is preserved with as little change as possible.

As a further example, consider rules for lifting statements like those of section to one in which we can express statements about Justice Holmes's opinion of the Sherlock Holmes stories.