Ruth Barcan Marcus on the Deduction Theorem in Modal Logic

ABSTRACT

In this paper, I examine Ruth Barcan Marcus's early formal work on modal systems and the deduction theorem, both for the material and the strict conditional. Marcus proved that the deduction theorem for the material conditional does not hold for system S2 but holds for S4. This last result is at odds with the recent claim that without proper restrictions the deduction theorem fails also for S4. I explain where the contrast stems from. For the strict conditional, Marcus proved the deduction theorem for S4 though restricted to arguments with necessary premises. I discuss Marcus's result and analyze her philosophical position on the significance of the deduction theorem for modal systems designed to express the notion of deducibility.

KEYWORDS:

• Ruth Barcan Marcus
• deduction theorem
• modal logic
• strict implication

Acknowledgments

I thank an anonymous referee of this journal for very helpful feedback which has been instrumental in substantially improving the paper. I am particularly grateful to Dave Gilbert for introducing me to the contemporary debate on the deduction theorem in modal logic and for many conversations on the topic. All mistakes are mine, but there would have been quite a few more had I not been so generously helped by both of them.

Notes

1 From 1946 to 1948, Ruth Barcan Marcus published her work as Ruth C. Barcan. For all her subsequent publications, she used the name ‘Ruth B. Marcus’. Marcus originally changed her publishing name because Alonzo Church, then editor of the Journal of Symbolic Logic, asked her to use her married and so, at the time, legal name. Though this was not initially her choice, she kept using the name ‘Marcus’ – under which she had meanwhile become well known – even after her divorce.

2 I employ $\to$ for the material conditional in place of Lewis's and Marcus's horseshoe, ⇒ for strict implication in place of their fishhook sign, $\leftrightarrow$ for the material biconditional (iff) in place of the triple bar, ⇔ for strict equivalence in place of the quadruple bar, and $\wedge$ in place of · for conjunction. At the time, Marcus, like Lewis, used the terms ‘implication’ and ‘equivalence’ rather than ‘conditional’ and ‘biconditional’. Thus she spoke of material implication and of material equivalence for $\to$ and $\leftrightarrow$. This terminology is now obsolete, but I sometimes use it when reporting her results.

3 Throughout the paper, I let expressions refer to themselves without placing them within quotation marks.

4 I have reformulated this rule switching the names of the formulas in the original text to match Marcus's later formulation of theorems XIX and XIX*.

5 In the 40s and 50s, Marcus does not discuss the semantic significance of BF and CBF, though this will become one of the central themes of her later work.

6 So, in this paper I follow Lewis's and Marcus's preference for writing $(A\Rightarrow B)$ over the equivalent $◻(A\to B)$.

7 74 is now standardly assumed as Axiom K.

8 It is unclear why Marcus numbered the most crucial theorems with a Roman numeral, supposed to be reserved for rules.

9 Marcus marks with an asterisk the results holding in S4 but not S2.

10 XIX and XIX* are hard to read. Their main connective is the strict conditional.

11 This requires extending the adjunction rule.

12 In this paper, I use the terms ‘hypotheses’, ‘assumptions’ and ‘premises’ interchangeably.

13 Clearly if 2${}^{†}$ fails so does the stronger 3${}^{†}$.

14 On the distinction between admissible and derivable rules and their relation to the deduction theorem, see Dosen 1996; Hakli and Negri 2012, Section 2.5; Iemhoff  2016; and Franks 2021, Sections 7 and 8. Sundholm (1983, 148) distinguishes instead between rules of proof and rules of inference.

15 In the literature on structural completeness, the term ‘derivable’ is reserved for rules that apply to extra-logical hypotheses. In a less technical, more general sense of ‘derivable’ the term includes all rules that can be derived in an axiomatized system. The primitive rules of a system are also included in this second sense of ‘derivable’, as there is a derivation from their premises to their conclusion, by application of the rule itself. Marcus's rules VI and VII of S2 are derivable only in the second, more general sense.

16 The rules that apply only to theorems are those to which there corresponds only a limited theorem: given a rule from A to B, $⊢(A\to B)$ holds only if A is a theorem.

17 They may be algebraic too, as Parry's matrix for Marcus's S2.

18 For a more comprehensive explanation, see Franks 2021, Section 8; and Hakli and Negri 2012, 857–859.

19 On the relations between these systems and their model theory, see Parry 1934, Halldén 1951 and Kripke 1965. See also Hughes and Cresswell 1996, 193–209.

20 In Lemmon's axiomatization of S2, where substitution of equivalents is not a primitive rule, rule VII is assumed as primitive (Lemmon 1957, 177–178).

21 Quine (1946 and 1947), who reviewed Marcus's first three papers for the Journal of Symbolic Logic, was also the papers' referee, as reported by Burgess (2014, 1570).

