Let M=(W,R,V) be a Kripke model for a modal logic L. Let Δ be a set of wff’s. Define a binary relationMathworldPlanetmath Δ on W:

wΔu  iff  wA iff uA for any AΔ.

Then Δ is an equivalence relationMathworldPlanetmath on W. Let W be the set of equivalence classesMathworldPlanetmath of Δ on W. It is easy to see that if Δ is finite, so is W. Next, let


Then V is a well-defined function. We call a binary relation R on W a filtrationPlanetmathPlanetmath of R if

  • wRu implies [w]R[u]

  • [w]R[u] implies that for any wff A with AΔ, if wA, then uA.

The triple M:=(W,R,V) is called a filtration of the model M.

Proposition 1.

(Filtration Lemma) Let Δ be a set of wff’s closed underPlanetmathPlanetmath the formation of subformulas: any subformula of any formulaMathworldPlanetmathPlanetmath in Δ is again in Δ. Then

M[w]A  𝑖𝑓𝑓  MwA.
Title filtration
Canonical name Filtration1
Date of creation 2013-03-22 19:35:39
Last modified on 2013-03-22 19:35:39
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 8
Author CWoo (3771)
Entry type Definition
Classification msc 03B45