The formal theory of context can be used to
represent inference and reason in the style of natural deduction.
This requires lifting axioms (or lifting rules) to treat the
context which a reasoning system is in as a formal object.
If *p* is a sentence and we are in some context *c*, we define
a new context so that it validates the
following rules:

**importation**-
**discharge**-

To make the presentation simpler we write them in the rule form. An interesting rule which can be derived from the above is

**assumption**-

To illustrate the rules we now give a natural-deduction style proof
of the **above** theorem, which was introduced in §4.
This theorem involves the lifting of the theory of above
into the context of situation calculus. The proof should be compared
to the Hilbert style proof which was given in §4.

**Proof !above(above):**
We begin with the direction of formula 4

It follows by universal instantiation that

By the **importation** rule we get

Therefore, by entering the context we get

Now, from formulas 3 and 6 it follows that

By entering we get

By instantiating the universal quantifier over situations we get

Therefore, by propositional logic we have

Therefore, by the **importation** rule we get

Now, by entering the context we get

By logic from formulas 23 and 29 it follows that

By exiting the context we get

The direction of formula 5

By propositional logic we have

Together with the **importation** rule the above formula
allows us to infer

By logic from (31) and (34) we get

Using the rule **discharge** it follows that

Therefore, by universal generalization we obtain what was to be proved

In the above proof we have entered the context in a number of instances. This creates an interesting example because it might not be obvious in which context the term is to be interpreted. However, since the logic needs to keep track of which contexts were entered in the process of reasoning, the answer becomes obvious: the term will be interpreted in the next outer context (see §3 for discussion on sequences of contexts).

We gave two treatments of the key argument: one in natural deduction (§4) and one Hilbert-style (above). This kind of proof transformation is logical routine, and any textbook on proof theory (say, the recent [57]), tells all about it.

Sun Jul 12 14:45:30 PDT 1998