BACK TO NATURAL DEDUCTION
Sara Negri, Jan von Plato · Cambridge University Press eBooks · 2001
The derivability relation of single succedent sequent calculus, written Γ⇒ C, is closely related to the derivability relation of natural deduction, written F h C in Chapter 1. Usually the latter is intended as: There exists a natural deduction derivation tree finishing with C and with open assumptions contained in Γ. Thus the derivability relation is not a formal but a metamathematical one. As a consequence, weakening is “smuggled in”: If C is derivable from F and if each formula of Γ is contained in Δ, then C is derivable from Δ. If the metamathematical derivability relation is used, it will be difficult to state in terms of natural deduction what weakening amounts to. We shall consider only a formal derivability relation for natural deduction, in which Γ is precisely the multiset of open assumptions in a natural deduction derivation. One consequence of the use of a formal derivability relation is that not all sequent calculus derivations have a corresponding natural deduction derivation. For example, if the last step is a left weakening, it will have no correspondence in natural deduction and similarly if the last step is a contraction. However, such steps are artificial additions to a derivation. Equivalence of derivability in natural deduction and sequent calculus will obtain if no such “useless” weakenings or contractions are present. We shall show in detail that weakening is, in terms of natural deduction, the same as the vacuous discharge of assumptions and that contraction is the same as multiple discharge. This explanation was already indicated in Section 1.3.