Requirement of the Second part of PDL Filtration Lemma

27 Views Asked by At

I was reading this filtration lemma of PDL in David Harel's book Dynamic Logic.

The Filtration Lemma: Let $\kappa = \langle W, \mathcal{R}, V\rangle$ be a Kripke model of PDL and let $u, v\in W$:

(i) For all $\psi\in FL(\varphi)$, $u\in V(\psi)$ iff $[u]\in V_{\sim_{FL(\varphi)}}(\psi)$.

(ii) For all $[\alpha]\psi\in FL(\varphi)$,

(a) if $(u,v)\in \mathcal{R}(\alpha)$ then $([u],[v])\in\mathcal{R}_{\sim_{FL(\varphi)}}(\alpha)$;

(b) if $([u], [v])\in\mathcal{R}_{\sim_{FL(\varphi)}}(\alpha)$ and $u\in V([\alpha]\psi)$, then $v\in V(\psi)$.

Here $FL(\varphi)$ is the Fischer-Ladner closure of $\varphi$. $\kappa_{\sim_{FL(\varphi)}} = \langle W_{\sim_{FL(\varphi)}}, \mathcal{R}_{\sim_{FL(\varphi)}}, V_{\sim_{FL(\varphi)}}\rangle$ is the quotient model created wrt $FL(\varphi)$ in a similar way quotient model were created in filtration of modal logic wrt $SF(\varphi)$. My question is:

What is the requirement of the second part of the lemma (point (ii)) in order to prove decidability? In usual modal logic, the first statement suffices since it shows the new quotient model built is preserving the truth with respect to the closure.