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

Question

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.

Answer 1

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

Answer 2

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

Answer 3

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