Natural deduction proof of $\forall x (\exists y (P(x) \vee Q(y))) \vdash \exists y (\forall x (P(x) \vee Q(y)))$ I'm trying to do a Fitch proof of
$$
\forall x (\exists y (P(x) \vee Q(y))) \vdash \exists y (\forall x (P(x) \vee Q(y)))
$$
Edit: using only the axioms on http://www.proofwiki.org/wiki/Category:Natural_Deduction_Axioms, along with universal/existential generalisation/instantiation
The following is my first attempt.
$$
\begin{array}{lll}
1 & \begin{array}{l}\forall x (\exists y (P(x) \vee Q(y))) \\ \hline \end{array} & \text{assumption} \\
2 & \exists y (P(v) \vee Q(y)) & \text{$\forall$E, 1} \\
3 & \begin{array}{ll} & \begin{array}{l} P(v) \vee Q(w) \\ \hline\end{array} \end{array} & \text{assumption} \\
4 & \begin{array}{ll} & \forall x (P(x) \vee Q(w)) \end{array} & \text{$\forall$I, 3} \\
5 & \forall x (P(x) \vee Q(w)) & \text{$\exists$E, 2, 3, 4} \\
6 & \exists y (\forall x (P(x) \vee Q(y))) & \text{$\exists$I, 5} \\
\end{array}
$$
Edit: I know that this proof is incorrect, since replacing $P(x) \vee Q(y)$ with $R(x, y)$ would yield the result
$$
\forall x (\exists y (R(x, y)) \vdash \exists y (\forall x (R(x, y)))
,$$
which is clearly not true in general.
I'm not exactly sure on which line the flaw is. I would appreciate it if someone could point that out, and explain why it's wrong.
I suspect that I'm supposed to use the distributivity of $\exists$ over $\vee$ for this one. But I don't know how to formally justify this distributivity, and I can't find a natural deduction proof for it.
Edit: I think I have successfully proved this, based on @ZevChonoles's answer. Here is a screencap:

 A: You can't go from step 3 to step 4. For the particular $v$ you chose, you know that you can find $w$ such that $P(v)\vee Q(w)$. If $Q(w)$ is true, then certainly $P(x)\vee Q(w)$ is true for all $x$, but if $Q(w)$ is false there's no reason why it should be the case that $P(x)\vee Q(w)$ for all $x$.

I don't know how to write this in the Fitch format, but the essential idea is just that either $Q(y)$ is true for some $y$, or $Q(y)$ is false for all $y$. 
If $Q(v)$ is true for some particular $v$, then $P(x)\vee Q(v)$ is true for all $x$, and so we certainly have that $\exists y(\forall x(P(x)\vee Q(y)))$; the $y$ that exists is just $y=v$.
If $Q(y)$ is false for all $y$, then $P(x)\vee Q(y)\iff P(x)$, so $\forall x(\exists y(P(x)\vee Q(y)))$ implies that $P(x)$ is true for all $x$, and hence $\exists y(\forall x(P(x)\vee Q(y)))$; any $y$ at all will work.
A: Universal introduction has the condition that the name letter generalized upon, cannot occur in any assumption still in effect (equivalently, can't occur in any assumption in the assumption set).  It doesn't matter if they appeared anywhere else, the rule only says that they can't appear in any assumption still in effect.  At step 3 you have the name letters "v" and "w".  So, can't generalize on v to get to line 4.  This behaves just like the following:
1 | (Fa $\lor$ Gb) assumption
2 | $\forall$x(Fx $\lor$ Gb)  1 universal introduction (invalid!)
3 ((Fa $\lor$ Gb)$\implies$$\forall$x(Fx $\lor$ Gb)) 1-2 conditional introduction
A: Like many beginners, the OP seems to be having some trouble tracking dependencies among variables -- dependencies that are created by existential specification (eliminate $\exists$) or some equivalent rule. Such dependencies never seem to be an issue in mathematics textbooks. Here is a simple alternative to tracking these dependencies that it seems most authors of mathematics textbooks follow instinctively:


*

*Introduce free variables only by a premise or existential specification (eliminate $\exists$). 

*The conclusion to every premise should not contain any free variables introduced in the premise or in any subsequent statement. The conclusion may require some universal or existential generalizations to get rid of any "new" free variables. (Do existential generalizations (introduce $\exists$) before generating conclusion.) 
This is not a new form of logic. Rather, it can be seen as a set of guidelines for writing formal mathematical proofs analogous to structured programming guidelines in CS. 
Example using DC Proof 2.0 at http://www.dcproof.com/ConclusionExample.htm 
A: Here is the OP's revised proof placed in a Fitch-style proof checker verifying that the proof is correct using Zev Chonoles' suggestion to use the law of the excluded middle on $\exists y Qy \lor \lnot \exists y Qy$. 
This also verifies that existential elimination and universal introduction were used correctly. In this proof the variables $x$ and $y$ where substituted with names $a$ and $b$ when not bound by a quantifier:


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
