Bound variables and two variables in a proposition

Question

I'm trying to derive the following as a theorem in a FOL Hilbert system:

$$∀x∃yQ(xy) → ∃yQ(yy) $$

But I'm a bit confused as to how one should interpret the incidence of two variables in $Q$. Is there variable collision or are the two statements separated by the logical implication not related in that sense? Is this an instantiation?

Answer 1

Beside the points stated in the comments, if you are not somehow familiar with the formula, you ought to check its validity, whether there is any counter-instance to it, preferably, by a semantic tableaux method.

A counter-instance has to make $\forall x\exists yQxy$ true and $\exists yQyy$ false. Eventually, you will see that in a domain with one element $\{a\}$ the formula does not have a counter-instance, but in domains with two $\{a, b\}$ (or more) elements, it does (the tableau will not close): There exists an assignment of truth values which verifies $Qab$ and $Qba$, but falsifies $Qaa$ and $Qbb$. Hence, it is not a valid formula.

Answer 2

Just posted by a different user: Naming random variables.

The point is that while it is technically correct to recycle a variable among different scopes (in the given sentence, each quantifier's scope does not extend across the material conditional "$→$"), many dislike this practice for poor communication and being misleading.

Christian's answer here is careful about not recycling variable names, whereas mine isn't so much.