Kripke submodel

Let =(W,R) be a Kripke frame. A subframe of is a pair =(W,R) such that W is a subset of W and R=R(W×W). A submodel of a Kripke model M=(W,R,V) of a modal propositional logicPlanetmathPlanetmath PLM is a triple (W,R,V) where (W,R) is a subframe of (W,R), and V(p)=V(p)W for each propositional variable p in PLM.

The most common submodel of a Kripke model M=(W,R,V) is constructed by taking Ww:={uwR*u}, where R* is the reflexive transitive closure of R, for any wW. The submodel Mw:=(Ww,Rw,Vw) is called the submodel of M generated by the world w, and w the subframe of generated by w. A submodel of M is called a generated submodel if it is generated by some world w in M.

Proposition 1.

For any wff A and any uWw, MuA iff MwuA.


We do inductionMathworldPlanetmath on the number n of connectivesMathworldPlanetmath in A.

If n=0, then A is either or a propositional variable. Clearly, M⊧̸u iff Mw⊧̸u, or Mu iff Mwu. If A is some propositional variable p, then Mup iff uV(p) iff uV(p) iff uV(p) and uWw (by assumptionPlanetmathPlanetmath) iff uV(p)Mw iff uVw(p) iff Mwup.

Next, suppose A is BC. Then MuA iff uV(B)cV(C) iff u(W-V(B))V(C) and uWw (by assumption) iff uWw-V(B) or uVw(C) iff uWw-Vw(B) or uVw(C) iff MwuA.

Finally, suppose A is B. First let MuA. To show MwuA, pick any vWw such that uRwv. Then uRv, so that MvB, or vV(B). Since vWw, vVw(B), or MwvB, and thus MwuA. Conversely, let MwuA. To show MuA, pick any vW such that uRv. Since wR*u, wR*v so that vWw. Furthermore (u,v)R(Ww×Ww)=Rw. So MwuB, or vVw(B)V(B), which means MuA. ∎

Corollary 1.

MA iff MwA for all wW.


If MA, then MuA for all uW, so that MwuA for all uWw and all wW, or MwA for all wW. Conversely, if MwA for all wW, then in particular MwwA (since R* is reflexiveMathworldPlanetmathPlanetmath) for all wW, or MwA for all wW, or MA. ∎

Corollary 2.

A iff FwA for all wW.


If A, then MA for all M based on , or MwA, where Mw is based on w, for all wW by the last corollary. Since any model based on w is of the form Mw, wA. Conversely, suppose wA for all wW. Let M be any model based on . Then Mw is based on w, and therefore MwA. Since w is arbitrary, MA by the last corollary, so A. ∎

Title Kripke submodel
Canonical name KripkeSubmodel
Date of creation 2013-03-22 19:34:50
Last modified on 2013-03-22 19:34:50
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 11
Author CWoo (3771)
Entry type Definition
Classification msc 03B45
Defines generated submodel