Is $\forall x(P(x) \vee Q(y))$ the same as $(\forall x P(x)) \vee Q(y)$?
I understand that if I had $\forall x(P(x) \vee Q(x))$, that it is not the same as $(\forall x P(x)) \vee (\forall x Q(x))$. However the presence of a second variable is really throwing me off, and I don't understand how to think up an example to see if they are equivalent.
For a formal proof start with $$\forall x, (P(x) \lor Q(y)) \vdash (\forall x, P(x)) \lor Q(y)$$ and apply the law of excluded middle on $Q(y)$ to split that into two statements $$Q(y), [\forall x, (P(x) \lor Q(y))] \vdash (\forall x, P(x)) \lor Q(y)$$ and $$\lnot Q(y), [\forall x, (P(x) \lor Q(y))] \vdash (\forall x, P(x)) \lor Q(y),$$ the first is immediate: just introduce $x$ and take the right disjunction and you prove $Q(y)$, for the second, introduce x and eliminate the possibility of $Q(y)$ using the hypothesis to get $P(x)$ which you then generalize to get $\forall x, P(x)$. This proves $(\forall x, P(x)) \lor Q(y)$ from $\forall x, (P(x) \lor Q(y))$. Proving the converse implication is much easier.
It might be interesting to note (and part of the reason it's difficult to see why this is true) that this is not intuitionistically provable. In constructive logic it matters which of the disjunctions $\forall x, (P(x) \lor Q(y))$ are taken depending on $x$, the second formula $(\forall x, P(x)) \vee Q(y)$ does not allow such dependencies, so it's actually a much stricter formula.