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$?


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)$:


  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.

  • 1
    $\begingroup$ When you inferred step 7, didn't you use the rule {($\alpha$→$\beta$), ($\beta$→$\gamma$} $\vdash$ ($\alpha$→$\gamma$)? $\endgroup$ – Doug Spoonwood May 25 '14 at 0:55
  • 1
    $\begingroup$ Sorry, not modus ponens. Transitivity of the material conditional I should have said. Thanks. $\endgroup$ – Hunan Rostomyan May 25 '14 at 1:11

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).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.