Natural Deduction with Alternatives

November 6, 2020

Abstract: In this talk, I will introduce natural deduction with alternatives, explaining how this framework can provide a simple well-behaved single conclusion natural deduction system for a range of logical systems, including classical logic, (classical) linear logic, relevant logic and affine logic, by varying the policy for managing discharging of assumptions and retrieval of alternatives. Along the way, the talk will touch on (1) the connection between normalisation of a natural deduction proof and cut elimination in a corresponding sequent calculus; (2) the separation between the operational rules governing the connectives and the “antecedently given context of deducibility”, to borrow a phrase from Nuel Belnap’s essay, “Tonk, Plonk and Plink” (1962); and (3) the sense in which the operational rules for a connective might be understood as providing a definition of that connective.

Greg Restall—Natural Deduction with Alternatives from logicmelb on Vimeo.


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, and the Director of the Arché Philosophical Research Centre for Logic, Language, Metaphysics and Epistemology I like thinking about – and helping other people think about – logic and philosophy and the many different ways they can inform each other.


To receive updates from this site, subscribe to the RSS feed in your feed reader. Alternatively, follow me at, where most updates are posted.


This site is powered by Netlify, GitHub, Hugo, Bootstrap, and coffee.   ¶   © 1992– Greg Restall.