next up previous
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 tex2html_wrap_inline3980 , which expresses a static theory of the blocks world predicates tex2html_wrap_inline3982 and tex2html_wrap_inline3984 . 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 tex2html_wrap_inline3980 to outer contexts that do involve situations or times.

To describe tex2html_wrap_inline3980 , 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 tex2html_wrap_inline3980 in a context tex2html_wrap_inline4000 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 tex2html_wrap_inline4000 predicates tex2html_wrap_inline3982 and tex2html_wrap_inline3984 have a third argument denoting a situation. Thus the context tex2html_wrap_inline4000 needs to relate its three-argument predicates tex2html_wrap_inline4012 and tex2html_wrap_inline4014 to two-argument predicates tex2html_wrap_inline4016 and tex2html_wrap_inline4018 of the tex2html_wrap_inline3980 context. This is done by introducing a context of a particular situation, tex2html_wrap_inline4022 . A context tex2html_wrap_inline4022 is associated with each situation s, such that




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


asserting that the facts of tex2html_wrap_inline3980 all hold in the contexts associated with every situation. The following relation between tex2html_wrap_inline4012 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 tex2html_wrap_inline3980 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 tex2html_wrap_inline4054 direction of formula 4 we get


Now we enter tex2html_wrap_inline4022 and get


From (3) and (6) we conclude


Therefore, by entering tex2html_wrap_inline4000 we have


By universal instantiation it follows that


Entering tex2html_wrap_inline4022 gives


By logic, formulas 9 and 13 give


We can now either continue reasoning in tex2html_wrap_inline4022 or exit tex2html_wrap_inline4022 and get


Together with the universally instantiated form of the tex2html_wrap_inline4066 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 tex2html_wrap_inline4022 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 up previous
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