Proof that standard translation of modal formula is equivalent to the FO formula

Question

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?

Answer 1

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)]$.