Natural Deduction via Context

 

  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

Note that these rules can be replaced by lifting axioms. Thus importation is replaced by

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

assumption

In analogy to the restriction to the rule of introduction in formal systems of natural deduction, we will have to restrict the rule of universal generalization to ensure that the variable being generalized does not occur free in any of the terms of the current context; see [49].

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.

• Postponing Preconditions via