Prove the following argument $\forall x \exists y (Px \to Rxy) \vdash \forall y (Py \to \exists x Ryx)$ using the rules of sequent calculus.
I've been struggling how to prove this argument.
I've tried to use different paths using the Left and Right rules for the $\forall $ and the $\exists$, but everything I've tried so far hasn't worked.
Can someone help solve this, find a good way to use the rules in order to reach the goal?
This what I had so far:
$1. -\forall x \exists y (Px → Rxy) ⊢ \forall y (Py → \exists x Ryx)$
$2. -\forall x \exists y (Px → Rxy) ⊢ Py → \exists x Ryx$
$3. -Py, \forall x \exists y (Px → Rxy) ⊢ \exists x Ryx$
$4. -Py, \forall x \exists y (Px → Rxy) ⊢ Ryt$
Thank you in advance.
I tried also by starting by the left side, and didn't reach to the goal.
The subtlety here is to use the rule $\exists_L$ (which has some constraints about free variables) at the right moment. You get stuck because in your step $4$, you use the rule $\exists_R$, but you should apply this rule after the rule $\exists_L$ (reading the derivation bottom up), otherwise the constraints about free variables demanded $\exists_L$ would never be fulfilled.
A correct derivation of $\forall x \exists z (Px \to Rxz) \vdash \forall y (Py \to \exists x Ryx)$ in the sequent calculus is below. Note that the sequent $\forall x \exists z (Px \to Rxz) \vdash \forall y (Py \to \exists x Ryx)$ is the same as $\forall x \exists y (Px \to Rxy) \vdash \forall y (Py \to \exists x Ryx)$ (I used the former to avoid any ambiguity between the different occurrences of $y$ on the LHS and on the RHS of the sequent).
\begin{align} \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{\dfrac{}{Px \vdash Px}\text{ax} \qquad \dfrac{}{Ryz \vdash Ryz}\text{ax}}{Px \to Ryz, Py \vdash Ryz}\to_L } {Px \to Ryz, Py \vdash \exists x Ryx}\exists_R } {\exists z (Px \to Ryz), Py \vdash \exists x Ryx}\exists_L} {\forall x \exists z (Px \to Rxz), Py \vdash \exists x Ryx} \forall_L } {\forall x \exists z (Px \to Rxz) \vdash Py \to \exists x Ryx} \to_R } {\forall x \exists z (Px \to Rxz) \vdash \forall y (Py \to \exists x Ryx)} \forall_R \end{align}