$$
\vdash \exists x(P(x)\lor Q(x))\Leftrightarrow \exists xP(x)\lor \exists xQ(x)
$$
I'm unsure about a step in my (forward direction) attempt in solving this using natural deduction proof:
Forward direction:
1.* $\exists x(P(x)\lor Q(x))$ (Assumption)
2.* $P(c)\lor Q(c)$ ($\exists$-elim 1)
3.** $\lnot Q(c)$ (Assumption)
4.** $P(c)$ ($\lor$-elim 2,3)
5.** $\exists x(P(x))$ ($\exists$-intro 4)
6.** $\exists xP(x)\lor \exists xQ(x)$ ($\lor$-intro 5)
By ($\Rightarrow$– elimination 1,6) can I deduce:
- $\exists x(P(x)\lor Q(x))\Rightarrow \exists xP(x)\lor \exists xQ(x)$?
Thanks in advance!
Best Answer
This is very close! You showed that assuming $\exists x(P(x)\vee Q(x))$ and $\neg Q(c)$ that $\exists x P(x) \vee \exists x Q(x)$ . Notice how this uses the extra assumption that $\neg Q(c)$ is true. We can mimic a standard proof by cases here: you have already dealt with the case that $\neg Q(c)$ implies your desired conclusion, now we need to show that if we assume $Q(c)$ then your conclusion is true as well. This isn't too hard; you can just use $\exists$-intro and $\vee$-intro like you did in the other case. I'm not sure which rules your deductive system allows, but there is definitely a way to formalize a proof by cases, and this would complete your argument!