Prove that modal logic S4 is properly contained in S5

Question

Is it possible to prove using just the semantics for $S_4/S_5$ that $S_4$ is properly contained in $S_5$?
I can see how one could show that there is a theorem of $S_5$ which is not a theorem of $S_4$, but I can't see how one could show that every theorem of $S_4$ is also a theorem of $S_5$?

Answer 1

Hughes and Cresswell's Intro to Modal Logic has a short proof that $\Box p \rightarrow\Box\Box p$ is a theorem of S5, and since that's the axiom you add to T to get S4, that proves the containment.

If you want a proof in terms of Kripke semantics, every S5 model is also an S4 model, because the accessibility relation for S5 is more constrained (symmetric, not just reflexive and transitive).

Answer 2

We start with a definition of the relation of 'containment' between logics:

Definition. (Sublogicality) Given logics $\mathbf L$ and $\mathbf L'$, we say that $\mathbf L \leq \mathbf L'$ (to be read: $\mathbf L$ is a sublogic of $\mathbf L'$) iff for all formulas $\varphi$, if $\vdash_{\mathbf L}\varphi$ then $\vdash_{\mathbf L'}\varphi$.

Recall that:

• $\mathbf{S4}$ is characterized by axiom 4: $\Box\varphi \rightarrow \Box\Box\varphi$ (accessibility relation is a preorder);
• $\mathbf{S5}$ is characterized by axiom 5: $\Diamond\varphi \rightarrow \Box\Diamond\varphi$ (accessibility relation is an equivalence).

An easy way of proving $\mathbf{S4} \leq \mathbf{S5}$ would be to derive axiom (4) in $\mathbf{S5}$, i.e., to show that $\vdash_\mathbf{S5} (4)$:

Proof.

1. $\Diamond\lnot \varphi \rightarrow \Box\Diamond\lnot \varphi$ (an instance of axiom 5)
2. $\lnot\Box\Diamond\lnot \varphi \rightarrow \lnot\Diamond\lnot \varphi$ (the contrapositive of 1)
3. $\Diamond\Box \lnot\lnot \varphi \rightarrow \lnot\Diamond\lnot \varphi$ (pushing the negation in and flipping the operators)
4. $\Diamond\Box \varphi \rightarrow \Box \varphi$ (double-negation elimination and box-diamond duality)
5. $\Box\Diamond\Box \varphi \rightarrow \Box\Box \varphi$ (RE, 4)
6. $\Box \varphi \rightarrow \Box\Diamond\Box \varphi$ (instance of axiom B: $\varphi \rightarrow \Box\Diamond \varphi$)
7. $\Box \varphi \rightarrow \Box\Box \varphi$ (propositional logic, 6, 5)

If we wanted to prove proper sublogicality ($\mathbf L \lneq \mathbf L'$) we could devise an $\mathbf{S4}$ model that violates axiom (5). For details about the RE rule used at step (5), take a look at: Chellas (1980), §8.2.