Hello I have a slightly unusual question which relates to a definition of filtration structure. The following is my current state of the definition:

$ \mathcal{M} = (W, R, L) $, W is a set of worlds, $R$ is a binary relation on the worlds, $ R \subseteq W \times W$, and $L$ is a labelling function $ L : W \rightarrow\ \mathcal{P} (PropAtoms) $, here $PropAtoms$ is the set of atomic formulas.

Let $ \mathcal{M} = (W, R, L) $ be a Kripke model and let $\Gamma$ be a set of formulas that is closed under subformulas. Now, for each world $ w \in W$ we define the following: $ \Gamma_{w} = \{ \psi \in \Gamma : (\mathcal{M},w) \vDash \psi \}$,

that is, $\Gamma_{w} $ contains formulas from $ \Gamma $ that are true at $w$ and consequently in model $\mathcal{M}$. Next we define an equivalence relation $\sim_{\Gamma} $ on worlds $w, w' \in W$, $ \sim_{\Gamma} w w' $ if and only if $\Gamma_{w} \sqsubset \Gamma_{w'}$, that is, worlds $w$ and $w'$ are equivalent if and only if they satisfy the same formulas in $\Gamma$. We also have equivalence classes $[w]$ of worlds $w$ with respect to $\sim_{\Gamma}$.

Lets now present the following quotient structure $ \mathcal{M}_{\Gamma} = (W_{\Gamma}, R_{\Gamma}, L_{\Gamma})$ which is in fact filtration of $\mathcal{M}$ with respect to $\Gamma$. $\mathcal{M}_{\Gamma}$ is defined as follows: .........

Here is the bit I need help with, I am struggling to define my filtration model. This is mainly because the definitions online don't use the same labelling function but rather use a valuation function which is of the form $v(p)$. And such function takes an atomic formula whearas my labelling function takes in a specific world written $L(x)$. Could someone please help me our here and try providing correct definition which will match my model $M$ definition?


2 Answers 2


You are probably looking for something like: $L_\Gamma([w]) = L(w) \cap \Gamma$. This will falsify any propositional letter not in $\Gamma$.

(Filtration is (afaik) usually defined as a property that a model may have. There could be several (or none) concrete models satisfying this property.)


You got quite close to the final model.

Keeping your $\mathcal{M} = (W, R, L)$, $\Gamma$, $\sim_{\Gamma} $ on worlds $w, w' \in W$, and $[w]$ of worlds $w$ with respect to $\sim_{\Gamma}$. Define further $W_\Gamma = \{ [w] \mid w \in W \}$.

Suppose that $\mathcal{M}^f = (W^f, R^f, L^f)$ is any model satisfying

  • $W^f = W_\Gamma$,
  • If $Rwv$ then $R^f[w][v]$
  • If $R^f[w][v]$ then for all $\Diamond \phi \in \Gamma$, if $\mathcal{M}, v \Vdash \phi$ then $\mathcal{M}, w \Vdash \Diamond \phi$
  • $V^f(p) = \{ [w] \mid\mathcal{M}, v \Vdash p \}$ for all $p$ in PropAtoms.

Then $\mathcal{M}^f$ is called a filtration of $\mathcal{M}$ through $\Gamma$.

Now, for your question on construction. The above restrictions only impose restrictions on $R^f$:


  1. $R^s[w][v]$ if and only if $\exists w' \in [w], \exists v' \in [v] . Rw'v'$
  2. $R^l[w][v]$ if and only if for all formulae $\Diamond \phi$ in $\Gamma$, $\mathcal{M}, v \Vdash \phi$ implies $\mathcal{M}, w \Vdash \phi$

These two give rise to the largest and smallest filtrations, $(W_\Gamma, R^s, L^f)$ and $(W_\Gamma, R^l, L^f)$.

Based on P Blackburn, M De Rijke, and Y Venema. "Modal Logic (Cambridge Tracts in Theoretical Computer Science)." (2002), pp 77-80.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.