modal logic S5


The modal logic S5 is the smallest normal modal logic containing the following schemas:

  • (T) AA, and

  • (5) AA.

S5 is also denoted by KT5, where T and 5 correspond to the schemas T and 5 respectively.

In this entry (http://planetmath.org/ModalLogicT), we show that T is valid in a frame iff the frame is reflexiveMathworldPlanetmathPlanetmath.

A binary relationMathworldPlanetmath 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 first-order definable:

uvw((uRvuRw)vRw).
Proposition 1.

5 is valid in a frame F iff F is Euclidean.

Proof.

First, let be a frame validating 5. Suppose wRx and wRy. Let M be a model based on , with V(p)={x}. Since xp, we have wp, and so wp, or up for all u such that wRu. In particular, yp. So there is a z such that yRz and zp. But this means z=x, whence yRx, meaning R is Euclidean.

Conversely, suppose is a Euclidean frame, and M a model based on . Suppose wA. Then there is a v such that wRv and vA. Now, for any u with wRu, we have uRv since R is Euclidean. So uA. Since u is arbitrary, wA, and therefore wAA. ∎

Now, a relation is both reflexive and Euclidean iff it is an equivalence relationMathworldPlanetmath:

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 transitiveMathworldPlanetmathPlanetmathPlanetmath. 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 AA, valid in any symmetric frame (see here (http://planetmath.org/ModalLogicB)), and 4 is the schema AA, valid in any transitive frame (see here (http://planetmath.org/ModalLogicS4)). It is also not hard to show that

S5 = KDB4 = KDB5,

where D is the schema AA, valid in any serial frame (see here (http://planetmath.org/ModalLogicD)).

As a result,

Proposition 2.

S5 is sound in the class of equivalence frames.

Proof.

Since any theoremMathworldPlanetmath A in S5 is deducibleMathworldPlanetmath from a finite sequencePlanetmathPlanetmath consisting of tautologiesMathworldPlanetmath, 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 propositionPlanetmathPlanetmath above, and applications of modus ponensMathworldPlanetmath 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 additionPlanetmathPlanetmath, using the canonical model of S5, which is based on an equivalence frame, we have

Proposition 3.

S5 is completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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, 𝐒𝟓 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 Λ be such a logic. Suppose uRΛv and uRΛw. We want to show that vRΛw, or Δv:={BBv}w. Let A be any wff. If Aw, AΔu since uRΛv, so Au by the definition of Δu, or ¬Au since u is maximal, or ¬Au by substitution theorem on ¬A¬A, or ¬Au by modus ponens on 5 and the fact that u is closed under modus ponens. This means that ¬AΔu by the definition of Δu, or ¬Av since uRΛv, so that ¬Av by the substitution theorem on ¬A¬A, which means Av since v is maximal, or AΔv by the definition of Δv. ∎

Title modal logic S5
Canonical name ModalLogicS5
Date of creation 2013-03-22 19:34:04
Last modified on 2013-03-22 19:34:04
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 11
Author CWoo (3771)
Entry type Definition
Classification msc 03B45
Classification msc 03B42
Defines S5
Defines 5
Defines Euclidean