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?

  • $\begingroup$ Are you using natural deduction? $\endgroup$ – Taroccoesbrocco Nov 5 '18 at 8:04
  • $\begingroup$ Because there are multiple formal proof systems, it is important to say exactly which system you are using. $\endgroup$ – Carl Mummert Nov 5 '18 at 12:26
  • $\begingroup$ @Taroccoesbrocco Yes. Sorry for not making it clear. $\endgroup$ – 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)$.

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

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

enter image description here

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/

  • 1
    $\begingroup$ 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. $\endgroup$ – Graham Kemp Aug 25 at 3:04
  • $\begingroup$ @GrahamKemp There may be alternate ways to do this. That this works is all I'm aiming for. $\endgroup$ – Frank Hubeny Aug 25 at 3:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.