Natural Deduction with Alternatives: on structural rules, and identifying assumptions

March 17, 2022

Abstract: In this talk, I will introduce natural deduction with alternatives, explaining how this framework provides 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, in addition to the familar intuitionistic restrictions of these systems. Each of these proof systems have identical connective rules. As we expect in substructural logics, different logical systems are given by varying the structural rules in play. The distinctly classical behaviour of these systems is given by the presence of alternatives (formulas in consequent, or positive position, other than the conclusion of the proof) in addition to assumptions (formulas in antecedent, or negative position). Unlike multiple conclusion proof systems, this proof system is single conclusion, but unlike traditional natural deduction à la Gentzen or Prawitz, the context in which that formula is proved consist of formulas ruled in (assumptions) and formulas ruled out (alternatives). The result is a proof system that is mildly bilateralist.

I will introduce this framework, and show how the presence of alternatives in natural deduction can give us a new angle from which to view the impact of the structural rules of weakening and contraction, and the difference between multiplicative and additive connectives.

• The talk was a face-to-face presentation at the 2022 Bilateralism and Proof-Theoretic Semantics Conference at the Ruhr University Bochum, in Germany.

• The slides for the talk are available here.