Why not ban nested quantifiers over the same variable? People seem to think (1, 2, 3) that a wff can have nested quantifiers over the same variable, e.g., $\forall x(Px \wedge \exists x Qx)$.
However, consider the following argument:


*

*$\forall x \exists y Pxy$ (Premise)

*$\exists y P\hat{x}y$ (1, $\forall$E)

*$\forall y \exists y Pyy$ (2, $\forall$I)


This is clearly not valid, but what is wrong with it?  According to wikipedia, the application of $\forall$I is wrong because $y$ occurs in 2.
Here is another invalid argument:


*

*$\forall x Pxc$ (Premise)

*$\exists x \forall x Pxx$ (1, $\exists$I)


This is considered invalid for a similar reason: the application of $\exists$I is wrong because $x$ occurs in 1.
But we wouldn't need these restrictions if we just banned nested quantifiers over the same variable.  This seems like a simpler rule and we're not losing any expressive power.  Does anyone set up predicate logic this way?

Nesting of quantifiers is not exactly the issue with the elimination-introduction confusion.
Attempt the argument actually using the supposed problem child: $\forall x\,(Px \wedge \exists x\,Qx)$


*

*$\forall y\,(Py \wedge \exists x\,Qx)$ as premised.

*$Pa \wedge \exists x\,Qx$ via $\forall$ elimination to arbitrary $a$.

*$\forall x\,(Px \wedge \exists x\,Qx)$ via $\forall$ introduction from arbitrary $a$.
This is no problem.   When introducing an universal quatifier, you may safely alpha-replace the arbitrary witness, $a$, with any variable which does not occur free inside any shared scope.   Here, $x$ does not occur free, as it is bound by the existential. 
Your original argument did have $x$ occuring inside a shared scope.   It was this that caused the issue, not the nesting of quantifiers.
