filtration (original) (raw)

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

Then ∼Δ is an equivalence relation on W. Let W′ be the set of equivalence classes 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 filtration 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.