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.
The talk is an online presentation at our Applied Logic Workshop.
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. ¶ 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 @email@example.com, where most updates are posted.