Abstract

Eight distinct rules for implication in the antecedent for the sequent calculus, one of which being Gentzen’s standard rule, can be derived by successively applying a number of cuts to the logical ground sequent A → B, A ⇒ B. A naive translation into natural deduction collapses four of those rules onto the standard implication elimination rule, and the remaining four rules onto the general elimination rule. This collapse is due to the fact that the difference between a formula occurring in the succedent of a premise of a sequent calculus rule and that formula instead occurring in the antecedent of the conclusion cannot be adequately expressed in the framework of natural deduction. In contrast to this, the difference between a formula occurring in the succedent of the conclusion of a sequent calculus rule and that formula instead occurring in the antecedent of a premise corresponds exactly to the distinction between the standard implication elimination rule and its general counterpart. This incongruity can be remedied by introducing a notational facility that requires of the particular premise of a rule to which it is attached to be an assumption, i.e., to prevent it from being the conclusion of another rule application. Applying this facility to implication elimination results in eight distinct rules that correspond exactly to the eight sequent calculus rules. These eight rules are presented and discussed in detail. It turns out that a natural deduction calculus (for positive implication logic) that employs the rule corresponding to the standard left implication rule of the sequent calculus as well as a rule for explicit substitution can be seen as a natural deduction style sequent calculus.