Prove that modal logic S4 is properly contained in S5 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$?  
 A: 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.

*

*$\Diamond\lnot \varphi \rightarrow \Box\Diamond\lnot \varphi$ (an instance of axiom 5)

*$\lnot\Box\Diamond\lnot \varphi \rightarrow \lnot\Diamond\lnot \varphi$ (the contrapositive of 1)

*$\Diamond\Box \lnot\lnot \varphi \rightarrow \lnot\Diamond\lnot \varphi$ (pushing the negation in and flipping the operators)

*$\Diamond\Box \varphi \rightarrow \Box \varphi$ (double-negation elimination and box-diamond duality)

*$\Box\Diamond\Box \varphi \rightarrow \Box\Box \varphi$ (RE, 4)

*$\Box \varphi \rightarrow \Box\Diamond\Box \varphi$ (instance of axiom B: $\varphi \rightarrow \Box\Diamond \varphi$)

*$\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.
A: 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).
