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

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?

• Are you using natural deduction? – Taroccoesbrocco Nov 5 '18 at 8:04
• Because there are multiple formal proof systems, it is important to say exactly which system you are using. – Carl Mummert Nov 5 '18 at 12:26
• @Taroccoesbrocco Yes. Sorry for not making it clear. – Ang. Nov 6 '18 at 8:41

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)$$.

• Do you mean by imagining doing S[$x_0$/y] to get S($y_0$, $x_0$) ? – Ang. Nov 5 '18 at 7:27
• Yes, apply 'existential generalization' twice: once to introduce $\exists y$ and once more to introduce $\exists x$. – Magdiragdag Nov 5 '18 at 8:44
• Okay, thank you so much for this! – Ang. Nov 5 '18 at 9:12

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/

• Well, that is valid, but it is a rather roundabout route. You can do it directly with just assumptions, disjunction elimination, existential introductions, and existential eliminations. – Graham Kemp Aug 25 at 3:04
• @GrahamKemp There may be alternate ways to do this. That this works is all I'm aiming for. – Frank Hubeny Aug 25 at 3:41