How to solve ∃x:X.PvQ |- (∃x:X.P) v (∃x:X.Q)?

Question

What I've done is the following however I'm stuck on PvQ

∃x:X.PvQ |- (∃x:X.P) v (∃x:X.Q)

1) ∃x:X.PvQ                  hyp
2)      PvQ                  ass
.
.
.
        P=>P                 => I
        Q=>P                 => I
        P                    v E 
        P [x->x]             law P = P[x->x]
        ∃x:X.P               ∃ I
        ∃x:X.P v ∃x:X.Q      v I
 PvQ=>(∃x:X.P) v (∃x:X.Q)    => I
 ∀x:X.PvQ=>(∃x:X.P)v(∃x:X.Q) ∀ I
 (∃x:X.P) v (∃x:X.Q)         ∃ E    

Thanks once again for your help and tips!

Answer 1

If you think about this .... your proof basically attempts to derive $\exists x . P$ from $\exists x . (P \lor Q)$ .... does that follow? .... No!

Ok, so you need a different proof strategy.

Try this: after getting $P \lor Q$, try to get $\exists x \ P$ in the case of $P$, after which you can derive your conclusion with a $\lor Intro$. And in the case of $Q$, derive $\exists x \ Q$, after which again you can get your desired conclusion with $\lor Intro$. So, since in both cases you can get your conclusion, you can get your conclusion using $\lor \ Elim$, period.