# How do you reduce repeated modality in S5?

Kenneth Konyndyk's Introductory Modal Logic claims (p. 55) that all formulas in S5 with a modal degree greater than 1 can be reduced to degree 1. By degree, he means the maximum number of modal operators that any one sentence letter is in the scope of (e.g., ◊p has degree 1, □◊p has degree 2, (□◊p v ◊p) has degree 2, ◊(□◊p v ◊p) has degree 3).

Konyndyk doesn't really explain how to do this reduction. He gives exercises where he asks the reader to reduce several formulas to degree 1, but he never goes through an example that uses a two-place truth function, so I have no clue how to do it.

For a specific example, how would you turn ◊(◊p ⊃ ◊p) into something where each instance of p is only in the scope of one modal operator?

For another example, how would you turn □(p v □q) into something where each sentence letter is only in the scope of one modal operator?

Edit: By "reduce," Konyndyk means that there should be a necessary equivalence between the iterated modality and the single-degree formula, so it's not enough to derive a simpler formula if that formula can't also be used to derive the starting point.

Edit 2: I can only use Fitch's natural deduction laws to transform formulas.

To address your examples in (ascending) order of complexity, in S5 □ distributes over disjunction (too) as long as one of the disjuncts is modal (starts with □ or ◊). So

□(p v □q) = □p v □□q = □p v □q

As for ◊(◊p ⊃ ◊q), first rewrite the implication (as in classical logic) to ◊(¬◊p v ◊q), then apply the ◊ to □ interchange (definition) to the first disjunct, yielding ◊(□¬p v ◊q), then distribute ◊, obtaining ◊□¬p v ◊◊q and reduce each of the disjuncts □¬p v ◊q.

The equivalences I used here can be found in most reasonable texts on S5, e.g. see this page.

Hughes & Cresswell's book proves these more systematically and they give (in chapter 5) a general algorithm for putting S5 formulas in (modal conjunctive) normal form, which is basically along the lines of what I've done above:

1. Rewrite all "unusual" connectors (e.g. implication) using just ¬, v, and ∧ (and with □ and ◊ as well if you have some unusual modal connectors too).
2. Eliminate ¬ immediately before parentheses (by De Morgan's laws) and before modal operators by interchange (as I did above in the 2nd example above with ¬◊p = □¬p).
3. Reduce iterated modalities to the right-most one (e.g. ◊□¬p = □¬p).
4. When you're left with a modal operator in front of a parenthesis, either distribute it unconditionally (which works for ◊ over v and for □ over ∧ in other modal logics) or using the special distributivity rules that hold in S5 as long as one of inner terms is modal, which is what I did in the first example. The only time where you can't do this (in S5) is when you have something like □(p v q v r v ...) (or ◊(p ∧ q ∧ r ∧ ... )) where the conjuncts or disjuncts are of degree 0.

Steps 2-4 above reduce the degree by 1. You may then need to repeat them again to reduce the degree again.

• The fact that □ distributes is exactly what I'm trying to prove. I can't use it as a step. Commented Mar 10, 2021 at 16:07
• @EthanBradley: if you want a proof all the properties/theorems needed above (from the S5 axioms), ask separately. They are somewhat lengthy proofs, in toto. A book like Hughes & Cresswell has them, but it's about the first four chapters or so... Commented Mar 10, 2021 at 16:10
• @EthanBradley: also there are different things (all) called Fitch-style proofs for modal logic. I have no idea what kind your book is using. Commented Mar 10, 2021 at 16:26