(continuing proof of theorem at end of April 10 notes) Induction step: (Am.m ~=~ n -> m = n) -> (Am.m ~=~ n'-> m = n') Assume (Am.m ~=~ n -> m = n) for a fixed n (this is our inductive hypothesis). Our goal is to prove (Am.m ~=~ n'-> m = n'). Let m be arbitrary. Assume m ~=~ n'. Thus, we can choose a bijection (m,f,n'). n' = n U {n}. Since f is a bijection, so target covering and target constricted, there is a unique x E m such that f(x) = n. Observe that ((m-{x}),f-{(x,n)},n'-{n}) is a bijection, and moreover that n'-{n} = n. So we have a bijection between m-{x} and n. By our formal theory of arithmetic (and the fact that m =/= 0 by the basis step) there is a unique natural number p such that p' = m. We claim that p ~=~ m-{x}; the bijection is the identity map on p if x = p and otherwise is the map which sends x to p and fixes all other elements of p. So we have p ~=~ m-{x} ~=~ n, which means, by the Claim of transitivity of ~=~ above and the inductive hypothesis that p = n and so that m = p' = n' which is our goal. The proof of the induction step is complete. Notice that we are free to use theorems of our formal arithmetic which follow from axioms we have verified. There was a lot of ``sales resistance'' with this proof, so I have added some facts about bijections and a reexamination of the crucial step p ~=~ m - {x} below. Some clarifications which might help with the proof of the theorem (m ~=~ n -> m = n): it would have helped if we had proved a couple of extra results about bijections. The notions introduced here are also independently important facts about functions!!! Definition: If (A,f,B) is a function, and C c= A, we define the restriction of f to A as the triple (C,f |\ C,B), where f |\ C is defined as f ^ (C x B). (^ is typewriter notation for intersection). Theorem: If (A,f,B) is a function from A to B, and C c= A, then (C,f|\ A,B) is a function from C to B. Proof: (C,f |\ C,B) is a relation from C to B; it is clear that f |\ A is a subset of C x B, because it is defined as an intersection with that set. We need to show that (C,f |\ C,B) is source covering and source constricted. For any x in C, there is a y in B such that y = f(x) because f is a function. The pair (x,y) belongs to C x B, so it still belongs to f |\ A, establishing that for every x in C there is y in B such that x (f |\ A) y. (we have to use f |\ A as a relation rather than a function until we have shown that it is a function!). Now suppose that x and y belong to B, that z belongs to A, and that z (f|\A) x and z (f|\A) y. It follows that x = f(z) and y = f(z), so x = y (since f is a function!). Definition: If (A,f,B) is a function and C c= A, we define f[C] (the image of f under C) as {y E B : (Ex E C.y = f(x))}. Definition: We can now distinguish between codomain and range: the codomain of (A,f,B) is B, while the range is f[A] (a possibly proper subset of B). Functions for which these two concepts coincide are surjections. Theorem: For any function (A,f,B), the triple (A,f,f[A]) is a function and a surjection. Proof: We need to show that f c= A x f[A], to verify that this triple is a relation from A to f[A]. Any element of f will be an ordered pair (x,y) with x E A and y E B. But notice that we will have y E f[A]: it will be true that for some x in A (the given x), y = f(x). So any element of f belongs to A x f[A], which establishes that (A,f,f[A]) is a relation from A to f[A]. We need to show that (A,f,f[A]) is source covering and source constricted. This is obvious; for each x in A there is one and only one y in B such that (x,y) E f (this is what it means for (A,f,B) to be a function) , and this y is also in f[A], so it is also the case that for each x in A there is one and only one y in f[A] such that (x,y) E f, which is what needs to be shown. (A,f,f[A]) is a surjection because for each y in f[A] there is x in A such that y = f(x), by definition of f[A]. Theorem: If (A,f,B) is a bijection and C c= A, then (C,f|\A,f[C]) is a bijection. Proof: left as an exercise. Theorem: If (A,f,B) and (C,g,D) are bijections, and A ^ C = {} and B ^ D = {} (the respective domains and codomains are disjoint) then (A U B,f U g,B U D) is a bijection. Proof: left as an exercise. Definition: we define the identity map on any set A as (A,ID(A),A), where ID(A) = {(x,x) : x E A}. We leave it as an exercise to show that (A,ID(A),A) is a bijection. We now make some additional remarks on the proof of the induction step of the theorem ``m ~=~ n -> m = n''. Showing that there is a bijection from p to m - {x} can perhaps be organized better using these theorems. Recall from the context there that m =/= 0, x E m, p' = p U {p} = m. Either x = p, in which case m - {x} = p and the two sets are the same, so the identity map on p works as the bijection, or x =/= p, in which case we proceed as follows: (p-{x}, ID(p-{x}) , p-{x}) is a bijection, ({x}, {(x,p)}, {p}) is a bijection, their respective domains and codomains are disjoint, so the Theorem proved just above shows that ((p-{x}) U {x} , ID(p-{x}) U {(x,p)} , (p-{x}) U {p}) = (p, ID(p-{x}) U {(x,p)}, m-{x}) is a bijection. Then we consider that since (m,f,n') is a bijection, (m-{x}, f|\(m-{x}, f[m-{x}]) will be a bijection by a theorem cited above. f[m-{x}] = n by choice of x (x was chosen so that f(x) = n). So we have m-{x} ~=~ n. Since ~=~ is transitive, we have p ~=~ n, and so p = n by ind hyp. I don't know if this really helps. Another part of the confusion is the difficulty of thinking about the roles of p as both a member and a subset of its successor m = p U {p}, and taking similar facts into account about n and n'. At the end of the hour, we introduced the definitions of addition and multiplication. Definition: If m and n are natural numbers, we define m+n as |(mx{0}) U (nx{1})| and m*n as |mxn|. This is the kind of definition where there is a theorem to be proved before the definition is really usable. It is necessary to prove that there really are natural numbers the same size as the set (mx{0}) U (nx{1}) and the set mxn, which amounts to proving that unions of finite sets are finite and cartesian products of finite sets are finite. (This is where we stopped on Tuesday).