version of this book
In set theory there is only induction up to an ordinal. One cannot use inductions up to an ordinal to recursively construct a new object. One can perform recursive operations on a functional that is a notation for an ordinal to construct a new functional that represents the result of set theory style induction. The sequences of parameters this new functional accepts and the operations performed on those parameters can mirror the structure obtained from set theory style induction.
For example one can recursively define an ordinal function on recursive ordinal notations, , as a functional that outputs a notation for the successor of x. The notation generated is a function on the integers that outputs a notation for the nth successor to x for integer input n.
In set theory one can do the same operation at any limit ordinal because the elements in that limit (and their union) are each sets. In a recursive functional hierarchy the type of limit determines the nature of the operation. If the ordinal type is that of the integers then one typically constructs a functional on the integers that iterates some process up to the value of the integer parameter. If the type is that of recursive ordinal then one defines a functional that does different operations for 0, a successor ordinal and a limit ordinal. The next level in the hierarchy of limit types is that of a functional well founded for notations for recursive ordinals. Recursive ordinals can be thought of as providing schemes for constructing functions on the integers through integration and diagonalization. Functional well founded for recursive ordinals provide similar schemes for iterating the construction of recursive ordinals. A limit type of all such objects is typically a process for doing induction on such schemes.
We can iterate the notion of a limit type that is well founded for a lower limit type. We can iterate this up to any ordinal structure we define. At this point we have exhausted the notion of ordinal in recursive functional hierarchies. The next step in set theory is all ordinals definable in this way but that set is the set of all countable ordinals. This would take us outside the domain of recursive processes in a potentially infinite universe. Instead we need to generalize the notion of ordinal to allow induction on all objects of this class without resorting to uncountable structures. It is at this point that we must part from set theory style definitions.
version of this book