
Introduction to Logic

Tools for Thought

As an illustration of these concepts, consider the following problem. Suppose we believe that everybody loves somebody. And suppose we believe that everyone loves a lover. Our job is to prove that Jack loves Jill.
First, we need to formalize our premises. Everybody loves somebody. For all y, there exists a z such that loves(y,z).
∀y.∃z.loves(y,z)
Everybody loves a lover. If a person is a lover, then everyone loves him. If a person loves another person, then everyone loves him. For all x and for all y and for all z, loves(y,z) implies loves(x,y).
∀x.∀y.(∃z.loves(y,z) ⇒ loves(x,y))
Our goal is to show that Jack loves Jill. In other words, starting with the preceding sentences, we want to derive the following sentence.
loves(jack,jill)

A proof of this result is shown below. Our premises appear on lines 1 and 2. The sentence on line 3 is the result of applying Universal Elimination to the sentence on line 1, substituting jill for y. The sentence on line 4 is the result of applying Universal Elimination to the sentence on line 2, substituting jack for x. The sentence on line 5 is the result of applying Universal Elimination to the sentence on line 4, substituting jill for y. Finally, we apply Implication Elimination to produce our conclusion on line 6.
1.  ∀y.∃z.loves(y,z)  Premise 
2.  ∀x.∀y.(∃z.loves(y,z) ⇒ loves(x,y))  Premise 
3.  ∃z.loves(jill,z)  UE: 1 
4.  ∀y.(∃z.loves(y,z) ⇒ loves(jack,y))  UE: 2 
5.  ∃z.loves(jill,z) ⇒ loves(jack,jill)  UE: 4 
6.  loves(jack,jill)  IE: 5,3 

Now, let's consider a slightly more interesting version of this problem. We start with the same premises. However, our goal now is to prove the somewhat stronger result that everyone loves everyone. For all x and for all y, x loves y.
∀x.∀y.loves(x,y)

The proof shown below is analogous to the proof above. The only difference is that we have free variables in place of object constants at various points in the proof. Once again, our premises appear on lines 1 and 2. Once again, we use Universal Elimination to produce the result on line 3; but this time the result contains a free variable. We get the results on lines 4 and 5 by successive application of Universal Elimination to the sentence on line 2. We deduce the result on line 6 using Implication Elimination. Finally, we use two applications of Universal Introduction to generalize our result and produce the desired conclusion.
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 
6.  loves(x,y)  IE: 5,3 
7.  ∀y.loves(x,y)  UI: 6 
8.  ∀x.∀y.loves(x,y)  UI: 7 

This second example illustrates the power of free variables. We can manipulate them as though we are talking about specific individuals (though each one could be any object); and, when we are done, we can universalize them to derive universally quantified conclusions.

Use the arrow keys to navigate.
