Structural Rules in Natural Deduction with Alternatives (article in progress)

 download pdf

You are welcome to download and read this document. I especially welcome feedback on it. As it is not yet published in final form, if you want to cite the paper, please check with me first. Thanks.

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.

Do you like this, or have a comment? (I especially value feedback on work which is yet to be be published in final form.) If you do, please  share or reply on Twitter, or  email me.

← Collection Frames for Distributive Substructural Logics | Writing Archive


I’m Greg Restall, and this is my personal website. ¶ I am the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews.



To receive updates from this site, you can subscribe to the  RSS feed of all updates to the site in an RSS feed reader, or follow me on Mastodon at, where I’ll update you if anything is posted.