filtration


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

V′⁢(p):={[w]∈W′∣w∈V⁢(p)}.

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

  • •

    w⁢R⁢u implies [w]⁢R′⁢[u]

  • •

    [w]⁢R′⁢[u] implies that for any wff A with □⁢A∈Δ, if ⊧w□⁢A, 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  𝑖𝑓𝑓  M⊧wA.
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
\@unrecurse