You are here
Homemodal logic S4
Primary tabs
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, 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.
Mathematics Subject Classification
03B42 no label found03B45 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections