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:
To make the presentation simpler we write them in the rule form. An interesting rule which can be derived from the above is
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 ), tells all about it.