next up previous
Next: Wednesday, March 9, 2000 Up: Lecture Notes Previous: Monday, March 6, 2000

Tuesday, March 7, 2000

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.



Randall Holmes
2000-05-05