Natural deduction proof: distributivity of existential quantification

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?

You didn't say exactly what you tried, but it looks like you're trying to get there by applying elimination rules. That's not the simplest approach, and it might not work directly without case analysis on $$P$$ and $$Q$$ (I haven't tried). There's a very powerful theorem about natural deduction and most other basic logical framework: if there's a way to derive a proposition, there's a way to derive it without using elimination rules. This is called normalization. In the Curry-Howard correspondence, normalization of derivations corresponds to evaluation of programs and an introduction-only proof is a value (program with only constructors).
To prove that $$(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$$, let's use $$\rightarrow_I$$: we need to prove that if there's a derivation of $$\exists x. P \lor Q$$ then there's a derivation of $$P \lor (\exists x.Q)$$.
If there's a derivation of $$\exists x. P \lor Q$$, then there is a normal derivation of it, and in particular there is a derivation ending in $$\exists_I$$. The premise of this derivation is $$[t/x](P \lor Q) = ([t/x]P) \lor ([t/x]Q)$$ for some term $$t$$. This proposition itself has a derivation ending in one of the introduction rules for disjunction: either $$_I\lor$$ with the premise $$[t/x]P$$ or $$\lor_I$$ with the premise $$[t/x]Q$$. In the first case, we have a derivation of $$[t/x]P = P$$. In the second case, we can apply $$\exists_I$$ to derive $$\exists x. Q$$. In the first case, we can then derive $$P \lor (\exists x. Q)$$ with $$_I\lor$$. In the second case, we can derive the same proposition $$P \lor (\exists x. Q)$$ with $$\lor_I$$. We've shown that if there's a derivation of $$\exists x. P \lor Q$$ then there's a derivation of $$P \lor (\exists x. Q)$$, QED.
• Your claim about normal forms is incorrect. For example, you cannot prove $P \lor Q \to Q \lor P$ without elimination of disjunction. I believe you may have confused things a bit: the theorem you refer to works when there are no schematic letters (but we have $P$ and $Q$). Also, you are using elimination rules for existentials and disjunction in your third paragraph. You are dressing it up by talking about normal-form derivations, but it's really just elimination rules. If you think otherwise, please provide an explicit derivation or proof term that does not use any eliminations. Mar 9, 2020 at 19:28
• @AndrejBauer You're right. A value has applications under $\lambda$… I only use the fact that it's a head normal form, so the gist of my proof is correct, isn't it? Are elimination rules for disjunction and exists complete, or does the proof need to reason about normal forms? I present a proof that a derivation exists, not an opaque construction of a derivation: I show that the rule is admissible, not that it's derivable. Is it derivable? Mar 10, 2020 at 8:55