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.

New contributor
Avijeet Ghosh is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
  • $\begingroup$ Welcome to MSE. It is in your best interest that you type your posts (using MathJax) instead of posting links to pictures. $\endgroup$ Jun 23 at 8:53
  • $\begingroup$ @JoséCarlosSantos Thank you. I have restated it. $\endgroup$ Jun 23 at 9:15


Your Answer

Avijeet Ghosh is a new contributor. Be nice, and check out our Code of Conduct.

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.