2023-04-30

264: For Transfinite Recursion Theorem, Some Conditions with Which Partial Specifications of Formula Are Sufficient

<The previous article in this series | The table of contents of this series | The next article in this series>

A description/proof of for transfinite recursion theorem, some conditions with which partial specifications of formula are sufficient

Topics


About: set

The table of contents of this article


Starting Context



Target Context


  • The reader will have a description and a proof of for the transfinite recursion theorem, some conditions with which partial specifications of the formula are sufficient.

Orientation


There is a list of definitions discussed so far in this site.

There is a list of propositions discussed so far in this site.


Main Body


1: Note 1


For the transfinite recursion theorem, a formula, \(\gamma (f, v)\), which determines a unique \(v\) for any function from any subset of a well-ordered set, \(S\), is required (in a version I have seen in a text book, \(\gamma\) has to be able to take any function, \(f\), but 'any function from any subset of \(S\)' should be enough, because the target function, \(f'\), is \(f': S \rightarrow S'\), where \(S'\) is unknown, that satisfies \(\gamma (f'\vert_{seg \text{ }s}, f' (s))\), and the specifications for the functions that are not from any subset of \(S\) should not matter). Note there that as \(S'\) is not predetermined, \(\gamma\) has to deal with any \(f\) that maps from any subset of \(S\) into any set, because we do not know where \(f'\) maps into.

But the problem is the text book begins to use the theorem with only a part of \(\gamma\) specified, specifically, a part that concerns only the functions into a predetermined \(S''\), and concludes that the target function, \(f'\), is a function into \(S''\), . . ., is that OK? I mean, while there should be surreptitious specifications for functions that are into \(S'''\), \(S''''\), etc., why \(f'\) is guaranteed to be a function into \(S''\) just because the author cited only the specific part? . . . It should be because the specific part satisfies a condition that guarantees that only the part matters.

Intuitively speaking, if the part maps the function whose domain is the empty set into \(S''\), \(f' (m)\) where \(m\) is the least element of \(S\) is in \(S''\), because \(\gamma (f'\vert_{seg \text{ }m} = f'\vert_\emptyset, f' (m))\), and \(f' (s)\) for any larger \(s\) seems to keep being in \(S''\), by virtue of \(\gamma (f'\vert_{seg \text{ }s}, f' (s))\), because the next least element, \(s'\), satisfies \(\gamma (f'\vert_{seg \text{ }s'} = f'\vert_{\{m\}}, f' (s'))\), but \(f'\vert_{\{m\}}\) is into \(S''\) as the only value is \(f' (m) \in S''\), and so on, but of course, that is not a rigid proof.


2: Description 1


For the transfinite recursion theorem, if a part of the specification for the formula, \(\gamma\), includes all the functions each of which maps any subset of the well-ordered set, \(S\), into a predetermined set, \(S''\), and the function from the empty set (inevitably into the empty set), which (the function) is really the empty set, and \(\gamma\) maps the function from the empty set into \(S''\), then, only the part does matter as the specification of \(\gamma\), and the target function, \(f'\), maps into \(S''\).


3: Proof 1


In a proof of the transfinite recursion theorem, \(f'\) is the union of the approximating functions, each of which is a function, \(f_t\), from a subset of \(S\), \(T := \{s \in S\vert s \leq t\}\), into any set, such that for any \(s \le t\), \(\gamma (f_t\vert_{seg \text{ }s}, f_t (s))\). So, if every \(f_t\) is into \(S''\), \(f'\) will be into \(S''\).

\(T\) is canonically a well-ordered set, by the proposition that any subset of any well-ordered set is well-ordered with the restriction of the ordering. Let us define the subset of \(T\), \(T' := \{s \in T\vert f_t (s) \in S''\}\). We aim to prove that \(T' = T\), which means that \(f_t\) is into \(S''\), by the transfinite induction principle.

For any \(s\) such that \(seg \text{ }s \subseteq T'\), \(s \in T'\)? As \(f_t (seg \text{ }s) \subseteq S''\), \(f_t\vert_{seg \text{ }s}\) is a function into \(S''\), and it is included in the part of the specification, and \(f_t (s)\) is in \(S''\) by \(\gamma (f_t\vert_{seg \text{ }s}, f_t (s))\). So, \(s \in T'\). So, by the transfinite induction principle, \(T' = T\).

Only the part of the specification matters because any \(f_t\vert_{seg \text{ }s}\) is a function into \(S''\) and the rest of the specification does not play any role in for any \(f_t\) to be an approximating function or not.


4: Note 2


So, the specific part, instead of another surreptitious part that includes the functions into a \(S'''\), determines \(f'\) because the part includes the function from the empty set, which cannot be included in another part at the same time, because the function is a single function.


References


<The previous article in this series | The table of contents of this series | The next article in this series>