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
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
First use () to get
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.