Vacuous Quantification In this formula, a vacuous quantification can be removed:
$ \exists x \forall x (P(x) \rightarrow Q(x)) \equiv \forall x (P(x) \rightarrow Q(x)) $
What about a formula like this?:
$ \forall x (P(x) \rightarrow \exists x Q(x)) $
Is this also a vacuous quantification or is it not a well formed formula?
Can it be rewritten in a different form like for the first formula?
 A: The formula $\exists x \forall x (P(x) \to Q(x))$ is logically equivalent to $\forall x (P(x) \to Q(x))$$-$and hence the former can be rewritten to the latter without changing its meaning$-$because $\exists x$ does not bind any occurrence of $x$ in $\forall x (P(x) \to Q(x))$ and so this $\exists x$ is superfluous (technically, it is often said dummy).
On the contrary, in the formula $\forall x (P(x) \to \exists x Q(x))$, the quantifier $\forall x $ is not dummy (or "vacuous" according to your terminology), because it binds the occurrence of $x$ in $P(x)$. Therefore, $\forall x$ cannot be removed. A similar discourse holds for $\exists x$ (with respect to the occurrence of $x$ in $Q(x)$).
But you can rewrite the formula $\forall x (P(x) \to \exists x Q(x))$ as $\forall x (P(x) \to \exists y Q(y))$: they are exactly the same formula, since formulas are identified up to renaming of bound variables. The advantage of the second version of the formula is that you can now move the existential quantifier in front of the implication, without changing the meaning of the formula. Indeed, the formula $\forall x (P(x) \to \exists y Q(y))$ is logically equivalent to
$$\forall x \exists y (P(x) \to  Q(y))$$
The latter is a formula in prenex normal form, which means that all the quantifiers are at the beginning of the formula. A well-known theorem in classical logic says that every formula is logically equivalent to a formula in prenex normal form.
A: Quantification is vacuous when it binds no variables at all, either because there are no occurrences of the binding variable or because it gets entirely overridden by another quantifier. The latter is the case with the first formula, where $\exists x$ is immediately followed by $\forall x$.
In the second formula, hower, $\forall x$ does have an active binding, namely the occurrence of $x$ in $P(x)$. It is only the occurrence in $Q(x)$ that gets overwritten by $\exists x$. $\forall x$ can hence not be removed.
In most definitions of FOL syntax, vacuous quantification, binding overriding and identically named binding across independent subformulas (such as $(\exists x P(x)) \land (\forall x Q(x))$) is permitted.
If you want to make the formula clearer by avoiding identical variable names for different bindings, you can perform bound renaming and e.g. write $\forall x (P(x) \to \exists y P(y))$. This formula will be logically equivalent to the original.
