On March 7, we completed the proof of the commutativity of addition (mod sloppiness with line numbers on my part, for which I will atone by at least trying to be meticulous about such things in these notes!) We began with a technicality of notation: I introduce (Axy.P) to abbreviate (Ax.(Ay.P)) (and similarly for three or more leading universal quantifiers). Similarly, (Exy.P) abbreviates (Ex.(Ey.P)). Here is a derived rule of inference: (Axy.P) ----------- univ. quantifier switching (Ayx.P) (and variations; leading universal quantifiers may be freely reordered. This is important because it allows us to choose which variable to do induction on). Proof: 1. (Axy.Pxy), equivalently (Ax.(Ay.Pxy)) premise Goal: (Ayx.Pxy), equivalently (Ay.(Ax.Pxy)) | 2. a = a arbitrary object intro | Goal: (Ax.Pxa) | | 3. b = b arbitrary object intro | | Goal: Pba | | 4. Pba univ. elim, twice, line 1 | 5. (Ax.Pxa) univ. intro. lines 3-4 6. (Ayx.Pxy) = (Ay.(Ax.Pxy)) univ. intro. lines 2-5 We restart our line numbering for this section. We supply the last result from yesterday, with a line number. Top Level Goal: (Axy.x+y=y+x) Goal (basis step): (Ay.0+y=y+0) 1. (Ay.0+y=y+0) proved in previous section! We open a box to complete the proof by math induction, with the inductive hypothesis as the opening premise of the box: | 2. (Ay.a+y=y+a) inductive hypothesis | Goal: (Ay.a'+y=y+a') | | 3. b=b arbitrary object intro | | Goal: a'+b = b+a' We attempt an informal proof of this: b+a' = (by axiom 4) (b+a)' = (by ind hyp and univ. elim.) (a+b)' = (by ???) a'+b We have no axiom or theorem which would allow us to show directly that (a+b)' = a'+b, but we should suspect that this is always true! So we set out to prove it by induction. Goal: (Axy.(x+y)' = x'+y) We attempt to prove this by induction on x: Basis Step: (Ay.(0+y)'=0'+y) But we can't easily do this. Informally, (0+y)' = (by line 1, univ. elim.) y' = (by theorem 1) y+1 = (by definition of 1) y+0' but there is no easy way to get to 0'+y (actually, there's an easy induction proof, but this seems excessive, and we would probably also have trouble in the induction step.) Thus, we try induction on y: Goal: (Ayx.(x+y)' = x'+y) Note the switch of leading variable. Goal (basis step): (Ax.(x+0)' = x'+0) | 1. c=c arbitrary object intro | Goal: (c+0)'=c'+0 | 2. (c+0)' = c' axiom 3, univ. elim, prop = | 3. c' = c'+0 axiom 3, univ, elim. | 4. (c+0)' = c'+0 transitivity of =, lines 2,3 5. (Ax.(x+0)' = x'+0) univ. intro. lines 1-4 | 6. (Ax.(x+d)' = x'+d) inductive hypothesis | Goal: (Ax.(x+d')' = x'+d') (replace d with d' in ind hyp) | | 7. e = e arbitrary object intro | | Goal: (e+d')' = e'+d' | | 8. e'+d' = (e'+d)' axiom 4, univ. elim | | 9. (e'+d)' = ((e+d)')' ind hyp (line 6), univ. elim, prop = | | 10. ((e+d)')' = (e+d')' axiom 4, univ. elim, prop = | | 11. (e+d')' = e'+d' symm., trans. =, lines 8-10 | 12. (Ax.(x+d')' = x'+d') univ. intro. lines 7-11 13. (Ayx.(x+y)' = x'+y) math induction, 5, 6-12 14. (Axy.(x+y)' = x'+y) universal quantifier switching, line 13 So we have proved a Lemma: (Axy.(x+y)' = x'+y) We present this as the proof of a separate Lemma, which we will reference by name in the main proof. The proof could have been embedded in the main proof, though it really could not be inserted into the middle of the box which begins on line 2; it would have to have been inserted earlier. We restate the beginning of the main proof: Top Level Goal: (Axy.x+y=y+x) Goal (basis step): (Ay.0+y=y+0) 1. (Ay.0+y=y+0) proved in previous section! We open a box to complete the proof by math induction, with the inductive hypothesis as the opening premise of the box: | 2. (Ay.a+y=y+a) inductive hypothesis | Goal: (Ay.a'+y=y+a') | | 3. b=b arbitrary object intro | | Goal: a'+b = b+a' | | 4. b+a' = (b+a)' axiom 4, univ elim | | 5. (b+a)' = (a+b)' ind hyp (line 2), univ. elim, prop = | | 6. (a+b)' = a'+b Lemma, univ. elim. | | 7. a'+b = b+a' symm, trans =, lines 4-6 | 8. (Ay.a'+y=y+a') univ. intro. lines 3-7 9. (Axy.x+y=y+x) math. ind. lines 1, 2-8. This proof is quite convoluted! It is worth noting that the convolutions found in this proof are quite representative of the kinds of situations which arise in ``real-life'' induction proofs where you have more information. The need to choose the variable on which to do the induction (arising in the Lemma) and the need to prove subgoals in an induction proof by induction themselves are features of induction proofs at every level.