Equivalence in natural deduction in First-order logic

Question

Task

$\vdash \exists x (P(x)\lor Q(x)) \iff \exists xP(x) \lor \exists xQ(x) $

My answer

If we have $A \iff B$ then $A\vdash B$ and $B \vdash A$. So I started trying to see if I could prove $B$ from $A$, but in my tests I couldn't prove that. Below is an image of my attempt.

Is this correct or am I missing a step here? Any help is appreciated, thanks!

Edit

Would it maybe be possible to replace the $?$ with $Q(u) \space\space\space \space \neg Q(u)$ which would result in $\bot$ and from there I could use RAA?

Answer 1

A derivation in natural deduction proving that $\exists x (P(x) \lor Q(x)) \vdash \exists x \, P(x) \lor \exists x \, Q(x)$: $$ \dfrac{\exists x (P(x) \lor Q(x)) \quad \dfrac{[P(x) \lor Q(x)]^*\quad \dfrac{\dfrac{[P(x)]^{**}}{\exists y \, P(y)}\exists_i}{\exists y P(y) \lor \exists z Q(z)}\lor_{i_R} \quad \dfrac{\dfrac{[Q(x)]^{**}}{\exists z \, Q(z)}\exists_i}{\exists y P(y) \lor \exists z Q(z)}\lor_{i_L}}{\exists y \, P(y) \lor \exists z \, Q(z)}\lor_e^{**}}{\exists y \, P(y) \lor \exists z \, Q(z)}\exists_e^* $$

The other direction is quite similar: the last rule of the derivation is a $\lor_e$ whose minor premises are conclusions of $\exists_e$.

In both directions there is no need for RAA.

Answer 2

Here's an outline (in words) of how you could approach proving that $LHS \vdash RHS$:

Suppose that $\exists x (P(x) \vee Q(x))$. Then choose a witness $a$ for this existence statement, so that $P(a) \vee Q(a)$. We then proceed using a proof by cases to show that $(\exists x P(x)) \vee (\exists x Q(x))$. In the first case, if $P(a)$, then it immediately follows that $\exists x P(x)$, so we can conclude $(\exists x P(x)) \vee (\exists x Q(x))$. Likewise, if $Q(a)$, then it immediately follows that $\exists x Q(x)$, so we can conclude $(\exists x P(x)) \vee (\exists x Q(x))$ in this case also. $\quad\square$

Answer 3

If there is something that satisfies P or Q, then there is a case for something satisfying P or there is a case for something satisfying Q.
$$\dfrac{\dfrac{\dfrac{[\exists x~(P(x)\vee Q(x))]^1}{a:P(a)\vee Q(a)}~\dfrac{\dfrac{[a:P(a)]^2}{\phantom{\exists x~P(x)}}}{\phantom{\exists x~P(x)~\vee~\exists x~Q(x)}}~\dfrac{\dfrac{[a:Q(a)]^2}{\phantom{\exists x~Q(x)}}}{\phantom{\exists x~P(x)~\vee~\exists x~Q(x)}}}{{\exists x~P(x)~\vee~\exists x~Q(x)}}{^2}}{\exists x~(P(x)\vee Q(x))~\to~(\exists x~P(x)~\vee~\exists x~Q(x))}{^1}$$

---

If there is something that satisfies P then there is something satisfying P or Q. If there is something that satisfies Q then there is something satisfying P or Q. In either case the conclusion holds.

$$\dfrac{\dfrac{\lower{8ex}{[\exists x~P(x)~\vee~\exists x~Q(x)]^1}~\dfrac{[\exists x~P(x)]^2}{\dfrac{\phantom{a:P(a)}}{\dfrac{\phantom{a:P(a)\vee Q(a)}}{\phantom{\exists x~(P(x)\vee Q(x))}}}}~\dfrac{[\exists x~Q(x)]^2}{\dfrac{\phantom{a:Q(a)}}{\dfrac{\phantom{a:P(a)\vee Q(a)}}{\phantom{\exists x~(P(x)\vee Q(x))}}}}}{\exists x~(P(x)\vee Q(x))}{^2}}{(\exists x~P(x)~\vee~\exists x~ Q(x))~\to~\exists x~(P(x)\vee Q(x))}{^1}$$