modal logic S5 (original) (raw)

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

• •
  (T) □⁢A→A, and
• •
  (5) ⋄A→□⋄A.

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

Proposition 1.

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

Proof.

First, let ℱ be a frame validating 5. Suppose w⁢R⁢x and w⁢R⁢y. Let M be a model based on ℱ, with V⁢(p)={x}. Since ⊧xp, we have ⊧w⋄p, and so ⊧w□⋄p, or ⊧u⋄p for all u such that w⁢R⁢u. In particular, ⊧y⋄p. So there is a z such that y⁢R⁢z and ⊧zp. But this means z=x, whence y⁢R⁢x, meaning R is Euclidean.

Conversely, suppose ℱ is a Euclidean frame, and M a model based on ℱ. Suppose ⊧w⋄A. Then there is a v such that w⁢R⁢v and ⊧vA. Now, for any u with w⁢R⁢u, we have u⁢R⁢v since R is Euclidean. So ⊧u⋄A. Since u is arbitrary, ⊧w□⋄A, and therefore ⊧w⋄A→□⋄A. ∎

This also shows that

S5 = KTB4,

where B is the schema A→□⋄A, valid in any symmetric frame (see here (http://planetmath.org/ModalLogicB)), and 4 is the schema □⁢A→□⁢□⁢A, 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 □⁢A→⋄A, 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.

In addition, using the canonical model of S5, which is based on an equivalence frame, we have

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 u⁢RΛ⁢v and u⁢RΛ⁢w. We want to show that v⁢RΛ⁢w, or Δv:={B∣□⁢B∈v}⊆w. Let A be any wff. If A∉w, A∉Δu since u⁢RΛ⁢v, so □⁢A∉u by the definition of Δu, or ¬⁢□⁢A∈u since u is maximal, or ⋄¬⁢A∈u by substitution theorem on ¬⁢□⁢A↔⋄¬⁢A, or □⋄¬⁢A∈u 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 ⋄¬⁢A∈v since u⁢RΛ⁢v, so that ¬⁢□⁢A∈v by the substitution theorem on ⋄¬⁢A↔¬⁢□⁢A, which means □⁢A∉v since v is maximal, or A∉Δv by the definition of Δv. ∎