The inference pattern known as disjunctive syllogism (DS) appears as a derived rule in Gentzen’s natural deduction calculi ni and nk. This is a paradoxical feature of Gentzen’s calculi in so far as DS is sometimes thought of as appearing intuitively more elementary than the rules \(\vee \) E, \(\lnot \) E, and EFQ that figure in its derivation. For this reason, many contemporary presentations of natural deduction depart from Gentzen and include DS as a primitive rule. However, such departures violate the spirit of natural deduction, according to which primitive rules are meant to relationally define logical connectives via universal properties (§2). This situation raises the question: Can disjunction be relationally defined with DS instead of with Gentzen’s \(\vee \) I and \(\vee \) E rules? We answer this question in the affirmative and explore the duality between Gentzen’s definition and our own (§3). We argue further that the two universal characterizations, rather than provide competing relational definitions of a single disjunction operator, disambiguate natural language’s “or” (§4). Finally, this disambiguation is shown to correspond exactly with the additive and multiplicative disjunctions of linear logic (§5). The hope is that this analysis sheds new light on the latter connective, so often deemed mysterious in writing about linear logic.
