Notes on the in-class conversation: It is important to remember two little mottoes: 1. A negative hypothesis can be used in two ways: one either uses it for disjunction elimination (disjunctive syllogism) or one uses it as part of a contradiction (in either neg. intro. or neg. elim.) 2. When in doubt as to how to prove a statement P, try proving ~~P. I PROMISE to include solutions to the first page of Homework 7 in the notes (after a decent interval to allow stragglers to turn it in). Induction, Continued I decided not to do the formal proof of Theorem 2 above (every nonzero number has a predecessor) but instead to go ahead and do the more natural proof of commutativity of addition. We got as far as proving the basis step on the 6th, and that's how much I'll write up here. Here I repeat myself from the part of the March 3 notes not covered in class: Since math induction is an important form of proof, we introduce a derived rule: 0 E P (Ax.x E P -> x' E P) --------------------- mathematical induction, set form (Ay.y E P) which will allow the omission of the tedious (and often rather long!) lines n+i+1 and n+i+2 or the following form without set notation: P[0/z] (Ax.P[x/z] -> P[x'/z]) ----------------------- mathematical induction, property form (Ay.P[y/z]) This is proved by replacing the set P in the set form with the set notation {x | P[x/z]} and appealing to the definition of set notation. Although we stated the math induction axiom in terms of sets, we will initially work with the property-based derived rule. We will come back to what induction has to say about sets when we talk about such things as the Least Number Principle. Always remember when we DO use set notation that (for the time being) sets are just aliases for predicates. There is a form of math induction with a box, which I now introduce (it was also discussed in the out-of-class portion of the March 3 notes): n. P[0/z] ??? (basis step proved) | n+1. P[a/z] subpremise (inductive hypothesis) | . | . | . | n+i. P[a'/z] ??? n+i+1. (Ax.P[x/z]) math induction, n, (n+i)-(n+i) where a does not occur outside the box. The reason that this works is that the box can be replaced by two boxes as follows: n. P[0/z] ??? (basis step proved) Goal: (Ax.P[x/z]->P[x'/z]) | n+(1/2). a=a arbitrary object intro | Goal: P[a/z] -> P[x'z] | | n+1. P[a/z] subpremise (inductive hypothesis) | | . | | . | | . | | n+i. P[a'/z] ??? | n+i+1. P[a/z]->P[a'/z] imp. intro. lines (n+1)-(n+i) n+i+1. (Ax.P[x/z]->P[x'/z]) univ. intro. lines (n+(1/2))-n+i+1 n+i+2 (Ay.P[y/z]) math induction (property form) lines n, n+i+1 We'll see both forms of the proof of the basis step of the commutative law. Now for the main event. Theorem 3: (Ax.(Ay.x+y = y+x)) Goal: (Ax.(Ay.x+y = y+x)) This breaks into two subgoals, the familiar basis step and induction step. Goal: (Ay.0+y=y+0) Goal: (Az.(Ay.z+y=y+z)->(Ay.z'+y=y+z')) It is important to recognize that the induction axiom, unlike the basic rules of the propositional and predicate logic, introduces subgoals which are actually more complex than the statment to be proved. This is a reason for the mathematical power of this axiom, but of course it also makes proofs using it more complex... The rest of the notes for Monday are occupied by the proof of the basis step: Goal: (Ay.0+y=y+0) We prove this goal by induction as well! Goal (basis step): 0+0=0+0 1. 0+0=0+0 (properties of equality) We will relax our formality in certain respects as we go on. One feature is that we avoid explicit reference to the equality rules where possible. Goal (induction step): (Az.0+z=z+0 -> 0+z'=z'+0) We open a box for univ. intro. | 2. a=a arbitrary object intro | Goal: 0+a=a+0 -> 0+a'=a'+0 We open a box for imp. intro. | | 3. 0+a=a+0 subpremise | | Goal: 0+a' = a'+0 | | 4. 0+a' = (0+a)' axiom 4, univ. elim. | | 5. 0+a = (a+0)' line 3, prop = | | 6. 0+a = a' axiom 3, univ. elim., line 5, prop = The justification here allows us to eliminate the ``obvious'' line a+0 = a (an instance of axiom 3) and an application of equality elimination using the omitted line and line 5. | | 7. 0+a = a'+0 axiom 3, univ. elim., line 6, prop = Similar to the previous line. We are now done. | 8. 0+a=a+0 -> 0+a'=a'+0 imp. elim. lines 3-7 9. (Az.0+z=z+0 -> 0+z'=z'+0) univ. intro. lines 2-8 10. (Ay.0+y=y+0) math. induction (property form) lines 1,9 Here we have not used the form of the math induction rule with a box described above. We demonstrate how the proof can be abbreviated: Goal: (Ay.0+y=y+0) We prove this goal by induction as well! Goal (basis step): 0+0=0+0 1. 0+0=0+0 (properties of equality) We open a box for the induction step (a casualty of abbreviation is that this proof has no line 2). | 3. 0+a=a+0 inductive hypothesis | Goal: 0+a' = a'+0 | 4. 0+a' = (0+a)' axiom 4, univ. elim. | 5. 0+a = (a+0)' line 3, prop = | 6. 0+a = a' axiom 3, univ. elim., line 5, prop = | 7. 0+a = a'+0 axiom 3, univ. elim., line 6, prop = which is our goal. 10. (Ay.0+y=y+0) math. induction lines 1,3-7. This is clearly more economical, and we should be able to see from the more verbose proof above why this form of proof is valid.