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.