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 c0 denotes an outer context. Section §9 has more about c0. 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.
