Consider $\forall x \forall y P(y,y)$, where $x$ is quantified, but does not appear.
Is quantifying a variable that otherwise does not appear well-formed or meaningful? I've seen this sort of thing only once before, in a constructive proof that $\forall x A(x) \supset \exists x A(x) $, where what's proved instead is $\forall y (\forall x A(x) \supset \exists(x)A(x))$. I believe this is meant to guard against the possibility of an empty type, where "$\forall x A(x) \supset \exists(x)A(x) $" on its own would be false. But is this meaningful in a classical sense, where we assume the domain is non-empty?
And if $\forall x \forall y P(y,y)$ $is$ meaningful, how does it differ from $\forall y \forall x P(y,y)$?
What about $\exists x \exists y P(x,x)$ and $\exists y \exists x P(x,x)$?