nLab
the logic S4(m)

Idea

The flavor of modal logic called $S4$ is propositional logic equipped with a single modality usually written ”$\square$” subject to the rules that for all propositions $p,q:\mathrm{Prop}$ we have

1. $\square K:\square (p\to q)\to (\square p\to \square q)$ (K modal logic)

2. $\square T:\square p\to p$ (T modal logic)

3. $\square 4:\square p\to \square \square p$. (S4 modal logic)

Traditionally the canonical interpretation of the Box operator is that $\square p$ is the statement that ”$p$ is necessarily true.” Then the interpretation of $\square$ is that “If $p$ is necessarily true then it is necessarily necessarily true.” S4 modal logic appears in many temporal logics.

If instead of a single Box operator one considers $n\in \mathbb{N}$ box operators ${\square }_i$ of this form the resulting modal logic is denote $S4(n)$. Here ${\square }_{i}p$ is sometimes interpreted as “the $i$th agent knows $p$.”

Properties

Relation to Kripke frames

The models for T modal logic corresponded to Kripke frames where each relation $R_i$ is reflexive.
For $S4$ modal logic they are furthermore transitive.

Theorem (Soundness of $S{4}_{(m)}$)

$S{4}_{(m)}⊢\varphi \Rightarrow 𝒮4(m)\vDash \varphi .$

Proof

(We show this for $m=1$.)

Suppose that $𝔐=((W,R),V)$ where $R$ is a reflexive transitive relation on $W$. We have to check that $𝔐\vDash (4)$.

Suppose $𝔐,w\vDash Kp$, then, for every $t$ with $Rwt$, we have $𝔐,t\vDash p$. Now suppose we seek to check that $𝔐,w\vDash KKp$ so we have $t$ with $Rwt$ and want $𝔐,t\vDash Kp$, so we look at all $u$ with $Rtu$ and have to see if $𝔐,u\vDash p$, but as $Rwt$ and $Rtu$ hold then $Rwu$ holds, since $R$ is transitive, and we then know that $𝔐,u\vDash p$.

Related concepts

• K modal logic

• T modal logic

References

• Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter, Categorical and Kripke Semantics for Constructive S4 Modal Logic (pdf)

More on $S4$, $S{5}_{(m)}$ and their applications in Artificial Intelligence can be found in

• J.- J. Ch. Meyer and W. Van der Hoek, Epistemic logic for AI and Computer Science, Cambridge Tracts in Theoretical Computer Science, vol. 41, 1995.

General books on modal logics which treat these logics thoroughly in the general context include

• Patrick Blackburn, M. de Rijke and Yde Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001.

• Marcus Kracht, Tools and Techniques in Modal Logic, Studies in Logic and the Foundation of Mathematics, 142, Elsevier, 1999.