Next: Natural Deduction via Context Up: Formalizing Context (Expanded Notes) Previous: Entering and Exiting Contexts

# Lifting Axioms

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

From (3) and (6) we conclude

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.

Next: Natural Deduction via Context Up: Formalizing Context (Expanded Notes) Previous: Entering and Exiting Contexts

Sasa Buvac
Sun Jul 12 14:45:30 PDT 1998