set of formulas from ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ that use at most three different first-order variables (however, a variable can be quantified and reused several times in a formula). The main result of this section is that, for formulas with zero or one free variable, the logics ${\textup{FO}}[{\rightarrow},{\lhd},\le]$, ${\textup{FO}}^3[{\rightarrow},{\lhd},\le]$, ${{{\textup{PDL}_{\mathsf{sf}}}}}$, and ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ are expressively equivalent.

Consider ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formulas $\Phi_0$, $\Phi_1(x)$ and $\Phi_2(x,y)$ with respectively zero, one, and two free variables (hence, $\Phi_0$ is a sentence). Consider also some ${{{\textup{PDL}_{\mathsf{sf}}}}}$ sentence ${\xi}$, event formula $\varphi$, and path formula $\pi$. The respective formulas are equivalent, written $\Phi_0\equiv{\xi}$, $\Phi_1(x)\equiv\varphi$, and $\Phi_2(x,y)\equiv\pi$, if, for all MSCs $M$ and all events $e,f$ in $M$, we have $$\begin{aligned}
  M &\models \Phi_0 && \text{iff} & M &\models {\xi}\\
  M,[x\mapsto e] &\models \Phi_1(x) && \text{iff} & M,e &\models \varphi \\
  M,[x \mapsto e, y \mapsto f] &\models \Phi_2(x,y) && \text{iff} & M,e,f &\models \pi\end{aligned}$$

We start with a simple observation, which can be shown easily by induction:

\[prop:pdl-fo3\] Every ${{{\textup{PDL}_{\mathsf{sf}}}}}$ formula is equivalent to some ${\textup{FO}}^3[{\rightarrow},{\lhd},\le]$ formula. More precisely, for every ${{{\textup{PDL}_{\mathsf{sf}}}}}$ sentence ${\xi}$, event formula $\varphi$, and path formula $\pi$, there exist some ${\textup{FO}}^3[{\rightarrow},{\lhd},\le]$ sentence $\widetilde{{\xi}}$, formula ${\widetilde{\varphi}}(x)$ with one free variable, and formula ${\widetilde{\pi}}(x,y)$ with two free variables, respectively, 