Structural rules in natural deduction with alternatives

Greg Restall*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


Natural deduction with alternatives extends Gentzen–Prawitz-style natural deduction with a single structural addition: negatively signed assumptions, called alternatives. It is a mildly bilateralist, single-conclusion natural deduction proofsystem in which the connective rules are unmodified from the usual Prawitz introduction and elimination rules — the extension is purely structural. This framework is general: it can be used for (1) classical logic, (2) relevant logic without distribution, (3) affine logic, and (4) linear logic, keeping the connective rules fixed, and varying purely structural rules. The key result of this paper is that the two principles that introduce kindsofirrelevanceto natural deduction proofs: (a) the rule of explosion (from acontradiction, anything follows); and (b) the structural rule of vacuous discharge;are shown to be two sides of a single coin, in the same way that they correspond tothe structural rule of weakening in the sequent calculus. The paper also includes a discussion of assumption classes, and how they can play a role in treating additive connectives in substructural natural deduction.
Original languageEnglish
Article number14404
Pages (from-to)109-143
Number of pages35
JournalBulletin of the Section of Logic
Issue number2
Early online date18 Jul 2023
Publication statusPublished - 1 Dec 2023


  • Proof
  • Natural deduction
  • Classical logic
  • Bilateralism
  • Substructual logics


Dive into the research topics of 'Structural rules in natural deduction with alternatives'. Together they form a unique fingerprint.

Cite this