2

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.

  • 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
2

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

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.

enter image description here

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 – Patrick Browne Jun 14 at 17:18
1

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. – Patrick Browne Jun 14 at 17: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.