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