next up previous
Next: Monday, April 17, 2000 Up: Lecture Notes Previous: Tuesday, April 11, 2000

Wednesday, April 12

There will be no class on Friday, April 14.  I will not be in town
on the 13th or 14th.

In class on Wednesday, we went through the theorems on bijections which
are given in the Tuesday notes.  We then went (a bit too hurriedly at the
end) through the proof of the following Theorem.  The exposition suffered
from the fact that the overall logical structure of the proof was not
clear in my mind:  this should be clarified here. 

Addition Theorem: for all natural numbers m and n, the following are true:

   i.  m+n exists (this means (Ep E N. p ~=~ (mx{0}) U (nx{1})))

   ii.  m+0 = m

   iii.  If m+n exists, m+n' = (m+n)' (which in combination with
         i means that m+n' = (m+n)' always holds).

The form of this proof presented some difficulties for me in class!
I will present it here as a proof of part (i) by mathematical induction
on n, with proofs of parts (ii) and (iii) appearing as ingredients of
the main proof.  Notice that the effect of this is to show that we
have correctly defined addition for the purposes of our formal arithmetic.

Basis step:  Our goal is to prove that m+0 exists.  It is clearly
   sufficient to prove (ii):  m+0 = m.

   m+0 is defined as |(mx{0}) U (0x{1})|.  |(mx{0}) U (0x{1})| = m
   is defined as meaning m ~=~ (mx{0}) U (0x{1}).  Observe that 0x{1}
   = {(y,z) : y E 0 & z = 1} is the empty set, since no y can belong to 0.
   Thus our goal simplifies to m ~=~ (mx{0}).

   We claim that (m, {(y,(y,0)) : y E m} , mx{0}) is a bijection
   from m to mx{0}, establishing that m ~=~ (mx{0}).  

   We define f = {(y,(y,0)) : y E m} for brevity.  It is obvious that
   f c= m x (mx{0}), so the triple is a relation from m to mx{0}.
   Further, f is source covering:  for any y in m, there is a corresponding
   (x,0) in mx{0}; moreover, it is source constricted:  for any x in m,
   there is only one corresponding (x,0) in mx{0}.  This shows that f
   is a function.  Further, f is target covering:  for any z in mx{0}
   = {(y,0) : y E m} there is a y such that z = (y,0) = f(y) (by definition
   of f).  Also, f is target restricted:  if f(y) = f(z), we have 
   (y,0) = (z,0), from which y = z by the basic property of ordered pairs.

Induction step:  Our inductive hypothesis is (Am E N.m+n exists).

   Our goal is to show that (Am.m+n' exists).

   Let m be arbitrary.

   It will be sufficient to prove (iii):  for any natural numbers
   m and n, if m+n exists, then m+n' = (m+n)'.  For our particular
   choices of m and n, we already have ``m+n exists'' by inductive hypothesis,
   so (iii) would allow us to conclude that m+n' is well-defined as
   the successor of m+n, completing the proof by induction of (i).

   The proof of (iii) now commences.  m+n' is defined as
   |(mx{0}) U (n' x {1})|.  We cite without proof the fact that
   (AxB) U C = (AxC) U (BxC) (you are welcome to prove this).
   From this, it follows that n'x{1} = (n U {n}) x {1} = (n x {1}) U
   ({n} x {1}) =  (n x {1}) U {(n,1)}.  Thus (mx{0}) U (n' x {1}) =
   (mx{0}) U (n x {1}) U {(n,1)}.

   By hypothesis, m+n exists.  This means that there is a bijection
   (m+n,f,(mx{0}) U (n x {1})).  ({m+n},{(m+n,(n,1))},{(n,1)}) is the
   unique bijection between the one-element sets {m+n} and {(n,1)}.
   The domains m+n and {m+n} are disjoint (m+n is the set of all
   natural numbers smaller than m+n).  The codomains (mx{0}) U (n x
   {1}) and {(n,1)} are disjoint (the pair (n,1) certainly does not
   belong to mx{0} (wrong second coordinate) and cannot belong to
   nx{1} because n does not belong to n).  This means that the
   coordinatewise ``union'' 

   (m+n U {m+n} , f U {(m+n,(n,1))} , (mx{0}) U (n x {1}) U {(n,1)})

   is a bijection by a theorem in yesterday's notes (introduced on the
   board today).  The domain m+n U {m+n} of this bijection is (m+n)'
   by definition of the successor and the codomain 
   (mx{0}) U (n x {1}) U {(n,1)} has already been shown to be 
   equal to (mx{0}) U (n' x {1}).  So we have shown that 
   if m+n exists, (m+n)' ~=~ (mx{0}) U (n' x {1}), which implies
   that (m+n)' = |(mx{0}) U (n' x {1})| = m+n', which was what we
   needed to prove.  We have seen above that (iii), which we have
   just established, is what is needed to complete the proof of

   The proof is complete.

Randall Holmes