next up previous
Next: Wednesday, March 15 Up: Lecture Notes Previous: Monday, March 13, 2000

Tuesday, March 14, 2000

My xor introduction rule as originally reported in the notes is wrong.
See corrected version (Feb 4 notes).  This also means that the two
missing xor elimination rules are _really_ needed (Feb. 11 notes).

It's probably better to break a goal P <+> Q into two implications thus:

Goal:  P <+> Q

Goal 1:  P -> ~Q  (or the contrapositive Q -> ~P)

Goal 2:  ~Q -> P  (or the contrapositive ~P -> Q)

(this is Grantham's approach, I think).

Also, the first occurrence of axiom 6 in the notes was wrong (the second
occurrence is correct):

6. (Axy. xy' = xy + x)

is the correct form of the axiom (as common sense would dictate).

Notes for the proof done in class follow, supplied by a student (with some
editing):

Holmes adds:  note that indentation is used to indicate boxes.

*******************************************************************************
M387

These are the notes for class on 03/14/00

A proof was undertaken at the blackboard:

Prove (Axy. xy = yx)

*******************************************************************************

            Goal: Axy. x*y = y*x

            Goal: Induction basis step (Ax. x*0 = 0*x)
            1.    0*0 = 0*0             prop =

               Goal: Induction step (a'*0 = 0*a')
                  2.    a*0 = 0*a       induction hypothesis

Holmes adds:  the goal is now a'*0 = 0*a'

                  3.    a'*0 = a'*0     prop. equality
                  4.    a'*0 = 0        axiom 5
                  5.    0*a' = 0*a+0    axiom 6
                  6.    0*a' = 0*a      axiom 3, prop. equality
                  7.    0*a' = a*0      ind. hyp., prop. equality
                  8.    0*a' = 0        line 7, axiom 5
                  9.    a'*0 = 0*a'     prop. equality, lines 4,8
            10.   Ax. x*0 = 0*x   induction lines 1,2-9

                Goal: Induction step (Ax. xa' = a'x)
                 11.   Ax. xa = ax     induction hypothesis

                  
                      12.   b = b           arb. obj. intro
                      Goal:  ba' = a'b
                      13.   ba' = ba + b     axiom 6
                      14.   ba  = ab         univ. elim. line11
                      15.   ba' = ab + b     lines 13, 14 prop =

At this point, the need for a Lemma was determined for justification
of the equality of the right side of line 15 (ab + b) with the desired
target a'b.

Dr. Holmes made note of the fact that for use of axioms 5 & 6 that annotation
for or recognition of the use of universal elimination is required.

Dr. Holmes himself adds:  I said that this is formally required, but
since when ax 5, 6 (or most of the other axioms) are used we always
have this use of univ. elim, it seems redundant to mention it; I 
officially allow it to be omitted.



         LEMMA

              Goal: (Axy. xy+y = x'y)

	      Holmes:  I made the bound variables here the familiar x,y
              rather than z,a as in the class discussion.

                Goal: Induction basis step (Ax. (x*0)+0 = x'*0)

	            L0.   c=c                 arbitrary object intro
                    L1.   c*0+0 = c*0         axiom 3

                    Holmes:  the goal is now c*0 + 0 = c'*0

                    L2.   c'*0 = 0            axiom 5
                    L3.   c*0 = 0             axiom 5
                    L4.   (c*0)+0 = c'*0      prop. equal. 2x, lines1,2,3
               L5.   Ax.(x*0)+0 = x'*0   univ. intro. lines 0-4

                Goal: Induction step Ax.(xa')+a' = x'a'
                    L6.   Ax. (xa)+a = x'a        induction hypothesis
                         L7.   c = c                   arb. obj. intro

                         Holmes:  the goal is now (c*a')+a' = c'*a'

                         L8.   (ca)+a = c'a            univ. elim. line6
                         L9.   (ca')+a = ((ca')+a)'    axiom 4
                         L10.

Here is where the class ended.

Holmes completes the proof in the same format, following the proof
of March 15 in class, and starting over at L8.

                         L8.   (c*a')+a' = (c*a+c)+a'   ax. 6, prop =
                         L9.   (c*a')+a' = (c*a+a')+c   comm, assoc +,prop =
                         L10.  (c*a')+a' = (c*a+a)'+c   ax. 4, prop =
                         L11.  (c*a')+a' = (c'*a)'+c    
                                 ind hyp(line 6), univ. elim., prop =
                         L12.  (c*a')+a' = c'*a + c' 
                                 lemma in proof of comm +, ax. 4, prop =
                         L13.  (c*a')+a' = c'*a'        ax. 6, prop =
                    L14.  (Ax. (xa')+a' = x'a)          univ. intro. L7-L13
               L15. The Lemma                           math. ind. L5,L6-14  

I reproduce the induction step of the main proof so far:

                Goal: Induction step (Ax. xa' = a'x)
                 11.   Ax. xa = ax     induction hypothesis

                  
                      12.   b = b           arb. obj. intro
                      Goal:  ba' = a'b
                      13.   ba' = ba + b     axiom 6
                      14.   ba  = ab         univ. elim. line11
                      15.   ba' = ab + b     lines 13, 14 prop =
                      16.   ba' = a'b        Lemma, univ. elim., prop =
                 17. (Ax. xa' = a'x)         univ. intro. 12-16
            18.  The Theorem                 math. ind. line 10, lines 11-17



Randall Holmes
2000-05-05