modal logic S4

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

  • (T) AA, and

  • (4) AA.

In this entry (, we show that T is valid in a frame iff the frame is reflexiveMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

Proposition 1.

4 is valid in a frame F iff F is transitiveMathworldPlanetmathPlanetmathPlanetmath.


First, suppose is a frame validating 4, with wRu and uRt. Let M be a model with V(p)={vwRv}, where p a propositional variable. So wp. By assumptionPlanetmathPlanetmath, we have wpp. Then wp. This means vp for all v such that wRv. Since wRu, up, which means sp for all s such that uRs. Since uRt, we have tp, or tV(p), or wRt. Hence R is transitive.

Conversely, let be a transitive frame, M a model based on , and w any world in M. Suppose wA. We want to show wA, or for all u with wRu, we have uA, or for all u with wRu and all t with uRt, we have tA. If wRu and uRt, wRt since R is transitive. Then tA by assumption. Therefore, wAA. ∎

As a result,

Proposition 2.

S4 is sound in the class of preordered frames.


Since any theorem in S4 is deducible from a finite sequencePlanetmathPlanetmath consisting of tautologiesMathworldPlanetmath, which are valid in any frame, instances of T, which are valid in reflexive frames, instances of 4, which are valid in transitive frames by the propositionPlanetmathPlanetmath above, and applications of modus ponensMathworldPlanetmath and necessitation, both of which preserve validity in any frame, whence the result. ∎

In addition, using the canonical model of S4, which is preordered, we have

Proposition 3.

S4 is completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath in the class of serial frames.


Since S4 contains T, its canonical frame 𝐒𝟒 is reflexive. We next show that the canonical frame Λ of any consistentPlanetmathPlanetmath normal logic Λ containing the schema 4 must be transitive. So suppose wRΛu and uRΛv. If AΔw:={BBw}, then Aw, or Aw by modus ponens on 4 and the fact that w is closed under modus ponens. Hence AΔw, or Au since wRΛu, or AΔu, or Av since uRΛv. As a result, wRΛv, and therefore 𝐒𝟒 is a preordered frame. ∎

By a proper translationMathworldPlanetmathPlanetmath, one can map intuitionistic propositional logic PLi into S4, so that a wff of PLi is a theorem iff its translateMathworldPlanetmath is a theorem of S4.

Title modal logic S4
Canonical name ModalLogicS4
Date of creation 2013-03-22 19:34:01
Last modified on 2013-03-22 19:34:01
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 9
Author CWoo (3771)
Entry type Definition
Classification msc 03B42
Classification msc 03B45
Defines S4
Defines 4