# Reflexive transitive closure in Propositional Dynamic Logic

Would anyone care to explain how can we dualize the Reflexive Transitive Closure in PDL from : $$\frac{(\phi\vee\langle\alpha\rangle\psi)\rightarrow\psi}{\langle\alpha^*\rangle\phi\rightarrow\psi}$$ to: $$\frac{\psi\rightarrow (\phi\vee [\alpha]\psi)}{\psi\rightarrow [\alpha^*]\phi}$$?

Where $\alpha$ is a program, $\phi,\psi$ are formulas and $\langle\alpha\rangle$ is the diamond from PDL.

• Are you sure it's not $(\phi \wedge [\alpha]\psi)$? – Fabio Somenzi Jan 18 '17 at 23:32

$\def\<#1>{\langle#1\rangle}$We start from the relation between box and diamond:

$$\<\alpha>p \equiv \neg [\alpha] \neg p \enspace.$$

Substitution in the reflexive transitive closure rule yields

$$\frac{(\phi \vee \neg[\alpha]\neg \psi) \rightarrow \psi}{\neg[\alpha^*]\neg\phi \rightarrow \psi} \enspace.$$

Taking the contrapositive of both premise and conclusion,

$$\frac{\neg \psi \rightarrow (\neg\phi \wedge [\alpha]\neg \psi)}{\neg\psi \rightarrow [\alpha^*]\neg\phi} \enspace.$$

We now rename, so that $\neg\phi$ is replaced by $\phi$ and $\neg\psi$ is replaced by $\psi$:

$$\frac{\psi \rightarrow (\phi \wedge [\alpha]\psi)}{\psi \rightarrow [\alpha^*]\phi} \enspace.$$

Finally, if we wish to obtain the loop invariance rule, we substitute $\psi$ for $\phi$ and simplify:

$$\frac{\psi \rightarrow [\alpha]\psi}{\psi \rightarrow [\alpha^*]\psi} \enspace,$$

having noted that $\psi \rightarrow (\psi \wedge [\alpha]\psi) \equiv \psi \rightarrow [\alpha]\psi$.