# Help with an existential natural deduction proof

From the assumption

∃x∃y R(x, y)

I need to derive the conclusion

∃y∃x R(x, y)

From the comments: I tried to use Existential Elimination but I can't figure out how to do it properly.

• What have you tried? Where are you stuck? – Eliran Aug 12 '19 at 1:19
• I tried to use Existential Elimination but cant figure out how to do it properly. – Rajamani Sarvesh Aug 12 '19 at 1:23

Here is a forward proof that gets by without contradiction, constructed with the Natural deduction proof editor and checker: Your problem presumably was that you can't just eliminate the existential quantifiers directly to replace them by an individual constant -- this would be unsound, and an incorrect application of the ∃E rule -- but rather the rule requires a subproof, where you make an assumption with the existentially quantified variable substituted by a term, derive some conclusion from this assumption, and this conclusion, rather than the substituted formula itself, will be the conclusion of the ∃E step. The structure of the ∃E rule is somewhat similar to ∨E.

So what you need to do is assume the formula with the quantifier eliminated, from that derive the formula with the quantifiers swapped by re-introducing them in reverse order, and have that as the conclusion to your ∃E rule, where you cite 1. the formula with the quantifier still present and 2. the subderivation from the assumption with the quantifier eliminated to the desired conclusion. The whole thing nested to take care of both of the existential quantifiers -- this is what you end up with.

From the comments: I tried to use Existential Elimination but I can't figure out how to do it properly.

Existential Elimination: When given that an existential statement (eg `∃z P(z)`) holds, and show that a statement (eg `Q`) may be derived when we assume a witness for the existential (eg `P(c)`, where `c` is a term that does not occur within `P(z)` or `Q`), then we may deduce that `Q` holds.

``````|  ∃z P(z)
|  |_ P(c)      c is a term (local to the context) which does not occur within P(z).
:  :  :
|  |  Q         c does not occur within Q
|  Q
``````

Existential Introduction: When you have derived a statement within a context, you may infer an existential statement within that context, replacing some of the terms with the quantifier's bound term (which must not occur within the statement).

``````|  |  S(c)
|  |  ∃z S(z)         z does not occur within S(c)
``````

So because you begin with `∃x ∃y R(x,y)` and wish to conclude with `∃y ∃x R(x,y)`, therefore you need to eliminate two existentials, and introduce two more.

``````|  ∃x ∃y R(x,y)
|  |_ ∃y R(a,y)        Assume for some a
|  |  |_ R(a,b)        Assume for some b
|  |  |  ∃x R(x,b)     Existential Introduction
|  |  |  ∃y ∃x R(x,y)  Existential Introduction
|  |  ∃y ∃x R(x,y)     Existential Elimination
|  ∃y ∃x R(x,y)        Existential Elimination
``````

That is all.