Subsection 5.2.7 Lemmas
Recall that a lemma is really just a theorem. But we typically call a theorem a lemma when the reason that we’ve proved it is that it’s a useful intermediate step. Once it’s proved, we can use it as often as we like in other proofs. The idea of proving lemmas so that we can save a lot of repeated work can be very useful. We saw several examples of this in our discussion of Boolean logic. Lemmas can be even more useful when we’re working in predicate logic because there may be many more steps involved in our proofs.
Wine and Chocolate
Define:
Wine(x): True if x is a wine lover.
Choc(x): True if x is a chocolate lover.
Food(x): True if x loves food.
Drink(x): True if x loves drinks.
Paris(x): True if x loves Paris.
Suppose that we’re given the following premises:
x (Choc(x) Food(x)) Chocolate lovers are food lovers.
x (Wine(x) Drink(x)) Wine lovers are drink lovers.
x ((Drink(x) Food(x)) Paris(x)) Anyone who loves food and drink loves Paris.
We’re also told about a lot of people who love wine and chocolate. We’d like to be able to peg all of them as Paris lovers. The easiest way to do that will be to prove a lemma:
x ((Wine(x) Choc(x)) Paris(x))
Then we can go directly to Paris-loving for everyone who’s a lover of wine and chocolate. This is a particularly good thing to do because proving the lemma, while not hard, is a bit annoying. We don’t want to have to do that reasoning more than once. So here it is (once):
[1] x (Choc(x) Food(x)) Premise
[2] x (Wine(x) Drink(x)) Premise
[3] x ((Drink(x) Food(x)) Paris(x)) Premise
We’ll use the Conditionalization inference rule. So we’ll assume the antecedent of our goal. More specifically, we’ll assume that it’s true of some arbitrary individual c. At the end of the proof, we can generalize it to all individuals.
[4] (Wine(c) Choc(c)) (Conditional) Premise
[5] Choc(c) Simplification [4]
[6] Choc(c) Food(c) Universal Instantiation [1]
[7] Food(c) Modus Ponens [5], [6]
[8] Wine(c) Simplification [4]
[9] Wine(c) Drink(c) Universal Instantiation [2]
[10] Drink(c) Modus Ponens [8], [9]
[11] (Drink(c) Food(c)) Paris(c) Universal Instantiation [3]
[12] (Drink(c) Food(c)) Conjunction [10], [7]
[13] Paris(c) Modus Ponens [12], [11]
[14] (Wine(c) Choc(c)) Paris(c) Conditional Discharge [4], [13]
[15] x ((Wine(x) Choc(x)) Paris(x)) Universal Generalization [14]
Whew. Done. Now we can identify a lot of Paris lovers very easily.