Filtration

Idea

Filtration is a construction for extracting finite countermodels from potentially infinite ones. Given a countermodel of a formula (or rule), filtration generates a finite countermodel whose size is determined by the number of subformulas of the formula being refuted, which is always finite.

Definition

These definitions are dual to one another.

On modal algebras

Let $\mathfrak{M},\mathfrak{N}$ be modal algebras, $V,U$ valuations on $\mathfrak{M},\mathfrak{N}$ respectively and $\Theta$ a set of formulae closed under subformulae. The pair $(\mathfrak{N},U)$ is called a filtration of $(\mathfrak{M},U)$ through $\Theta$ when the following conditions hold:

1. There is a Boolean embedding $h:\mathfrak{N}\to \mathfrak{M}$ whose range is precisely the Boolean subalgebra of $\mathfrak{M}$ generated by $\{V(\phi ):\phi \in \Theta \}$;
2. $V(\phi )=U(\phi )$ whenever $\phi \in \Theta$
3. The embedding $h$ satisfies:
   1. $h(\square a)\le \square h(a)$ for every $a\in N$;
   2. $h(\square a)=\square h(a)$ whenever $a=V(\phi )$ and $\square \phi \in \Theta$

On modal spaces and Kripke frames

Let $\mathfrak{X},\mathfrak{Y}$ be modal spaces or Kripke frames, $V,U$ valuations on $\mathfrak{X},\mathfrak{Y}$ respectively and $\Theta$ a set of formulae closed under subformulae. We say that $(\text{spa}Y,U)$ is a filtration of $(\text{spa}M,U)$ through $\Theta$ when the following conditions hold:

1. $\text{spa}Y$ is (isomorphic to) the quotient of $\text{spa}X$ generated by the equivalence relation $x\sim y$ iff $x$ and $y$ satisfy the same formulae from $\Theta$ in the model $(\text{spa}X,V)$.
2. For all $x,y\in X$ we have
   1. If $Rxy$, then $R[x][y]$, where $[x]$ is the equivalence class of $x$ under $\sim$;
   2. If $R[x][y]$, then for any $\square \phi \in \Theta$, if $\text{spa}Y,V,y/\models \phi$, then $\text{spa}X,V,x/\models \square \phi$.