When doing a derivation in predicate logic, am I allowed to use two different existential variables interchangeably?
For instance, is $\forall xPx$ (or $∃xPx$) equal to $\forall yPy(∃yPy)$? If I cannot directly mix the two, am I allowed to do a Existential Instantiation on the $\forall xPx$, make it into a $Pa$, and use Existential Generalization to change it to $\forall yPy$?
If this is not allowed, can someone explain why?
$\forall x \,Px\;$ means the same thing as $\,\forall y \,Py,\,$ just as $\,\exists x\, Px \,$ means the same thing as $\,\exists y \,Py$.
Variables are variables; there's no significance which variable you choose to quantify, but once chosen, you need to be consistent in it's use. E.g., $\forall x\, Py$ means very little, since $y$ is nothing more than a free variable that has nothing to do with the quantified $x$.
You can use Universal Instantiation on $\forall x\,Px$ to instantiate $Pa$, and then use Universal Generalization to later change that to $\forall y\, Py$.
You cannot, however, universally generalize from a constant that has not been universally instantiated.