# How do I apply existential elimination to the following Fitch proof?

I am trying to prove ∀x.∀y.loves(x,y) from Relational Proofs using the Fitch system from Barwise and Etchemendy.

I can get as far as line 5, but I cannot figure out how to apply Existential Elimination on line 6 in the Fitch system.

Any help would be appreciated.

```1.  ∀y.∃z.loves(y,z)                      Premise
2.  ∀x.∀y.∀z.(loves(y,z) ⇒ loves(x,y))   Premise
3.  ∃z.loves(y,z)                         UE: 1
4.  ∀y.∀z.(loves(y,z) ⇒ loves(x,y))      UE: 2
5.  ∀z.(loves(y,z) ⇒ loves(x,y))         UE: 4 OK to here
6.  loves(x,y)                            EE: 3, 5
7.  ∀y.loves(x,y)                         UI: 6
8.  ∀x.∀y.loves(x,y)                      UI:
```

My best effort is as follows:

```1.  ∀y.∃z.loves(y,z)                   Premise
2.  ∀x.∀y.∀z.(loves(y,z) ⇒ loves(x,y))  Premise
3.  ∃z.loves(a,z)                       UE: 1
4.  ∀y.∀z.(loves(y,z) ⇒ loves(b,y))    UE: 2
5.  ∀z.(loves(a,z) ⇒ loves(b,a))        UE: 4
6.  loves(b,a)                          FO Con: 3,5
8.  ∀x.∀y.loves(x,y)                    FO Con 2,6
```

Note that I am using arbitrary constants instead of the free variables suggested. This is because I do not know how to use free variables in Fitch. Also I am using First Order consequence (FO Con) instead of Existential Elimination. In short I cannot follow the Stanford Proof using the Fitch system.

• From 3: ∃z.loves(y,z) you have to apply Existential Eliminationintroducing a new variable a to get loves(y,a). Commented Jun 8, 2017 at 11:12
• But then, you have to use a in 5. to get loves(y,a) ⇒ loves(x,y). Commented Jun 8, 2017 at 11:15
• Thanks for the advice, I have tried this approach. I can start a sub proof at 3 with a new variable, but I cannot get out of the sub proof. Commented Jun 8, 2017 at 17:53
• The second paragraph of Chapter 13 from Barwise and Etchemendy seems to indicate that Fitch does not allow free variables in proofs. Commented Jun 8, 2017 at 22:24
• Your second solution seems ok... FO Con is only a "shortcu" for ExElim after step 3 with new const c to get loves(a,c) followed by UE from 5 with c to get loves(a,c) ⇒ loves(b,a) and finally modus ponens. Commented Jun 9, 2017 at 8:44

I have added what I think is a solution in Fitch

Any comments would be appreciated. My attempt seems much longer than the Stanford Proof (8.3), which talks about "the power of free variables". I think I need to post another question concerning Fitch, free variables, and arbitrary constants. I would have posted this as an edit to my original question, but being a new user I am restricted to two links

Here is a shorter proof than the one provided in an answer: https://philosophy.stackexchange.com/a/42928/29944 It is similar to the first 9 lines of this proof, but proceeds with universal introduction right after that.

To use the proof checker, I replaced loves(x,y) with Lxy to fit its input requirements.

Once I derived line 8 that did not have the constant c, I could close the subproof discharging the assumption on line 6 with existential elimination as the inference rule. This proof also uses constants rather than free variables for existential and universal elimination.

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

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf

• Thanks for the proof. I could not replicate your proof from line 9 on, using Fitch software. I think that Fitch needs a very specific form of universal instantiation, see an earlier post Commented Jun 14, 2019 at 17:18

I suggest starting from the end -- thusly work towards the target.

It is also useful to indent the proof when you introduce a new term.

If the target is a double universal, we need to introduce those from the assumption of two arbitrary terms.

`````` 1.|  ∀y.∃z.loves(y,z)                      Premise
2.|_ ∀x.∀y.∀z.(loves(y,z) ⇒ loves(x,y))   Premise
3.|  |_ [a]
4.|  |  |_ [b]
:  :  :
|  |  |  loves(a,b)
|  |  ∀y.loves(a,y)                       UI: 4-?
|  ∀x.∀y.loves(x,y)                       UI: 3-?
``````

Now to derive that `loves(a,b)` from the implication we need to eliminate two universals in the second premise with replacements [x\a] and [y\b]

`````` 1.|  ∀y.∃z.loves(y,z)                      Premise
2.|_ ∀x.∀y.∀z.(loves(y,z) ⇒ loves(x,y))   Premise
3.|  |_ [a]
4.|  |  |_ [b]
5.|  |  |  ∀y.∀z.(loves(y,z) ⇒ loves(a,y)) UE: 2 [x\a]
6.|  |  |  ∀z.(loves(b,z) ⇒ loves(a,b))    UE: 5 [y\b]
:  :  :
|  |  |  loves(a,b)
|  |  ∀y.loves(a,y)                       UI: 4-?
|  ∀x.∀y.loves(x,y)                       UI: 3-?
``````

Thusly we come to the need to prepare the antecedent with a witness for the existential embedded in the first premise (by first eliminating the universal).

Which basically completes the proof after eliminating a universal, and the conditional, to then derive the immediate target with an existential elimination.

`````` 1.|  ∀y.∃z.loves(y,z)                      Premise
2.|_ ∀x.∀y.∀z.(loves(y,z) ⇒ loves(x,y))   Premise
3.|  |_ [a]
4.|  |  |_ [b]
5.|  |  |  ∀y.∀z.(loves(y,z) ⇒ loves(a,y)) UE: 2 [x\a]
6.|  |  |  ∀z.(loves(b,z) ⇒ loves(a,b))    UE: 5 [y\b]
7.|  |  |  ∃z.loves(b,z)                    UE: 1 [y\b]
8.|  |  |  |_ [c] loves(b,c)                Ass:
9.|  |  |  |  loves(b,c) ⇒ loves(a,b)      UE: 6 [z\c]
10.|  |  |  |  loves(a,b)                    ⇒E: 8,9
11.|  |  |  loves(a,b)                       EE: 7,8-10
12.|  |  ∀y.loves(a,y)                       UI: 4-11
13.|  ∀x.∀y.loves(x,y)                       UI: 3-12
``````
• Thanks for your proof. It is shorted than mine and also works with Fitch software. Commented Jun 14, 2019 at 17:41