Natural Deduction Proof for Substructural, Constructive and Classical Logics

May 1, 2024

Abstract: Since the 1990s, we have seen how to understand a very wide range of logical systems (classical logic, intuitionistic logic, dual intuitionistic logic, relevant logics, linear logic, the Lambek calculus, affine logic, orthologic and more) by way of the distinction between operational and structural rules. We can have one set of rules for a connective (say, conjunction, negation, or the conditional) in a sequent calculus, and get different logical behaviour depending on the shape of the sequents allowed and the structural rules governing those sequents.

In this talk, I will consider the relationship between the “big four” traditional substructural logics—intuitionistic, relevant, affine and linear—corresponding to the four options for including or excluding the structural rules of weakening and contraction, in the setting of Gentzen/Prawitz-style natural deduction proofs for implication and the simply typed λ calculus. Such a natural deduction setting—in which proofs have any number of premises and a single conclusion—has a natural bias toward constructive, or intuitionistic logic.

I will show how the choice of whether to “go classical”, expanding the structural context to allow for more than one formula in positive position is orthogonal to the choice of the other structural rules, so that even in the context of natural deduction proofs, the familiar pair of traditional implication introduction and elimination rules gives rise to eight different propositional logics, four of which are “classical” and four of which are “constructive”. Furthermore, the familiar double-negation translation of classical logic inside intuitionistic logic generalises to the other three classical/constructive pairings.

I will explain these results, and, if there is time, I will end the talk with some reflections on what this might mean for the relationship between classical and constructive reasoning.

  • The talk is a presentation at the Leeds Logic Seminar.

  • If, for some reason you’d like to see the slides, they’re here.


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.