Rules of Inference : Showing that we can conclude $\exists xP(x) \lor \exists xQ(x)$ from $\exists x( P(x) \lor Q(x))$ From my discrete mathematics class, we are given an exercise, where one of the question is we have to prove that we can conclude $\exists xP(x) \lor \exists xQ(x)$ from $\exists x( P(x) \lor Q(x))$ using only rules of inference. Some of my fellow students think that we can do that by first using existential instantiation so $\exists x( P(x) \lor Q(x))$ become $P(c) \lor Q(c)$ for a specific element $c$ in domain $x$, and then existential generalization it, but to $\exists xP(x) \lor \exists xQ(x)$. Is it right? And if so, why? I can't understand why it become $\exists xP(x) \lor \exists x Q(x)$ instead of $\exists x( P(x) \lor Q(x))$ again.
 A: It all depends on exactly what inference rules you have to work with, but if you have something that formalizes a 'proof by cases', then from $P(c) \lor Q(c)$ you can infer $\exists x\ P(x)$ ( and thus $\exists x \ P(x) \lor \exists x \ Q(x)$ from the $P(c)$ case, and $\exists x \ Q(x)$ (and thus again $\exists x \ P(x) \lor \exists x \ Q(x)$) from the $Q(c)$ case.
Here is a formal proof to this effect created in the Fitch system:

A: Basically they are relying on $\exists x~(Sx\vee T)\iff (\exists x~Sx)\vee T$ holding if $x$ is not occuring free within $T$. 
$\begin{array}{l|l:l}1 & \exists x ~(Px \vee Qx) & \text{Assume/Premise}
\\ 2 & \quad Pc\vee Qc & \text{Existential Instantiation/Elimination}
\\ 3 & \quad \exists x~(Px \vee Qc) & \text{Existential Generalisation}
\\ 4 & \quad (\exists x~Px)\vee Qc & \text{Distribution}
\\ 5 & \exists x~((\exists x~Px)\vee Qx) & \text{Existential Generalisation}
\\ 6 & (\exists x~Px)\vee (\exists x~Qx) & \text{Distribution}
\\ \Box & 
\end{array}$

If you don't wish to use distribution, then use Disjunctive Syllogism .
$\begin{array}{l|l:l}1 & \exists x ~(Px \vee Qx) & \text{Assume/Premise}
\\ 2 & \quad Pc\vee Qc & \text{Existential Instantiation/Elimination}
\\ 3 & \qquad Pc & \text{Assume}
\\ 4 & \qquad \exists x~Px & \text{Existential Generalisation/Introduction}
\\ 5 & \quad Pc\to \exists x~Px & \text{Conditional Introduction / Discharge Assumption}
\\ 6 & \quad Qc\to \exists x~Qx & \text{Similarly}
\\ 7 & \exists x~Px~\vee~\exists x~Qx & \text{Disjunctive Syllogism/Elimination}
\\ \Box & 
\end{array}$

