# modal logic S4

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

• (T) $\square A\to A$, and

• (4) $\square A\to\square\square A$.

###### 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 $\models_{w}\square p$. By assumption  , we have $\models_{w}\square p\to\square\square p$. Then $\models_{w}\square\square p$. This means $\models_{v}\square p$ for all $v$ such that $wRv$. Since $wRu$, $\models_{u}\square p$, which means $\models_{s}p$ for all $s$ such that $uRs$. Since $uRt$, we have $\models_{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 $\models_{w}\square A$. We want to show $\models_{w}\square\square A$, or for all $u$ with $wRu$, we have $\models_{u}\square A$, or for all $u$ with $wRu$ and all $t$ with $uRt$, we have $\models_{t}A$. If $wRu$ and $uRt$, $wRt$ since $R$ is transitive. Then $\models_{t}A$ by assumption. Therefore, $\models_{w}\square A\to\square\square A$. ∎

As a result,

###### Proposition 2.

S4 is sound in the class of preordered frames.

In addition, using the canonical model of S4, which is preordered, we have

###### Proof.

Since S4 contains T, its canonical frame $\mathcal{F}_{\textbf{S4}}$ is reflexive. We next show that the canonical frame $\mathcal{F}_{\Lambda}$ of any consistent  normal logic $\Lambda$ containing the schema 4 must be transitive. So suppose $wR_{\Lambda}u$ and $uR_{\Lambda}v$. If $A\in\Delta_{w}:=\{B\mid\square B\in w\}$, then $\square A\in w$, or $\square\square A\in w$ by modus ponens on 4 and the fact that $w$ is closed under modus ponens. Hence $\square A\in\Delta_{w}$, or $\square A\in u$ since $wR_{\Lambda}u$, or $A\in\Delta_{u}$, or $A\in v$ since $uR_{\Lambda}v$. As a result, $wR_{\Lambda}v$, and therefore $\mathcal{F}_{\textbf{S4}}$ is a preordered frame. ∎

Title modal logic S4 ModalLogicS4 2013-03-22 19:34:01 2013-03-22 19:34:01 CWoo (3771) CWoo (3771) 9 CWoo (3771) Definition msc 03B42 msc 03B45 S4 4