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 $w R u$ and $u R t$ . 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 $w R v$ . Since $w R u$ , $\models_{u}\square p$ , which means $\models_{s}p$ for all $s$ such that $u R s$ . Since $u R t$ , we have $\models_{t}p$ , or $t\in V(p)$ , or $w R t$ . 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 $w R u$ , we have $\models_{u}\square A$ , or for all $u$ with $w R u$ and all $t$ with $u R t$ , we have $\models_{t}A$ . If $w R u$ and $u R t$ , $w R t$ 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
Canonical name	ModalLogicS4
Date of creation	2013-03-22 19:34:01
Last modified on	2013-03-22 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