Find a natural deduction proof to show ∃x∃y (S(x,y) ∨ S(y,x)) ⊢ ∃x∃y S(x,y) by predicate logic.

Question

I'm trying to prove $\exists x \exists y (S(x,y) \lor S(y,x)) \vdash \exists x \exists y S(x,y)$ in natural deduction, and I have already applied existential elimination to get $S(x_0,y_0)$, with $x_0$ and $y_0$ being the assumptions.

Yet I'm stuck on how to prove $S(x_0,y_0)$ from $S(x_0,y_0) \lor S(y_0,x_0)$ after getting $S(x_0,y_0) \lor S(y_0,x_0)$ from existential elimination.

Can someone help me out or is there other ways to approach this question?

Answer 1

From $S(x_0,y_0)$ you conclude $\exists x \exists y S(x,y)$ by using existential generalization twice, once to introduce $\exists y$ and once more to introduce $\exists x$. From $S(y_0,x_0)$ you also conclude $\exists x\exists y S(x,y)$. Therefore you can conclude $\exists x\exists y S(x,y)$ from $S(x_0,y_0) \lor S(y_0,x_0)$.

Answer 2

Here is a proof using a Fitch-style proof checker:

Note that I used universal elimination twice from the same line 3. This allowed me to ultimately derive a contradiction on line 13 from the two disjuncts on line 9.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/