Next: Solutions to the Proofs Up: Lecture Notes Previous: Tuesday, March 14, 2000

## Wednesday, March 15

```Modifications to Homework 8 can be seen under Homework 8 on the web page.

A corrected version of these notes was handed out, fixing the error in
xor introduction which appeared in earlier versions.

We resumed the proof of commutativity of multiplication, but using
something closer to standard mathematical practice (and with me at the
board!).  I will try to reproduce the in-class proof as far as
possible in what follows.

henceforth (you may have the opportunity to prove one of these
on the take-home exam).

(Axy.(x+y)*z = x*z+y*z)

associativity of multiplication:

(Axyz.(x*y)*z=x*y(*z))

This essentially completes standard algebraic properties; there may
be minor ones that we haven't explicitly noted, but which are fairly
easy to prove:

1*x = (by comm *)
x*1 = (by def 1)
x*0' = (by ax 6)
x*0+x = (by ax 5)
0+x = (by comm + and ax 3)
x

for example.

We also will ``believe'' some additional properties of order:

(the universal closures of) ((x<=y) & (y<=x)) -> x=y

and (x<=y) | (y<=x)

which have as a corollary

For all x,y exactly one of the following is true:  x<y , x = y, y<x
(this is called the ``trichotomy'' property of order.)

There was a request for a complete handout of logical rules and
axioms and theorems available so far:  this will be made available
Friday or Monday.

There will be other chances for students to earn homework credit by
preparation of class notes as the semester goes on -- in fact, I should
have had someone take notes today!

The Commutativity of Multiplication

Theorem:  (Axy.x*y=y*x)

We prove this by induction on y.  It doesn't really matter which variable
we choose.

Basis step

Goal: (Ax.x*0=0*x)

I hate to say it, but this need to be proved by induction as well!
The proof will be indented so that the structure of the main proof
is clearer.

Basis step:  0*0 = 0*0

This is obvious.

Induction step:  Using the inductive hypothesis a*0 = 0*a
(on the board a was an alpha) prove the goal a'*0 = 0*a'

0*a' = (by ax. 6)
0*a + 0 = (by ax. 3)
0*a = (by ind hyp)
a*0 = (by ax. 5)
0 = (by ax. 5)
a'*0

Thus a'*0 = 0*a', which was our goal.

The proof by induction of the basis step of the main theorem is
complete.

Induction step (of main theorem):  Using the inductive hypothesis
(Ax.x*a=a*x), prove the goal (Ax.x*a'=a'*x)

Let x be arbitrary (this corresponds to opening a box for univ. intro.)

x*a' = (by ax. 6)
x*a+a = (by ind hyp)
a*x + a = (by ???)
a'*x

This would complete the proof if we had something to put in place of ???
We now provide this something in the form of a Lemma (which we will,
of course, prove by induction :-)

Lemma:  (Axy.x*y + y = x'*y)

We prove this by induction on y (one way to see that y is the right choice
is to observe that the basis step is very easy with y and rather less
obvious with x).

Basis step: (Ax.x*0 + 0 = x'*0)

Let x be arbitrary:  then x*0 + 0 = 0 = x'*0 by applications of axioms
3 and 5.

Induction step:  Assuming the inductive hypothesis (Ax.x*a + a = x'*a),
prove the goal (Ax.x*a'+a' = x'*a')

Let x be arbitrary.

x*a'+a' = (by ax. 6)
(x*a + x) + a' = (by regrouping with +)
(x*a + a') + x = (by ax. 4)
(x*a + a)' + x = (by ind hyp)
(x'*a)' + x = (by x+1 = x' and regrouping with +)
x'*a + x' = (by ax. 6)
x'*a'

Thus x*a'+a' = x'*a' as desired, and since x was chosen arbitrarily,
(Ax.x*a'+a' = x'*a') as desired.

The proof by induction of the Lemma is complete.

We repeat the

Induction step (of main theorem):  Using the inductive hypothesis
(Ax.x*a=a*x), prove the goal (Ax.x*a'=a'*x)

Let x be arbitrary (this corresponds to opening a box for univ. intro.)

x*a' = (by ax. 6)
x*a+a = (by ind hyp)
a*x + a = (by the Lemma proved above)
a'*x

Thus x*a' = a'*x as desired.  Since x was chosen arbitrarily, we have
proved (Ax.x*a' = a'*x) as desired.

The induction proof of the Theorem is complete.

A Theorem I will mention as a target is

(Axy.(Eqr.qx+r = y & (x = 0 | r < x)))
```

Randall Holmes
2000-05-05