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. I made a list of additional theorems which we will ``believe'' henceforth (you may have the opportunity to prove one of these on the take-home exam). distributivity of multiplication over addition: (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)))