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