Contents

(0,1)-category

(0,1)-topos

Examples

# Contents

## Idea

The flavor of (classical) modal logic called $S4$ is (classical) propositional logic equipped with a single modality usually written “$\Box$” subject to the rules that for all propositions $p, q \colon Prop$ we have

1. $\Box K \colon \Box(p \to q) \to (\Box p \to \Box q)$ (K modal logic)

2. $\Box T \colon \Box p \to p$ (T modal logic)

3. $\Box 4 \colon \Box p \to \Box \Box p$. (S4 modal logic)

4. (in addition in S5 modal logic one adds: $\lozenge p \to \Box \lozenge p$).

Traditionally the canonical interpretation of the Box operator is that $\Box p$ is the statement that “$p$ is necessarily true.” (The de Morgan dual to the necessity modality is the “possibility” modality.) Then the interpretation of $\Box 4$ 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 $\Box_i$ of this form, the resulting modal logic is denoted $S4(n)$. Here $\Box_i p$ is sometimes interpreted as “the $i$th agent knows $p$.”

In intuitionistic (or constructive) Modal Logic, one does not expect the possibility modality to be dual to the necessity modality, necessarily. Alex Simpson has written in his thesis the most used constructive modal logic system, but other systems exist.

## 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 $S4_{(m)}$)

$S4_{(m)}\vdash \phi \Rightarrow \mathcal{S}4(m)\models \phi.$

###### Proof

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

Suppose that $\mathfrak{M}= ((W,R),V)$ where $R$ is a reflexive transitive relation on $W$. We have to check that $\mathfrak{M}\models (4)$.

Suppose $\mathfrak{M},w\models K p$, then, for every $t$ with $R w t$, we have $\mathfrak{M},t\models p$. Now suppose we seek to check that $\mathfrak{M},w\models K K p$ so we have $t$ with $R w t$ and want $\mathfrak{M},t\models K p$, so we look at all $u$ with $R t u$ and have to see if $\mathfrak{M},u\models p$, but as $R w t$ and $R t u$ hold then $R w u$ holds, since $R$ is transitive, and we then know that $\mathfrak{M},u\models p$.

## References

The terminology “S4” in modal logic originates with:

The “possible worldsKripke semantics of S4 originates with:

A natural deduction-formulation and making explicit the modal operator as a comonad:

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