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. Pat

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.

  • 1
    From 3: ∃z.loves(y,z) you have to apply Existential Eliminationintroducing a new variable a to get loves(y,a). – Mauro ALLEGRANZA Jun 8 '17 at 11:12
  • 1
    But then, you have to use a in 5. to get loves(y,a) ⇒ loves(x,y). – Mauro ALLEGRANZA Jun 8 '17 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. – Patrick Browne Jun 8 '17 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. – Patrick Browne Jun 8 '17 at 22:24
  • 1
    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. – Mauro ALLEGRANZA Jun 9 '17 at 8:44

I have added what I think is a solution in Fitch

enter image description here

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

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.