Lifting axioms are axioms which relate the truth in one context to the truth in another context. Lifting is the process of inferring what is true in one context based on what is true in another context by the means of lifting axioms. We treat lifting as an informal notion in the sense that we never introduce a lifting operator. In this section we give an example of lifting. See [13] for more examples.

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

Constant *c*0 denotes an outer context.
Section
§9 has more about *c*0.
In the following formulas, we put the context in which the formula is
true to the left followed by a colon.

We want to use the in a context which
contains the theory of blocks world
expressed using situation calculus.
(We assume that situations are a disjoint sort, and that the variable
*s* ranges over the situation sort.)
In the context predicates
and have a third argument denoting a situation.
Thus the
context needs to relate its
three-argument predicates and to two-argument
predicates and of the context.
This is done by introducing a context of a
particular situation, .
A context is associated with each situation *s*,
such that

In order to get relations between and , we will now import into the context. The importation of is expressed by the axiom

asserting that the facts of all hold in
the contexts associated with every situation.
The following relation between and *above*(*x*,*y*,*s*)
follows from the above axioms.

**Theorem (above):**

The example given is so small that it would be simpler to give the relations among the three-argument predicates directly, but imagine that was much larger than is given here.

We proceed to derive the above theorem.

**Proof !above(above):**
We begin by assuming

asserting that block *x* is on block *y* in a specific
situation *s*. Together with the universally instantiated
form of the direction of formula 4
we get

Now we enter and get

Therefore, by entering we have

By universal instantiation it follows that

Entering gives

By logic, formulas 9 and 13 give

We can now either continue reasoning in or exit and get

Together with the universally instantiated form of the direction of formula 5 we get

By the deduction theorem we can discharge the initial assumption to obtain

Finally, by universal generalization it follows that

In this derivation we used a function giving a context
which depends
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 ideas of [38]. Furthermore, the drafts of this paper have motivated a number of researchers to develop logics of context, in which (some version of) the above argument would be a derivation; these include [25, 45, 9, 5]. However, at present we are more attached to the derivation than to any specific logical system.

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

Sun Jul 12 14:45:30 PDT 1998