Kripke semantics for modal propositional logic

A Kripe model for a modal propositional logicPlanetmathPlanetmath PLM is a triple M:=(W,R,V), where

  1. 1.

    W is a set, whose elements are called possible worlds,

  2. 2.

    R is a binary relationMathworldPlanetmath on W,

  3. 3.

    V is a function that takes each wff (well-formed formula) A in PLM to a subset V(A) of W, such that

    • V()=,

    • V(AB)=V(A)cV(B),

    • V(A)=V(A), where S:={ssS}, and s:={tsRt}.

For derived connectivesMathworldPlanetmath, we also have V(AB)=V(A)V(B), V(AB)=V(A)V(B), V(¬A)=V(A)c, the complementPlanetmathPlanetmath of V(A), and V(A)=V(A):=V(A)cc.

One can also define a satisfaction relation between W and the set L of wff’s so that

wA  iff  wV(A)

for any wW and AL. It’s easy to see that

  • ⊧̸w for any wW,

  • wAB iff wA implies wB,

  • wAB iff wA and wB,

  • wAB iff wA or wB,

  • w¬A iff ⊧̸wA,

  • wA iff for all u such that wRu, we have uA,

  • wA iff there is a u such that wRu and uA.

When wA, we say that A is true at world w.

The pair :=(W,R) in a Kripke model M:=(W,R,V) is also called a (Kripke) frame, and M is said to be a model based on the frame . The validity of a wff A at different levels (in a model, a frame, a collectionMathworldPlanetmath of frames) is defined in the parent entry (

For example, any tautologyMathworldPlanetmath is valid in any model.

Now, to prove that any tautology is valid, by the completeness of PLc, every tautology is a theorem, which is in turn the result of a deductionMathworldPlanetmathPlanetmath from axioms using modus ponensMathworldPlanetmath.

First, modus ponens preserves validity: for suppose wA and wAB. Since wA implies wB, and wA by assumption, we have wB. Now, w is arbitrary, the result follows.

Next, we show that each axiom of PLc is valid:

  • A(BA): If wA and wB, then wA, so wBA.

  • (A(BC))((AB)(AC)): Suppose wA(BC), wAB, and wA. Then wBC and wB, and therefore wC.

  • (¬A¬B)(BA): we use a different approach to show this:

    V((¬A¬B)(BA)) = V(¬A¬B)cV(BA)
    = (V(¬A)V(¬B)c)V(B)cV(A)
    = (V(A)cV(B))V(B)cV(A)
    = (V(A)cV(B)c)V(A)=W.

In addition, the rule of necessitationPlanetmathPlanetmath preserves validity as well: suppose wA for all w, then certainly uA for all u such that wRu, and therefore wA.

There are also valid formulasMathworldPlanetmathPlanetmath that are not tautologies. Here’s one:


Let w be any world in M. Suppose w(AB). Then for all u such that wRu, uAB, or uA implies uB, or for all u such that wRu, uA, implies that for all u such that wRu, uB, or wA implies wB, or w(AB). Therefore, w(AB)(AB). ∎

From this, we see that Kripke semantics is appropriate only for normal modal logics.

Below are some examples of Kripke frames and their corresponding validating logics:

  1. 1.

    AA is valid in a frame (W,R) iff R weak identityPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath: wRu implies w=u.


    Let (W,R) be a frame validating AA, and M a model based on (W,R), with V(p)={w}. Then wp. So wp, or up for all u such that wRu. But then uV(p), or u=w. Hence R is the relationMathworldPlanetmath: if wRu, then w=u.

    Conversely, suppose (W,R) is weak identity, M based on (W,R), and w a world in M with wA. If wRu, then u=w, which means uA for all u such that wRu. In other words, wA, and therefore, wAA. ∎

  2. 2.

    A is valid in a frame (W,R) iff R=.


    First, suppose A is valid in (W,R), and M a model based on (W,R), with V(p)=. Since wp, up for any u such that wRu. Since no such u exists, and w is arbitrary, R=.

    Conversely, given a model M based on (W,), and a world w in M, it is vacuously true that uA for any u such that wRu, since no such u exists. Therefore wA. ∎

A logic is said to be sound if every theorem is valid, and completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath if every valid wff is a theorem. Furthermore, a logic is said to have the finite model property if any wff in the class of finite frames is a theorem.

Title Kripke semantics for modal propositional logic
Canonical name KripkeSemanticsForModalPropositionalLogic
Date of creation 2013-03-22 19:33:22
Last modified on 2013-03-22 19:33:22
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 30
Author CWoo (3771)
Entry type Definition
Classification msc 03B45
Related topic ModalLogic