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