Natural deduction proof: distributivity of existential quantification

Question

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?

Answer 1

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.