Give syntax proof of FOL Formla $\exists x.P(x) \lor \exists x.Q(x)$ $\vdash$ $\exists x.(P(x) \lor Q(x))$

Question

So the question is pretty much described in the title already. I have to show the following result. I have tried it but am failing to do so. Anyone who can please help me in understanding its proof. I have attached the picture of formulas that may prove to be helpful.

$\exists x.P(x) \lor \exists x.Q(x)$ $\vdash$ $\exists x.(P(x) \lor Q(x))$

Answer 1

Hint: the proof has 3 instances of an elimination rule.

Consider that the premise has as the principal operator a Vel, whereas on the right we have an existential quantifier.

Try to work backward to see what you need: clearly the last rule will be an application of $\exists$-introduction after a derivation of the formula $Pa \lor Qa$.

If you're still stuck let me know and I'll give you another hint.

Answer 2

Let us get you started with the derivation for $\exists x~.P(x)~\lor~\exists x~.Q(x)\vdash \exists x~.(P(x)\lor Q(x))$ using the Gentzen tree system.

$$\dfrac{\exists x~.P(x)~\lor~\exists x~.Q(x)\\\qquad\qquad\vdots}{\exists x~.(P(x)\lor Q(x))}{?}$$

---

Well, existential statements may be derived either by construction, or by reduction to absurdity.   Which is appropriate here?

We have existences in the premise, so that indicates we may be constructive.   Thus we shall be using existential introduction using a witnesses derived from the premise's existentials.

But wait!   To access those existentials we will first need to eliminate that disjunction.

$$\dfrac{\lower{1.5ex}{\exists x~.P(x)~\lor~\exists x~.Q(x)}\quad\dfrac{[\exists x~.P(x)]^1\\\quad\vdots}{\exists x~.(P(x)\lor Q(x))}\quad\dfrac{[\exists x~.Q(x)]^2\\\quad\vdots}{\exists x~.(P(x)\lor Q(x))}}{\exists x~.(P(x)\lor Q(x))}{\small\lor\textsf{elim}^{1,2}}$$

---

Now you can look to the existential introduction and elimination rules, and disjunction introduction while we are at it.$$\dfrac{\lower{1.5ex}{\exists z~.\phi(z)}~~\dfrac{[\phi(t)]^1\\\quad\vdots}{\psi}}{\psi}{\small\exists\textsf{elim}^1}\qquad\dfrac{\rho(t)}{\exists z~.\rho(z)}{\small\exists\textsf{intro}}\\~\\~\\\dfrac{\chi(s)}{\chi(s)\lor\varphi(s)}{\small\lor\textsf{intro}}\qquad\dfrac{\varphi(t)}{\chi(t)\lor\varphi(t)}{\small\lor\textsf{intro}}$$

Just put it together.