# 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$.

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 $\mathcal{F}$ iff $\mathcal{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 $\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.

###### 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}_{\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. ∎

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