22 Our discussion of the deduction theorem is focused on the propositional case. Marcus proves the theorem for the quantified system. Thus she needs to discuss also the case in which the axiom is the result of generalization applied to another axiom and is then of the form $\mathrm{\forall }{\alpha }_1\cdots \mathrm{\forall }{\alpha }_n(E\Rightarrow H)$. This case employs the Barcan formula to transform these quantifications of necessities into necessary quantifications and then proceeds as above. Finally, substitution is applied to prove the result for the initial quantified formula.

23 Independently from interpretative issues, Lemmon (1977, 7) advocates as simpler the formulation of these systems separating the propositional calculus as a base and taking □ rather than ⋄ as primitive, so that strict implication can be easily defined in terms of the material conditional.

24 For a comprehensive treatment of the deduction theorem in modal logic, see Hakli and Negri's (2012) discussion of the interplay between the deduction theorem, different notions of validity and different notions of derivation. Franks (2021) discusses the broader history of the deduction theorem and its conceptual relation with modus ponens and the notion of derivability.

25 This is exactly the thesis of those who claim that the deduction theorem fails for S4 when axiomatized with the rule of necessitation, e.g. Smorynski 1984, Chagrov and Zakharyaschev 1997 and Ganguli and Nerode 2004, as reported in Hakli and Negri 2012, 851.

26 Clearly, these remarks are purely speculative, but not unmotivated.

27 Interestingly Smorynski, who takes necessitation to obstruct the deduction theorem, suggests the possible solution of modifying the system ‘by adding $\mathrm{◻A}$ as an axiom for any instance A of an axiom. [Necessitation] is then a derived rule of inference, but no longer an obstacle to the validity of the Deduction Theorem’ (1984, 455). This is analogous to what Marcus did for generalization. On Smorynski's view, see Hakli and Negri 2012 which offers a comprehensive discussion of the recent debate.

28 Feys (1965, 73) calls ‘Becker's rules’ all rules like VI and VII that start from a strict implication and derive a strict implication with the original antecedent and consequent prefixed by the same modality.

29 These rules are not intrinsically problematic. They become such if one wants to extend the deduction theorem to them with no qualifications or restrictions.

30 Like Marcus, Feys considers a matrix that satisfies all the axioms and rules of S2 but not the characteristic axiom of S3, and concludes that this establishes that the deduction theorem fails for S2 (Feys 1965, 79–80). Strangely, Feys does not credit Marcus for this result, though he credits her for proving the deduction theorem for S4 (1965, 165) and both these results occur in Barcan 1946b.

31 For proofs of the deduction theorem for S2, see Satre 1972 which pursues Zeman's suggestion and proves the deduction theorem for the Lewis' systems based on appropriate restrictions of their modal rules, and Surma 1972 where the theorem is proved for certain fragments of S2. Kripke shows that S2 can be axiomatized with modus ponens (for the material conditional) as its only rule and credits Craig (1953) for this result (Kripke 1965, 206).

32 Step 1 holds by assumption (for reduction) that the deduction theorem for the strict conditional holds with no restrictions; step 2 is the assumption that $◻\mathrm{\Gamma }$ is provable.

33 Among other results, Martin (1960, 27) proves that in system S1 the weak deduction theorem for strict implication (taken as a rule from $A⊢B$ to $⊢(A\Rightarrow B$)) and the rule of necessitation are equivalent. He also proves (1960, 32–33) that if an intermediate deduction theorem for strict implication is added to S5 as a rule (from $A,B⊢C$ to $A⊢(B\Rightarrow \diamond C)$), then necessity is reduced to truth.

34 The restriction needed to save the theorem may be stated as a restriction on the theorem, as Marcus does, or as a restriction on the problematic rule, as Zeman suggests. The result is the same, though it corresponds to different conceptions of derivability in S4.

35 To this she later adds, ‘it would be a curious explication of the concept of deducibility if, although B followed from the premise A, B could not be said to be deducible from it’ (Marcus 1953, 235). Prima facie, this sentence and the one I quoted in the main text appear to be making the same point, yet the second sentence was removed from the 1993 reprint of the 1953 article in Modalities: Philosophical Essays. Perhaps this second statement was cut because redundant and less clear than the first?

36 I thank Pierdaniele Giaretta for bringing this point to my attention. See also Kennedy 2022, Section 2.5.3.

37 Dosen (1996) interprets the deduction theorem as expressing a form of deductive completeness.

38 Though, if the generalized contemporary problem has any merit, the standard axiomatization of S3 jeopardizes the deduction theorem due to its necessitation rule for axioms and tautologies.

39 In the original 1953 edition, the second turnstile is missing from II and III. In 1993, Marcus adds ‘is a theorem’ to the original formulations.

40 In a footnote, Marcus (1953, 235) credits Carnap (1946) for the proof of III for S5.

41 Franks (2021) discusses this sort of question for the conditional both for classical and for intuitionistic logic.

42 In this paragraph, I use ‘A follows from B’ and ‘A implies B’ as synonymous with ‘B is deducible from A’ to improve readability.