Rules of Inference : Showing that we can conclude $\exists xP(x) \lor \exists xQ(x)$ from $\exists x( P(x) \lor Q(x))$

Question

From my discrete mathematics class, we are given an exercise, where one of the question is we have to prove that we can conclude $\exists xP(x) \lor \exists xQ(x)$ from $\exists x( P(x) \lor Q(x))$ using only rules of inference. Some of my fellow students think that we can do that by first using existential instantiation so $\exists x( P(x) \lor Q(x))$ become $P(c) \lor Q(c)$ for a specific element $c$ in domain $x$, and then existential generalization it, but to $\exists xP(x) \lor \exists xQ(x)$. Is it right? And if so, why? I can't understand why it become $\exists xP(x) \lor \exists x Q(x)$ instead of $\exists x( P(x) \lor Q(x))$ again.

Answer 1

It all depends on exactly what inference rules you have to work with, but if you have something that formalizes a 'proof by cases', then from $P(c) \lor Q(c)$ you can infer $\exists x\ P(x)$ ( and thus $\exists x \ P(x) \lor \exists x \ Q(x)$ from the $P(c)$ case, and $\exists x \ Q(x)$ (and thus again $\exists x \ P(x) \lor \exists x \ Q(x)$) from the $Q(c)$ case.

Here is a formal proof to this effect created in the Fitch system:

Answer 2

Basically they are relying on $\exists x~(Sx\vee T)\iff (\exists x~Sx)\vee T$ holding if $x$ is not occuring free within $T$.

$\begin{array}{l|l:l}1 & \exists x ~(Px \vee Qx) & \text{Assume/Premise} \\ 2 & \quad Pc\vee Qc & \text{Existential Instantiation/Elimination} \\ 3 & \quad \exists x~(Px \vee Qc) & \text{Existential Generalisation} \\ 4 & \quad (\exists x~Px)\vee Qc & \text{Distribution} \\ 5 & \exists x~((\exists x~Px)\vee Qx) & \text{Existential Generalisation} \\ 6 & (\exists x~Px)\vee (\exists x~Qx) & \text{Distribution} \\ \Box & \end{array}$

---

If you don't wish to use distribution, then use Disjunctive Syllogism .

$\begin{array}{l|l:l}1 & \exists x ~(Px \vee Qx) & \text{Assume/Premise} \\ 2 & \quad Pc\vee Qc & \text{Existential Instantiation/Elimination} \\ 3 & \qquad Pc & \text{Assume} \\ 4 & \qquad \exists x~Px & \text{Existential Generalisation/Introduction} \\ 5 & \quad Pc\to \exists x~Px & \text{Conditional Introduction / Discharge Assumption} \\ 6 & \quad Qc\to \exists x~Qx & \text{Similarly} \\ 7 & \exists x~Px~\vee~\exists x~Qx & \text{Disjunctive Syllogism/Elimination} \\ \Box & \end{array}$

---