You are here
Homemodal logic S5
Primary tabs
modal logic S5
The modal logic S5 is the smallest normal modal logic containing the following schemas:

(T) $\square A\to A$, and

(5) $\diamond A\to\square\diamond A$.
S5 is also denoted by KT5, where T and 5 correspond to the schemas T and 5 respectively.
In this entry, we show that T is valid in a frame iff the frame is reflexive.
A binary relation $R$ on a set $W$ is said to be Euclidean iff for any $u,v,w$, $uRv$ and $uRw$ imply $vRw$. $R$ being Euclidean is firstorder definable:
$\forall u\forall v\forall w((uRv\land uRw)\to vRw).$ 
Proposition 1.
5 is valid in a frame $\mathcal{F}$ iff $\mathcal{F}$ is Euclidean.
Proof.
First, let $\mathcal{F}$ be a frame validating 5. Suppose $wRx$ and $wRy$. Let $M$ be a model based on $\mathcal{F}$, with $V(p)=\{x\}$. Since $\models_{x}p$, we have $\models_{w}\diamond p$, and so $\models_{w}\square\diamond p$, or $\models_{u}\diamond p$ for all $u$ such that $wRu$. In particular, $\models_{y}\diamond p$. So there is a $z$ such that $yRz$ and $\models_{z}p$. But this means $z=x$, whence $yRx$, meaning $R$ is Euclidean.
Conversely, suppose $\mathcal{F}$ is a Euclidean frame, and $M$ a model based on $\mathcal{F}$. Suppose $\models_{w}\diamond A$. Then there is a $v$ such that $wRv$ and $\models_{v}A$. Now, for any $u$ with $wRu$, we have $uRv$ since $R$ is Euclidean. So $\models_{u}\diamond A$. Since $u$ is arbitrary, $\models_{w}\square\diamond A$, and therefore $\models_{w}\diamond A\to\square\diamond A$. ∎
Now, a relation is both reflexive and Euclidean iff it is an equivalence relation:
Proof.
Suppose $R$ is both reflexive and Euclidean. If $aRb$, since $aRa$, $bRa$ so $R$ is symmetric. If $aRb$ and $bRc$, then $bRa$ since $R$ has just been proven symmetric, and therefore $aRc$, or $R$ is transitive. Conversely, suppose $R$ is an equivalence relation. If $aRb$ and $aRc$, then $bRa$ since $R$ is symmetric, so that $bRc$ since $R$ is transitive. Hence $R$ is Euclidean. ∎
This also shows that
S5 $=$ KTB4,
where B is the schema $A\to\square\diamond A$, valid in any symmetric frame (see here), and 4 is the schema $\square A\to\square\square A$, valid in any transitive frame (see here). It is also not hard to show that
S5 $=$ KDB4 $=$ KDB5,
where $D$ is the schema $\square A\to\diamond A$, valid in any serial frame (see here).
As a result,
Proposition 2.
S5 is sound in the class of equivalence frames.
Proof.
Since any theorem $A$ in S5 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 5, which are valid in Euclidean frames by the proposition above, and applications of modus ponens and necessitation, both of which preserve validity in any frame, $A$ is valid in any frame which is both reflexive and Euclidean, and hence an equivalence frame. ∎
In addition, using the canonical model of S5, which is based on an equivalence frame, we have
Proposition 3.
S5 is complete in the class of equivalence frames.
Proof.
By the discussion above, it is enough to show that the canonical frame of S5 is reflexive, symmetric, and transitive. Since S5 contains T, B, and 4, $\mathcal{F}_{{\textbf{S5}}}$ is reflexive, symmetric, and transitive respectively, the proofs of which can be found in the corresponding entries on T, B, and S4. ∎
Remark. Alternatively, one can also show that the canonical frame of the consistent normal logic containing 5 must be Euclidean.
Proof.
Let $\Lambda$ be such a logic. Suppose $uR_{{\Lambda}}v$ and $uR_{{\Lambda}}w$. We want to show that $vR_{{\Lambda}}w$, or $\Delta_{v}:=\{B\mid\square B\in v\}\subseteq w$. Let $A$ be any wff. If $A\notin w$, $A\notin\Delta_{u}$ since $uR_{{\Lambda}}v$, so $\square A\notin u$ by the definition of $\Delta_{u}$, or $\neg\square A\in u$ since $u$ is maximal, or $\diamond\neg A\in u$ by substitution theorem on $\neg\square A\leftrightarrow\diamond\neg A$, or $\square\diamond\neg A\in u$ by modus ponens on 5 and the fact that $u$ is closed under modus ponens. This means that $\diamond\neg A\in\Delta_{u}$ by the definition of $\Delta_{u}$, or $\diamond\neg A\in v$ since $uR_{{\Lambda}}v$, so that $\neg\square A\in v$ by the substitution theorem on $\diamond\neg A\leftrightarrow\neg\square A$, which means $\square A\notin v$ since $v$ is maximal, or $A\notin\Delta_{v}$ by the definition of $\Delta_{v}$. ∎
Mathematics Subject Classification
03B45 no label found03B42 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