Prove the following argument $\forall x \exists y (Px → Rxy) ⊢ \forall y (Py → \exists x Ryx)$ using the rules of sequent calculus 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.
 A: 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}
