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.

• The talk is an online presentation at our Applied Logic Workshop.

• The slides for the talk are available here.