Subsection 8.6.3 Copy and Paste
Sometimes when we’re working on a proof, we don’t have exactly the theorem or lemma that we need. But we may have one that’s very similar. When that happens, we may be able to start our new proof by cutting and pasting the proof that we’ve already got for the related theorem. Sometimes it works exactly as it is. More often, we need to tweak it. But at least we had a place to start from.
Suppose that we want to prove that everyone has a (possibly no longer living) great grandmother. (By the way, it’s not important that you follow every line of this excruciating proof. The point of this example is that there has to be a better way to write proofs.)
Assume the following premises:
[1] x (y (MotherOf(y, x)))
[2] x (y (FatherOf(y, x)))
[3] x (y (MotherOf(y, x) ParentOf(y, x)))
[4] x (y (FatherOf(y, x) ParentOf(y, x)))
[5] x (y (GreatGrandMotherOf(y, x) (z (MotherOf(y, z) t (ParentOf(z, t)
ParentOf(t, x)))))) (Definition)
[6] x (y (GreatGrandFatherOf(y, x) (z (FatherOf(y, z) t (ParentOf(z, t)
ParentOf(t, x)))))) (Definition)
We need to prove:
x (y (GreatGrandMotherOf(y, x)))Suppose that we wanted to do a detailed proof. Here’s one. In case you want to follow the details, we’ll add a key piece of information to every line that uses Instantiation or Generalization: Let p/x mean that, when we write the new line, we are substituting p for every instance of the variable x in the starting line. We’re doing so many of these, that this may help make it clearer what is going on.
[7] (y (MotherOf(y, p1)) Universal Instantiation p1/x [1]
[8] MotherOf(y1*, p1) Existential Instantiation y1*/y [7]
[9] y (MotherOf(y, p1) ParentOf(y, p1)) Universal Instantiation p1/x [3]
[10] MotherOf(y1*, p1) ParentOf(y1*, p1) Universal Instantiation y1*/y [9]
[11] ParentOf(y1*, p1) Modus Ponens [8],[10]
[12] (y (MotherOf(y, y1*)) Universal Instantiation y1*/ x [1]
[13] MotherOf(y2*, y1*) Existential Instantiation y2*/y [12]
[14] ParentOf(y2*, y1*) Modus Ponens [8],[13]
[15] (y (MotherOf(y, y2*)) Universal Instantiation y2*/ x [1]
[16] MotherOf(y3*, y2*) Existential Instantiation y3*/y [15]
Notice that now we have that p1 has parent y1*, y1* has parent y2*, and y2* has mother y3*. We’re close. We need to use the definition of great grandmother [5]. But we only need it in one direction (the one that concludes great grandmotherness), so let’s split it out to make things easier:
[17] x (y ((z (MotherOf(y, z) t (ParentOf(z, t) ParentOf(t, x))) GreatGrandMotherOf(y, x))) [5]
[18] y ((z (MotherOf(y, z) t (ParentOf(z, t) ParentOf(t, p1))) GreatGrandMotherOf(y, p1)) Universal Instantiation p1/x [17]
[19] (z (MotherOf(y3*, z) t (ParentOf(z, t) ParentOf(t, p1))) GreatGrandMotherOf(y3*, p1) Universal Instantiation y3*/y [18]
[20] ParentOf(y2*, y1*) ParentOf(y1*, p1) Conjunction [14], [11]
[21] t (ParentOf(y2*, t) ParentOf(t, p1)) Existential Generalization t/ y1* [20]
[22] (MotherOf(y3*, y2*) t (ParentOf(y2*, t) ParentOf(t, p1)) Conjunction [16], [21]
[23] (z (MotherOf(y3*, z) t (ParentOf(z, t) ParentOf(t, p1))) Existential Generalization z/ y2* [22]
[24] GreatGrandMotherOf(y3*, p1) Modus Ponens [23] [17]
[25] y (GreatGrandMotherOf(y, p1) Existential Instantiation y/y3* [24]
[26] x (y (GreatGrandMotherOf(y, x))) Universal Generalization x/p1 [25]
Q. E. D. (Whew!)
Now suppose that we want to prove that everyone has a great grandfather. We could start over. Our new proof would look a lot like the one we just did except that it would use the fact that everyone has a father [2] and the definition of great grandfather [6], instead of [1] and [5], as we have done. But it made us crazy to do this once. We’d certainly not want to do it again.
We cannot simply claim that we’ve already proved the new claim. We haven’t. But there are some things we can do:
Cut and paste: Our new proof will be so similar to the one we’ve just done that we could simply cut and paste it and then make the few simple changes that are necessary. This technique actually works in many more significant domains as well. Don’t forget about it.
The proof that we just did was messy. We don’t want to spend a lot of time writing proofs like it. So let’s remind ourselves of two other approaches that we’ve already discussed:
We can prove lemmas (intermediate results) that we can reuse for new proofs.
We can skip the four column format and write more natural proofs.
Let’s consider both of these approaches to the great grandparents problem:
Lemmas: We could, in doing the great grandmother proof, have proved that every person p has some parent y1*, who, in turn, has parent y2*. We could have given that claim a name as a lemma. Then we could have started the new proof and all we’d have had to add is that y2* has a father. Then we could have gone from there to p having a great grandfather.
A more natural proof: And, of course, we could have skipped the four column proof entirely, thus avoiding having to make explicit mention of all of the instantiations and generalizations. We could, instead, have written something like: