modal logic S4
The modal logic S4 is the smallest normal modal logic containing the following schemas:

•
(T) $\mathrm{\square}A\to A$, and

•
(4) $\mathrm{\square}A\to \mathrm{\square}\mathrm{\square}A$.
In this entry (http://planetmath.org/ModalLogicT), we show that T is valid in a frame iff the frame is reflexive^{}.
Proposition 1.
4 is valid in a frame $\mathrm{F}$ iff $\mathrm{F}$ is transitive^{}.
Proof.
First, suppose $\mathcal{F}$ is a frame validating 4, with $wRu$ and $uRt$. Let $M$ be a model with $V(p)=\{v\mid wRv\}$, where $p$ a propositional variable. So ${\vDash}_{w}\mathrm{\square}p$. By assumption^{}, we have ${\vDash}_{w}\mathrm{\square}p\to \mathrm{\square}\mathrm{\square}p$. Then ${\vDash}_{w}\mathrm{\square}\mathrm{\square}p$. This means ${\vDash}_{v}\mathrm{\square}p$ for all $v$ such that $wRv$. Since $wRu$, ${\vDash}_{u}\mathrm{\square}p$, which means ${\vDash}_{s}p$ for all $s$ such that $uRs$. Since $uRt$, we have ${\vDash}_{t}p$, or $t\in V(p)$, or $wRt$. Hence $R$ is transitive.
Conversely, let $\mathcal{F}$ be a transitive frame, $M$ a model based on $\mathcal{F}$, and $w$ any world in $M$. Suppose ${\vDash}_{w}\mathrm{\square}A$. We want to show ${\vDash}_{w}\mathrm{\square}\mathrm{\square}A$, or for all $u$ with $wRu$, we have ${\vDash}_{u}\mathrm{\square}A$, or for all $u$ with $wRu$ and all $t$ with $uRt$, we have ${\vDash}_{t}A$. If $wRu$ and $uRt$, $wRt$ since $R$ is transitive. Then ${\vDash}_{t}A$ by assumption. Therefore, ${\vDash}_{w}\mathrm{\square}A\to \mathrm{\square}\mathrm{\square}A$. ∎
As a result,
Proposition 2.
S4 is sound in the class of preordered frames.
Proof.
Since any theorem in S4 is deducible from a finite sequence^{} consisting of tautologies^{}, which are valid in any frame, instances of T, which are valid in reflexive frames, instances of 4, which are valid in transitive frames by the proposition^{} above, and applications of modus ponens^{} and necessitation, both of which preserve validity in any frame, whence the result. ∎
In addition, using the canonical model of S4, which is preordered, we have
Proposition 3.
S4 is complete^{} in the class of serial frames.
Proof.
Since S4 contains T, its canonical frame ${\mathcal{F}}_{\text{\mathbf{S}\U0001d7d2}}$ is reflexive. We next show that the canonical frame ${\mathcal{F}}_{\mathrm{\Lambda}}$ of any consistent^{} normal logic $\mathrm{\Lambda}$ containing the schema 4 must be transitive. So suppose $w{R}_{\mathrm{\Lambda}}u$ and $u{R}_{\mathrm{\Lambda}}v$. If $A\in {\mathrm{\Delta}}_{w}:=\{B\mid \mathrm{\square}B\in w\}$, then $\mathrm{\square}A\in w$, or $\mathrm{\square}\mathrm{\square}A\in w$ by modus ponens on 4 and the fact that $w$ is closed under modus ponens. Hence $\mathrm{\square}A\in {\mathrm{\Delta}}_{w}$, or $\mathrm{\square}A\in u$ since $w{R}_{\mathrm{\Lambda}}u$, or $A\in {\mathrm{\Delta}}_{u}$, or $A\in v$ since $u{R}_{\mathrm{\Lambda}}v$. As a result, $w{R}_{\mathrm{\Lambda}}v$, and therefore ${\mathcal{F}}_{\text{\mathbf{S}\U0001d7d2}}$ is a preordered frame. ∎
By a proper translation^{}, one can map intuitionistic propositional logic PL${}_{i}$ into S4, so that a wff of PL${}_{i}$ is a theorem iff its translate^{} is a theorem of S4.
Title  modal logic S4 

Canonical name  ModalLogicS4 
Date of creation  20130322 19:34:01 
Last modified on  20130322 19:34:01 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  9 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B42 
Classification  msc 03B45 
Defines  S4 
Defines  4 