I was reading this question and I was curious, since I haven't quite grasp this topic being fairly new and all, how much would it differ the "tree" or list of deductions if instead of $\vdash \exists x (Px \rightarrow \forall x Px)$ we had $\vdash \exists x (Px \rightarrow \forall y Py)$. With the same axioms from the aforementioned question:
- Tautologies
- $\forall x \alpha \rightarrow \alpha_t^x$, where $t$ is substitutable for $x$ in $\alpha$.
- $\forall x (\alpha \rightarrow \beta)\rightarrow(\forall x \alpha \rightarrow \forall x \beta)$
And if the language includes equality,
- $x=x$
- $x=y \rightarrow (\alpha \rightarrow \alpha')$ , where $ \alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing $x$ in zero or more places by $y$.
It seems like maybe we could use a substitution but I'm not sure its possible since $x$ occurs freely in $P(x)$. Any light shed on this problem would be highly appreciated, many thanks.