Proof that standard translation of modal formula is equivalent to the FO formula For example $\varphi:=\lozenge\lozenge p\rightarrow\lozenge p$ defines transitivity and it has a standard translation $St_{x}(\varphi):=\forall P\forall x(\exists y(R(x,y)\wedge \exists x(R(y,x)\wedge P(x)))\rightarrow\exists y(R(x,y)\wedge P(y)))$. The first order formula that corresponds to $St_{x}(\varphi)$ is of course $\psi(x):=\forall x\forall y \forall z(R(x,y)\wedge R(y,z)\rightarrow (R(x,z))$. Now, how do I prove that $St_{x}(\varphi)\Leftrightarrow\psi(x)$ without using van Benthem's characterization theorem?

_Hint_

There is an algorithm described into:

* Patrick Blackburn & Maarten de Rijke & Yde Venema, Modal Logic (2001), **Ch3.6 Sahlqvist Formulas** ; see Example 3.43, page 159.



The formula:

> $St_x(\varphi) := ∀P∀x \ [∃y(R(x,y) ∧ ∃z(R(y,z) ∧ P(z))) → ∃w(R(x,w) ∧ P(w))]$

must be converted by the algorithm, with the instantiation $\sigma(P) := \lambda u . (u=z)$, into:

> $∀x ∀y ∀z \ [(R(x,y) ∧ R(y,z) ∧ z=z) → ∃w(R(x,w) ∧ w=z)]$

which is equivalent to:

> $∀x ∀y ∀z \ [(R(x,y) ∧ R(y,z)) → R(x,z)]$.