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

Major Section:
Reference
Type of Math Object:
Definition
Parent:

## Mathematics Subject Classification

03B42 Logics of knowledge and belief (including belief change)
03B45 Modal logic (including the logic of norms)

## Recent Activity

May 17
new image: sinx_approx.png by jeremyboden
new image: approximation_to_sinx by jeremyboden
new image: approximation_to_sinx by jeremyboden
new question: Solving the word problem for isomorphic groups by mairiwalker
new image: LineDiagrams.jpg by m759
new image: ProjPoints.jpg by m759
new image: AbstrExample3.jpg by m759
new image: four-diamond_figure.jpg by m759
May 16
new problem: Curve fitting using the Exchange Algorithm. by jeremyboden
new question: Undirected graphs and their Chromatic Number by Serchinnho

## Info

Owner: CWoo
Added: 2012-06-21 - 05:21
Author(s): CWoo

## Versions

(v9) by CWoo 2013-03-22
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 66, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.3, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.8785535097122192, "perplexity_flag": "middle"}