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, the proof system is single conclusion, since one formula in positive position is singled out as the conclusion. The context in which that formula is proved consists, in general, of formulas ruled in (assumptions) and formulas ruled out (alternatives).
In sequent systems, and in some natural deduction systems that use labels, the structural rules of contraction and weakening govern an explicitly represented structure, such as a set or multiset or sequence of formulas occurring in each sequent. In this natural deduction framework, the structural rules have their force at the point of discharge, or more generally, at any point at which it is important to determine whether two occurrences of the same formula (in positive position, or in negative position) are the same assumption or the same alternative. There is no explicit representation of any structure of assumptions or alternatives, other than the structure of the proof itself.
Along the way, this presentation 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); (3) the sense in which the operational rules for a connective might be understood as providing a definition of that connective; and (4) the use of the identity or difference of variables in type systems such as the typed λ calculus in keeping track of the sameness or difference of assumptions as opposed to the sameness or difference of the things assumed.
