Fruitful and helpful ordinal functions (Q953278)

This article is part of a project of the author to develop proof-theoretically strong ordinal notation systems from below. This is different from the standard approach, in which ordinal notations are defined using collapsing functions, and therefore denotations for ordinals refer to bigger ordinals than the ordinal denoted. A different approach towards ordinal notation systems from below has been taken by the reviewer in [``Ordinal systems'', in: S.~B. Cooper et al. (eds.), Sets and proofs. Invited papers from the Logic colloquium '97, European meeting of the Association for Symbolic Logic, Leeds, UK, July 6--13, 1997. Cambridge: Cambridge University Press. Lond. Math. Soc. Lect. Note Ser. 258, 301--338 (1999; Zbl 0944.03054); ``Ordinal systems. II: One inaccessible'', in: S.~R. Buss et al. (eds.), Logic colloquium '98. Proceedings of the annual European summer meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9--15, 1998. Natick, MA: A K Peters, Ltd. Lect. Notes Log. 13, 426--448 (2000; Zbl 0951.03051)]. In a previous article, \textit{H. Simmons} [Arch. Math. Logic 43, No. 1, 65--83 (2004; Zbl 1067.03063)] introduced his basic approach, but there were some gaps which are now worked out very carefully in this article. The approach taken by the author is to use higher-type ordinal functions. Let \(\mathbb O{\text{rd}}^{(0 )} := \mathbb O{\text{rd}} \), \(\mathbb O{\text{rd}}^{(n+1)} := \mathbb O{\text{rd}}^{(n)} \rightarrow \mathbb O{\text{rd}}^{(n)}\), where \(\mathbb O{\text{rd}}\) denotes the set of countable ordinals. Instead of using the normal functions as in the approach by Veblen, the author uses the interplay of two kinds of functions: fruitful and helpful functions. Fruitful functions are (weakly) inflationary, (weakly) monotone and continuous (note that normal functions are strictly monotone and continuous). In addition the author demands that they are big, i.e., \(\forall \alpha > 0.f\;\alpha \geq \omega^\alpha\). Big normal functions are fruitful. Fruitful functions can be used in the \(\omega\)-step of the Veblen hierarchy. In the Veblen hierarchy, \(\varphi_\omega\) is formed by first forming \(f:= \sup_{n < \omega} \varphi_n\), and then forming the fixed points of \(f\). In the approach by the author, this step is divided into two steps: first \(f\) is formed, which is a fruitful function, and then the fixed points of \(f\) are formed, which is the same step as the step from \(\varphi_n\) to \(\varphi_{n+1}\). The second set of ordinal functions introduced by the author are the helpful functions, which are strictly inflationary, (weakly) monotone and strictly big. Here, strictly big means that \(f(\alpha)\) is strongly critical. Helpful functions can be used in the step from \(\varphi_n\) to \(\varphi_{n+1}\): Let \(\mathbf{Fix} : \mathbb O{\text{rd}}^{(2)}\), \(\mathbf{Fix}\;f\;\alpha := f^\omega\;(\alpha + 1)\), and \(\mathbf{Enm} : \mathbb O{\text{rd}}^{(2)}\), \(\mathbf{Enm}\;h\;\alpha := h^{1+\alpha}\;0\). \(\mathbf{Fix}\) maps fruitful functions to helpful functions, \(\mathbf{Fix}\;f\;\alpha\) is the next fixed point of \(f\) above \(\alpha\), and \(\mathbf{Enm}\) maps helpful functions to fruitful functions. \(\mathbf{Enm}\;(\mathbf{Fix}\;f)\) enumerates the fixed points of \(f\), and therefore \(\varphi_{n+1} = \mathbf{Enm}\;(\mathbf{Fix}\;\varphi_n)\). In order to analyse his classes of ordinal functions, the author introduces the notion of a smooth class of higher ordinal functions: a class is smooth if it is closed under composition and pointwise countable suprema, where pointwise suprema on \(\mathbb O{\text{rd}}^{(l)}\) are introduced. It follows that if \(f\) is an element of a smooth class, so is \(f^\alpha\) for \(\alpha > 0\). The author shows that the classes of helpful and of fruitful functions are both smooth. The author shows that \(\mathbf{Next}:= \mathbf{Fix}\;(\lambda \alpha .\omega^\alpha )\) is the smallest helpful function. Then he defines functions \([l]: \mathbb O{\text{rd}}^{(l+2)}\), \([l]\;h\;\mathbf{h} = \mathbf{Fix}\;(\lambda \alpha.h^\alpha\;\mathbf{h}\;0)\), and shows that \([l]\) is helpful. Then the author introduces the Veblen hierarchy: Let \(\mathbf{Veb} : \mathbb O{\text{rd}}^{(2)}\), \(\mathbf{Veb} := \mathbf{Enm} \circ \mathbf{Fix} \). The Veblen hierarchy over a given initial function \(f\) can be defined by \(\varphi[f]\;0 := f\), \(\varphi[f]\;(1 + \alpha) := \mathbf{Veb}^{\alpha+1}\;f\). Next, the author introduces \(\Uparrow\;f:= \lambda \alpha .\varphi[f]\;(1+\alpha)\;0\). Let \(f= \lambda \alpha.\omega^\alpha \). Then the fixed points of \(\Uparrow\;f\) are the \(\Gamma\)-numbers. We have \(\mathbf{Fix}\;(\Uparrow\;f) = [1]\;[0]\;(\mathbf{Fix}\;f)\), and \(\Gamma_0 = [1]\;[0]\;\mathbf{Next}\;\omega\). The author claims (without a full proof) that \([2]\;[1]\;[0]\;\mathbf{Next}\;\omega\) is the Ackermann ordinal. Finally, the author introduces \(\Delta[0]:= \omega\), \(\Delta[1]:= \mathbf{Next}\;\omega (= \epsilon_0)\), \(\Delta[n+2]:= [n]\;[n-1]\; \cdots \;[0]\;\mathbf{Next} \;\omega\). The author conjectures that \(\sup_{n < \omega }\Delta[n]\) is the Bachmann-Howard ordinal. This is an interesting approach towards ordinal notation systems from below. The article is very clearly written and I enjoyed reading it. What is needed in order to get a smooth theory is to find ways of using these functions in order to give a complete ordinal notation system for a suitable segment of the countable ordinals. We are looking forward to future progress in this project.