Why S4 Implies S5

---

Why S4 Implies S5

Necessitation Rule: (∀Q)(⊢Q>□Q)

(CT) Corollary of T: T > (∀Q)(Q>◊Q)

Definition 1: S4 = (T&(K&4))

Definition 2: B = (∀P)(P>□◊P)

Definition 3: S5 = (S4&B)

A1 (Assumption 1): S4

D1 (Substitution, Def 1, A1): T&(K&4)

D2 (Simplification, D1): T

D3 (Modus Ponens, D2, CT): (∀Q)(Q > ◊Q)

A2 (Assumption 2): ~(∀P)(P > □◊P)

1 (Material Implication, A2): ~(∀P)(~PV□◊P)

2 (Change of Quantifier, 1): (∃P)~(~PV□◊P)

3 (De Morgan’s Law, 2): (∃P)(~~P&~□◊P)

4 (Double Negation, 3): (∃P)(P&~□◊P)

5 (Existential Instantiation, 4): P&~□◊P

6 (Simplification, 5): P

7 (Universal Instantiation, D3): P > ◊P

8 (Modus Ponens, 7, 6): ◊P

9 (Necessitation Rule, 8): □◊P

10 (Simplification, 5): ~□◊P

11 (Conjunction, 9, 10): □◊P&~□◊P

AIP Assumed Indirect Proof (A2–11): (∀P)(P > □◊P)

D4 (Substitution, AIP, Def 2): B

D5 (Conjunction, A1, D4): S4&B

D6 (Substitution, D5, Def 3): S5

Assumed Conditional Proof (A1-D9): S4 > S5

Conclusion: S4 > S5