Kripke semantics for intuitionistic propositional logic

A Kripe model for intuitionistic propositional logicPlanetmathPlanetmath PLi is a triple M:=(W,,V), where

  1. 1.

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

  2. 2.

    is a preorderMathworldPlanetmath on W,

  3. 3.

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

    • if p is a propositional variable, V(p) is upper closed,

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

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

    • V(¬A)=V(A)#,

    • V(AB)=(V(A)-V(B))#,

    where S#:=(S)c, the complementPlanetmathPlanetmath of the lower closure of any SW.


  • If were used as a primitive symbol instead of ¬, then we require that V()=. Then introducing ¬ by ¬A:=A, we get V(¬A)=V(A)#.

  • Some simple properties of #: for any subset S of W, S# is upper closed. This means that for any wff A, V(A) is upper closed. Also, S and S# are disjoint, which means that V(A¬A)= for any A.

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

  • for any propositional variable p, if wp and wu, then up,

  • wAB iff wA and wB,

  • wAB iff wA or wB,

  • w¬A iff for all u such that wu, we have ⊧̸uA

  • wAB iff for all u such that wu, we have uA implies uB.

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

Remark. Since V(A) is upper closed, wA implies uA for any u such that wu. Now suppose wu and uw, then wA iff uA. This shows that, as far as validity of formulasMathworldPlanetmathPlanetmath is concerned, we can take to be a partial orderMathworldPlanetmath in the definition above.

Some examples of Kripke models:

  1. 1.

    Let M1 be the model consisting of W={w,u}, ={(w,w),(u,u),(w,u)}, with V(p)={u} and V(q)=W. Then V(p)#=V(q)#=, and we have the following:

    • V(p¬p)={u}.

    • V(qp)=V(p), and V(¬p¬q)=W, so

    • V(pq)=V(¬q¬p)=W, so

    • V((pq)(qp))=W.

    • In fact, for any wff’s A,B, either V(A)V(B) or V(B)V(A), since is linearly orderedPlanetmathPlanetmath, so that


      assuming V(A)V(B).

  2. 2.

    Let M2 be the model consisting of W={w,u,v}, ={(w,w),(u,u),(v,v),(w,u),(w,v)}, with V(p)={u} and V(q)={v}. Then

    • V(¬p)=V(p)#={v},

    • V(¬¬p)=V(¬p)#={u},

    • so V(¬p¬¬p)={u,v}.

    • V(pq)=V(p)#={v},

    • V(qp)=V(q)#={u},

    • so V((pq)(qp))={u,v}.

  3. 3.

    Let M be an arbitrary model. Then

    • V(ABA)=(V(AB)-V(A))#=W,

    • V(AAB)=(V(A)-V(AB))#=W,

    • V(A(BA))=(V(A)-V(BA))#=(V(A)-(V(B)-V(A))#)#=W. The last equation comes from the fact that for any upper set S, SSc#.

    • Suppose V(A)=V(AB)=W. Then =(V(A)-V(B))=(V(B)c). Since V(B) is upper, V(B)c is lower, so =(V(B)c)=V(B)c, or W=V(B). This shows that modus ponensMathworldPlanetmath preserves validity.

  4. 4.

    Let W be any set and =W2. Then for any wff A, either V(A)=W or V(A)=. Therefore, V(¬¬A)=V(A), and V(¬¬AA)=W.

The pair :=(W,) in a Kripke model M:=(W,,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 various levels can be found in the parent entry. Furthermore, A is valid (with respect to Krikpe semantics) for PLi if it is valid in the class of all frames.

Based on the examples above, we see that

  1. 1.

    (¬q¬p)(pq) is valid in M1, while (¬p¬q)(qp) is not.

  2. 2.

    (pq)(qp) is valid in the class of linearly ordered frames, while it is not valid in M2, and neither is ¬p¬¬p.

  3. 3.

    It is not hard to see that ¬A¬¬A is valid in any weakly connectedPlanetmathPlanetmath frame, that is, for any wW, the set {uwu} is linear.

  4. 4.

    Any wff in any of the schemas ABA, AAB, or A(BA) is valid in PLi. See remark below for more detail.

  5. 5.

    Any theoremMathworldPlanetmath in the classical propositional logic is valid in any universalPlanetmathPlanetmath frame, that is, a frame with a universal relation.

Remark. It can be shown that every theorem of PLi is valid. This is the soundness theorem of PLi. Conversely, every valid wff is a theorem. This is known as the completeness theorem of PLi. Furthermore, a wff valid in the class of finite frames is a theorem. This is the finite model property of PLi.

Title Kripke semantics for intuitionistic propositional logic
Canonical name KripkeSemanticsForIntuitionisticPropositionalLogic
Date of creation 2013-03-22 19:33:19
Last modified on 2013-03-22 19:33:19
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 35
Author CWoo (3771)
Entry type Definition
Classification msc 03B55
Classification msc 03B20
Related topic AxiomSystemForIntuitionisticLogic