Rules for Lifting

Consider a context
, which expresses a
static theory of the blocks world predicates and .
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
to outer contexts that do involve
situations or times.

To describe , we may write informally

which stands for

We want to apply
in a context in
which and 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. denotes an outer context
in which formulas not otherwise qualified are true. The next section
has more about . Suppose that in context we have

thus associating a context with each situation . We also need

which abbreviates to

and asserts that the facts of all hold in the contexts associated with situations. Mike Genesereth points out that this necessarily involves quantifying into an . Now suppose we have the specific fact

(9) |

(10) |

From () and () we conclude

from which entering gives

() and () give

holding in context . We can now either continue reasoning in or leave and get

and using ()

and finally

In this derivation we used a function giving a context depending on the situation parameter . 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.

2005-04-13