TEXT   63

transfinite.txt

Guest on 2nd September 2021 02:07:10 AM

  1. 0. our old friend "nat"
  2. -----------------------
  3.  
  4. Over the natural numbers (nat) we have the < ordering relation.  It has
  5. the well-ordered property:
  6.  
  7.   a non-empty subset of nat has a minimal member, i.e.,
  8.  
  9.   forall P:nat->bool.     (exist x. Px)
  10.                       ==> (exist m. Pm /\ ~(exist y. Py /\ y<m)) , i.e.,
  11.  
  12.   forall P:nat->bool.     (exist x. Px)
  13.                       ==> (exist m. Pm /\ ~(exist y<m. Py))
  14.  
  15. and strong induction:
  16.  
  17.   to prove Q true for all natural numbers, it suffices to:
  18.   for an arbitrary m,
  19.     assume Q true for all numbers < m, prove Q true for m.
  20.  
  21.   forall Q:nat->bool.     (forall x. Qx)
  22.                       <== (forall m.
  23.                               (forall y<m. Qy) ==> Qm)
  24.  
  25. (Exercise: Let "Waldo" = "the base case" = Q0. Where is Waldo?)
  26.  
  27. They are equivalent:
  28.  
  29.    forall P. (exist x. Px) ==> (exist m. Pm /\ ~(exist y<m. Py))
  30. =    <contrapose>
  31.    forall P. ~(exist x. Px) <== ~(exist m. Pm /\ ~(exist y<m. Py))
  32. =    <de Morgan>
  33.    forall P. (forall x. ~Px) <== (forall m. ~Pm \/ ~(forall y<m. ~Py))
  34. =    <material implication>
  35.    forall P. (forall x. ~Px) <== (forall m. (forall y<m. ~Py) ==> ~Pm))
  36. =    <change of variable: Q = ~P>
  37.    forall Q. (forall x. Qx) <== (forall m. (forall y<m. Qy) ==> Qm))
  38.  
  39.  
  40. 1. new friends
  41. --------------
  42.  
  43. In the above equivalence we never used the "nat"ness of nat.
  44. (Actually we never used transitivity or dichotomy of < either.)
  45. We may as well replace nat by some other set, impose a < ordering,
  46. and make sure < has the well-ordering property; then induction has
  47. to work.
  48.  
  49. Example. Pull, out of thin air, a new symbolic constant w (omega);
  50.          amend < so that n<w for all n:nat.  Then the set
  51.            nat U {w} = {0, 1, 2, ... (all the natural numbers),
  52.                         w}
  53.          together with < is well-ordered.
  54.  
  55.          Hehner and ACL2 write this more concretely as the set of tuples
  56.            {(0,0), (0,1), (0,2), ... (0,n), ... ,
  57.             (1,0)}
  58.          together with the lexicographical ordering:
  59.              (x0,x1)<(y0,y1) == x0<y0 \/ (x0=y0 /\ x1<y1)
  60.  
  61. This set is "larger" than nat.  This is not in the sense of
  62. cardinality (in fact the map w|->0, 0|->1, 1|->2, ... is 1-1 onto),
  63. but that no 1-1 onto map preserves the order (in fact w|->0 already
  64. breaks the order).
  65.  
  66. There is a 1-1 order-preserving map from nat to nat U {w}.  There
  67. is no 1-1 order-preserving map the other way round.  In this sense
  68. nat is "smaller" and natU{w} is "larger".
  69.  
  70. Example. {(0,0), (0,1), (0,2), ... ,
  71.           (1,0), (1,1), (1,2), ... ,
  72.           (2,0), (2,1), (2,2), ... ,
  73.           ...
  74.          } again using the lexicographical ordering.
  75.  
  76.          In "w" notation:
  77.          {0, 1, 2, ... ,
  78.           w, w+1, w+2, ...,
  79.           w+w, w+w+1, w+w+2, ... ,
  80.           ...
  81.          }
  82.  
  83. Transfinite induction simply refers to performing induction over some
  84. well-ordered set larger than nat.
  85.  
  86. In a well-ordered set, a member m falls into one of three cases:
  87.  
  88. - m is the minimum, e.g. 0;
  89. - m is the successsor of someone else, e.g., 1, 2, 3, ...
  90.   we call these "successors";
  91. - m is not the successor of someone else, nonetheless it is bigger than
  92.   a whole lot of other members; e.g., w, w+w, ...
  93.   we call these "limits"
  94.  
  95. so the proof obligation of induction, (forall y<m. Qy) ==> Qm, can also
  96. take on three forms:
  97.  
  98. - m is 0: Q0
  99. - m is a successor, say m=n+1: Qn ==> Q(n+1)
  100.   for pretty much the same reason "weak induction" equivales "strong induction"
  101. - m is a limit: no change, (forall y<m. Qy) ==> Qm
  102.  
  103. So in many treatises, transfinite induction is re-stated as:
  104.  
  105.   (forall x. Qx) <==    Q0
  106.                      /\ forall n. Qn ==> Q(n+1)
  107.                      /\ forall limit m. (forall y<m. Qy) ==> Qm
  108.  
  109. it is convenient in practice because usually the three cases do
  110. require three conceptually different proofs.
  111.  
  112.  
  113. 2. ordinals
  114. -----------
  115.  
  116. {0, 1, 2, ... , w}
  117.  
  118. and
  119.  
  120. {(0,0), (0,1), (0,2), ... , (1,0)}
  121.  
  122. are order-isomorphic to each other.  Their members seem to use different
  123. naming schemes, but that's the end of the difference.  We may as well
  124. pick one of them and call it "canonical", "representative", etc.
  125.  
  126. An ordinal is a "canonical" well-ordered set.
  127.  
  128. We impose these requirements on our canonical choice to obtain nice
  129. properties:
  130.  
  131. - ordinals are built bottom-up: from smaller ordinals we define
  132.   larger ordinals
  133. - an ordinal x, being a well-ordered set, has elements; each element
  134.   is in turn an ordinal smaller than x
  135. - in fact x = { those ordinals smaller than x }
  136. - natural numbers are recasted as ordinals, so that ordinals become
  137.   a generalization of natural numbers
  138.  
  139. Thus we re-build natural numbers and build ordinals this way (due to
  140. von Neumann):
  141.  
  142. 0 := the empty set
  143. 1 := {0} = 0 U {0}
  144. 2 := {0, 1} = 1 U {1}
  145. ...
  146. n+1 := {0, 1, ... , n} = n U {n}
  147. ...
  148.  
  149. w := nat = {0, 1, ... }  this is the first limit ordinal
  150. w+1 := {0, 1, ... , w} = w U {w}
  151. ...
  152.  
  153. w+w := {0, 1, ... , w, w+1, ... }  this is the second limit ordinal
  154. ...
  155.  
  156. In general, there is 0, there are successor ordinals x+1 = x U {x}
  157. such as 1 and w+1, and there are limit ordinals (non-successors) such
  158. as w and w+w.
  159.  
  160. The nice thing about the above requirements and construction is this
  161. equivalence:
  162.  
  163.    x smaller than y (has 1-1 order-preserving map from x to y)
  164. == x member of y
  165. == x subset of y
  166.  
  167. thus many different notions of "smaller/larger" are unified.
  168. We can just write x<y without misunderstanding.
  169.  
  170. Transfinite induction is therefore induction performed over ordinals
  171. (or sometimes one large ordinal --- which is a set of many ordinals
  172. anyway).  Again, for convenience we often split the induction step
  173. into the 0 base case, the successor ordinal case, and the limit
  174. ordinal case.
  175.  
  176.  
  177. 3. recursion
  178. ------------
  179.  
  180. Wherever there is induction, there is recursion.
  181.  
  182. Let x be an ordinal and S a set.  It is legal to define a function
  183. f:x->S this way:
  184.  
  185. f0 = whatever you like
  186. f(y+1) = expression involving fy
  187. fz = expression involving ft's where the t's are < z
  188.  
  189. Example. Let S be a complete lattice, h:S->S a monotonic function.
  190. Define f by
  191.   f0 = bottom
  192.   f(y+1) = h(fy)
  193.   fz = Join t<z. ft
  194. Then there is a large enough ordinal x such that fx = least fixpoint of h.

Raw Paste


Login or Register to edit or fork this paste. It's free.