In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic:
$(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,Q$ where $P$ does not have free occurences of variable x.
I managed to do the prove, until I arrived at the following:
$\frac{}{\exists x.P\lor Q, P \lor Q \ \vdash \ (\exists x. P) \lor (\exists x.Q)}$
Unfortunately, applying $\lor-elimination$ only strengthens what I need to prove, so applying that doesn't work. In general, whichever rule I try to apply, I cannot get far. I also cannot apply $\exists-elimination$, as the $Q$ in $P\lor Q$ is not guaranteed to have only bound occurenes of x.
Actually, $\frac{}{\exists x.P\lor Q, P \lor Q \ \vdash \ (\exists x. P) \lor (\exists x.Q)}$ is just a rewritten form of distributivity of existential quantification: $\frac{}{\vdash \ \exists x.P\lor Q \rightarrow (\exists x. P) \lor (\exists x.Q)}$.
How shall I proceed in the prove?