Structural Rules in Natural Deduction with Alternatives, Bulletin of the Section of Logic, pp. 35 (2023), Early View.
doi:10.18778/0138-0680.2023.6
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 proof system 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 kinds of irrelevance to natural deduction proofs: (a) the rule of explosion (from a contradiction, 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 to the 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.
This paper appears in a special issue of the Bulletin of the Section of Logic on Bilateralism and Proof-Theoretic Semantics.
download pdf
You are welcome to download and read this document. I welcome feedback on it. Please check the final published version if you wish to cite it. Thanks.
