A note on ordinal exponentiation and derivatives of normal functions

TL;DR

This paper explores the relationship between ordinal exponentiation, derivatives of normal functions, and logical induction principles, showing that certain equivalences hold in weaker base theories like RCA_0.

Contribution

It demonstrates that the equivalence between normal function derivatives and bar induction can be established in RCA_0, using specific normal functions with particular properties.

Findings

Normal functions with bounds f(α) ≤ 1 + α^2 and g(α) ≤ 1 + α·2 are constructed.

Derivatives of these functions correspond to specific ordinal exponentiation functions.

The base theory can be weakened from ACA_0 to RCA_0 for these equivalences.

Abstract

Michael Rathjen and the present author have shown that $\Pi^1_1$-bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in $\mathbf{ACA_0}$. In this note we show that the base theory can be weakened to $\mathbf{RCA_0}$. Our argument makes crucial use of a normal function $f$ with $f(\alpha)\leq 1+\alpha^2$ and $f'(\alpha)=\omega^{\omega^\alpha}$. We will also exhibit a normal function $g$ with $g(\alpha)\leq 1+\alpha\cdot 2$ and $g'(\alpha)=\omega^{1+\alpha}$.

Equations

$$2^X=\{⟨x_1,\dots ,x_n⟩|x_1,\dots ,x_n\in X\text{ and }{x}_n{<}_X\cdots {<}_X{x}_1\}$$

$$f(\alpha )=1+\sum _{\gamma <\alpha }(1+\gamma ).$$

$$f(0)$$

$$f(\alpha +1)$$

$$f(\lambda )$$

$$2^{\alpha }=\sup \{2^{\beta }+\gamma |\beta <\alpha \text{ and }\gamma <2^{\beta }\}.$$

$$\begin{gathered} 2^{\beta }+\gamma <f^{\prime }(\beta )+2^{\beta }\le f(f^{\prime }(\beta ))+1+f^{\prime }(\beta )= \\ =f(f^{\prime }(\beta )+1)\le f(f^{\prime }(\beta +1))=f^{\prime }(\beta +1)\le f^{\prime }(\alpha ), \end{gathered}$$

$$[X{]}^{<\omega }$$

$$[f{]}^{<\omega }(a)$$

$$D^T(X)=\{⟨a,\sigma ⟩|a\in [X{]}^{<\omega }\text{ and }\sigma \in T(|a|)\text{ and }{\mathrm{supp}}_{|a|}(\sigma )=|a|\}$$

$$|a|$$

$$⟨a_0,{\sigma }_0⟩{<}_{D^T(X)}⟨a_1,{\sigma }_1⟩:\iff T(|{\iota }_0|)({\sigma }_0){<}_{T(|a_0\cup a_1|)}T(|{\iota }_1|)({\sigma }_1),$$

$$f_T(\alpha )=\mathrm{otp}(D^T(\alpha )).$$

$$\sigma {<}_{T(n)}{\mu }_n(m)\iff {\mathrm{supp}}_n(\sigma )\subseteq m=\{0,\dots ,m-1\}$$

$$D_X^{\mu }(x)=⟨\{x\},{\mu }_1(0)⟩.$$

$$⟨a,\sigma ⟩{<}_{D^T(X)}{D}_X^{\mu }(x)\iff a\subseteq X\upharpoonright x=\{x^{\prime }\in X|x^{\prime }{<}_{X}x\}.$$

$$f(\alpha )=1+\sum _{\gamma <\alpha }(1+\gamma ).$$

$$1+X=\{\perp \}\cup X$$

$$(1+h)(x)=\{\begin{array}{ll}\perp & \text{if }x=\perp ,\\ h(x)& \text{if }x\in X.\end{array}$$

$$F(X)=1+\sum _{x\in 1+X}(1+X)\upharpoonright x=\{\perp \}\cup \{⟨x,y⟩\in (1+X{)}^2|y{<}_{1+X}x\}.$$

$$⟨x_0,y_0⟩{<}_{F(X)}⟨x_1,y_1⟩\iff \{\begin{array}{l}\text{either x0<Xx1},\\ \text{or x0=x1 and y0<1+Xy1}.\end{array}$$

$$F(h)(⟨x,y⟩)=⟨h(x),(1+h)(y)⟩.$$

$${\mathrm{supp}}_X^F(\perp )=\varnothing \text{and}{\mathrm{supp}}_X^F(⟨x,y⟩)=\{\begin{array}{ll}\{x\}& \text{if }y=\perp ,\\ \{x,y\}& \text{if }y\in X.\end{array}$$

$${\eta }_X:D^F(X)\stackrel{\cong }{\to }F(X)$$

$${\eta }_X(⟨a,\sigma ⟩)=F({\mathrm{en}}_a)(\sigma ),$$

$$F(|{\iota }_a^{a\cup b}|)(\sigma ){<}_{F(|a\cup b|)}F(|{\iota }_b^{a\cup b}|)(\tau ).$$

$${\mathrm{en}}_a={\iota }_a^X\circ {\mathrm{en}}_a^0={\iota }_{a\cup b}^X\circ {\iota }_a^{a\cup b}\circ {\mathrm{en}}_a^0={\iota }_{a\cup b}^X\circ {\mathrm{en}}_{a\cup b}^0\circ |{\iota }_a^{a\cup b}|.$$

$$\begin{gathered} {\eta }_X(⟨a,\sigma ⟩)=F({\mathrm{en}}_a)(\sigma )=F({\iota }_{a\cup b}^X\circ {\mathrm{en}}_{a\cup b}^0)\circ F(|{\iota }_a^{a\cup b}|)(\sigma ){<}_{F(X)} \\ {<}_{F(X)}F({\iota }_{a\cup b}^X\circ {\mathrm{en}}_{a\cup b}^0)\circ F(|{\iota }_b^{a\cup b}|)(\tau )={\eta }_X(⟨b,\tau ⟩). \end{gathered}$$

$${\eta }_X(⟨a,\sigma ⟩)=F({\mathrm{en}}_a)(⟨1,0⟩)=⟨{\mathrm{en}}_a(1),(1+{\mathrm{en}}_a)(0)⟩=⟨x,y⟩.$$

$$\begin{gathered} {\eta }_X\circ D_X^{{\mu }^F}(x)={\eta }_X(⟨\{x\},{\mu }_1^F(0)⟩)=F({\mathrm{en}}_{\{x\}})(⟨0,\perp ⟩)= \\ =⟨{\mathrm{en}}_{\{x\}}(0),(1+{\mathrm{en}}_{\{x\}})(\perp )⟩=⟨x,\perp ⟩={\mu }_X^F(x), \end{gathered}$$

$$(T\circ S)(n)=D^T(S(n)).$$

$${\zeta }_X^{T,S}:D^T\circ D^S(X)\stackrel{\cong }{\to }{D}^{T\circ S}(X).$$

Full text

††footnotetext: © 2020 The Authors. Mathematical Logic Quarterly published by Wiley-VCH GmbH.

This is the accepted version of a publication in Mathematical Logic Quarterly 66:3 (2020) 326-335. Please cite the official journal publication, which is an open access article under the terms of the Creative Commons Attribution-NonCommercial-NoDerivs License.

1. Introduction

A function $f$ from ordinals to ordinals is called normal if it is strictly increasing and continuous at limit stages. The latter means that we have $f(\lambda)=\sup_{\alpha<\lambda}f(\alpha)$ whenever $\lambda$ is a limit ordinal. For any normal function $f$, the class $\{\alpha\,|\,f(\alpha)=\alpha\}$ of fixed points is closed and unbounded. The strictly increasing enumeration of these fixed points is itself a normal function, which is called the derivative $f^{\prime}$ of $f$. In the present paper we will only be concerned with normal functions that map countable ordinals to countable ordinals. These play an important role in proof theory and have interesting computability theoretic properties (see [14, 11]).

In many investigations of normal functions, ordinal exponentiation is presupposed as a starting point. Most notably, the first function in the Veblen hierarchy is usually defined as $\varphi_{0}(\alpha)=\omega^{\alpha}$ (see e. g. [14]). This makes a lot of sense in the context of ordinal notation systems, since a non-zero ordinal is of the form $\omega^{\alpha}$ if and only if it is closed under addition. On the other hand, ordinal exponentiation does itself presuppose certain set existence principles, as the following result from reverse mathematics shows (see below for an introduction):

Theorem 1.1** (J.-Y. Girard [7], J. Hirst [8]).**

The following are equivalent over the base theory $\mathbf{RCA}_{0}$:

• •

arithmetical comprehension (i. e. the principal axiom of $\mathbf{ACA}_{0}$),

• •

if $(X,<_{X})$ is a well-order, then so is

[TABLE]

with the lexicographic order.

Note that elements of $2^{X}$ correspond to ordinals in base-$2$ Cantor normal form. In particular, $2^{X}$ has order type $2^{\alpha}$ (as usually defined in ordinal arithmetic) if $X$ has order type $\alpha$. The theorem is also valid with base $\omega$ (recall $\omega^{\alpha}=2^{\omega\cdot\alpha}$), but base $2$ will have technical advantages in the following.

Theorem 1.1 has been formulated as a result of reverse mathematics. In this research program one investigates implications between foundational and mathematical principles that can be expressed in the language of second order arithmetic. Implications and equivalences are proved over some weak base theory, most commonly in $\mathbf{RCA}_{0}$. The latter can handle primitive recursive constructions relative to an oracle. More specifically, the acronym $\mathbf{RCA}_{0}$ alludes to the recursive comprehension axiom, which allows to form $\Delta^{0}_{1}$-definable subsets of $\mathbb{N}$. Furthermore, $\mathbf{RCA}_{0}$ allows induction for induction formulas of complexity $\Sigma^{0}_{1}$. For a detailed introduction to reverse mathematics we refer to [15].

The case of Theorem 1.1 shows that it is relatively straightforward to consider specific normal functions in reverse mathematics. It is considerably more difficult to express statements that quantify over all normal functions, or at least over a sufficiently rich class. In order to do so, one needs a general representation of normal functions by subsets of the natural numbers. Such a representation is possible via J.-Y. Girard’s [6] notion of dilator and related work by P. Aczel [1, 2]. Full details have been worked out in [5, Section 2]; we will recall them as they become relevant for the present paper. Relative to the representation of normal functions in second order arithmetic, M. Rathjen and the present author have shown that the following are equivalent over $\mathbf{ACA}_{0}$ (see [5, Theorem 5.9]):

1. (1)

Every normal function has a derivative. 2. (2)

The principle of $\Pi^{1}_{1}$-bar induction (also called transfinite induction) holds.

Considering the proof given in [5], we see that the implication from (1) to (2) uses arithmetical comprehension (in the form of the Kleene normal form theorem, cf. [15, Lemma V.1.4]). The proof that (2) implies (1) is carried out in $\mathbf{RCA}_{0}$. In any case, a result of J. Hirst [9] shows that (2) implies arithmetical comprehension (the author is grateful to E. Frittaion for pointing this out). To establish the equivalence between (1) and (2) over $\mathbf{RCA}_{0}$ it remains to show that (1) implies arithmetical comprehension as well. This is the main result of the present paper.

Concerning terminology, we use “bar induction” and “transfinite induction” synonymously, since this coincides with the usage in other papers on the reverse mathematics of well ordering principles (cf. e. g. [13]). At the same time, we appreciate that bar induction is a conceptually different notion in constructive mathematics.

In the rest of this introduction we sketch the proof that statement (1) above implies arithmetical comprehension. Since we have not yet explained the representation of normal functions in second order arithmetic, the following argument will be rather informal. Formal versions of all claims will be established in the following sections. The idea of the proof is to construct a normal function $f$ such that the following holds for any ordinal $\alpha$ (where $f^{\prime}$ is the derivative of $f$):

1. (i)

We have $f(\alpha)\leq 1+\alpha^{2}\leq(1+\alpha)^{2}$. 2. (ii)

We have $2^{\alpha}\leq f^{\prime}(\alpha)$.

Part (i) is supposed to ensure that $\mathbf{RCA}_{0}$ recognizes $f$ as a normal function (since it proves that $(1+\alpha)^{2}$ is well-founded for any well-order $\alpha$). Invoking (1) from above, we obtain access to the well-founded values $f^{\prime}(\alpha)$ of the derivative. The inequality in (ii) corresponds to an order embedding of $2^{\alpha}$ into $f^{\prime}(\alpha)$, which witnesses that $2^{\alpha}$ is also well-founded. By Theorem 1.1 this yields arithmetical comprehension.

Let us now show how clauses (i) and (ii) can be satisfied: Working in a sufficiently strong set theory, the required function $f$ can be described by

[TABLE]

More formally, this infinite sum corresponds to the recursive clauses

[TABLE]

which immediately reveal that $f$ is normal. It might appear more natural to set $f(\alpha+1)=f(\alpha)+\alpha$ in the successor case (at least for $\alpha>0$), but the summand $1$ will be crucial in the following sections. A straightforward induction on $\alpha$ shows that we have $f(\alpha)\leq 1+\alpha^{2}$. The inequality $2^{\alpha}\leq f^{\prime}(\alpha)$ is also proved by induction on $\alpha$: In view of $1=f(0)\leq f^{\prime}(0)$ the claim holds for $\alpha=0$. In case $\alpha\neq 0$ we have

[TABLE]

Given $\beta<\alpha$ and $\gamma<2^{\beta}$, the induction hypothesis yields

[TABLE]

which completes the induction step. When we formalize the proof, we will see that the use of transfinite induction can be avoided, which may be somewhat surprising.

The bound $2^{\alpha}\leq f^{\prime}(\alpha)$ suffices to lower the base theory of [5, Theorem 5.9], but it is not optimal: In the last section of this note we will establish $f^{\prime}(\alpha)=\omega^{\omega^{\alpha}}$. In ordinal arithmetic one is particularly interested in the function $\alpha\mapsto\omega^{\alpha}$, which is the most common starting function for the Veblen hierarchy (see e. g. [14]). In this context it is natural to ask whether $\alpha\mapsto\omega^{\alpha}$ itself is the derivative of some normal function. This is not the case: For any normal function $g$ we see that $g(0)=0$ implies $g^{\prime}(0)=0<\omega^{0}$ while $g(0)>0$ implies $g(1)>1$ and then $g^{\prime}(0)>1=\omega^{0}$. However, this value is the only obstruction: We will exhibit a normal function $g$ with $g(\alpha)\leq 1+\alpha\cdot 2$ and $g^{\prime}(\alpha)=\omega^{1+\alpha}$.

2. A normal function justified by recursive comprehension

In the present section we recall how normal functions can be represented in second order arithmetic; further explanations and full details of all missing proofs can be found in [5, Section 2]. We then apply this representation to the normal function $f$ that has been considered in the introduction.

To find a representation of normal functions, we need to understand how they can be determined by a countable amount of information. Clearly, normal functions are not determined by their values on some fixed countable set of arguments. This suggests to extend our functions into objects with more internal structure. For this purpose it is convenient to use some notions from category theory, namely those of category, functor and natural transformation. We will not need anything that goes beyond these basic concepts; an introduction to category theory (which is much too comprehensive for our purpose) can be found in [10].

The category of linear orders consists of the linear orders as objects and the embeddings (strictly increasing functions) as morphisms. We will be particularly interested in the finite orders $n=\{0,\dots,n-1\}$ (with the usual order relation). These orders and the embeddings between them form the category of natural numbers. Girard’s [6] idea was to consider particularly uniform functors from linear orders to linear orders; those functors that preserve well-foundedness are called dilators. Due to their uniformity, dilators are essentially determined by their restrictions to the category of natural numbers. Provided that these restrictions are countable, they can be used to represent normal functions in reverse mathematics.

In order to describe the uniformity property of dilators, we consider the finite subset functor on the category of sets, which is given by

[TABLE]

where the second clause refers to $f:X\to Y$ and $a\in[X]^{<\omega}$. The cardinality of a finite set $a$ will be denoted by $|a|\in\mathbb{N}$ (which can in turn stand for the finite order $\{0,\dots,|a|-1\}$). The following is essentially due to Girard [6]; we refer to [3, Remark 2.2.2] for a detailed comparison with his original definition.

Definition 2.1** ($\mathbf{RCA}_{0}$).**

A prae-dilator consists of

1. (i)

a functor $T$ from natural numbers to linear orders, such that each order $T(n)=(T(n),<_{T(n)})$ has field $T(n)\subseteq\mathbb{N}$, and 2. (ii)

a natural transformation $\operatorname{supp}:T\Rightarrow[\cdot]^{<\omega}$ that satisfies the following support condition: Each $\sigma\in T(n)$ lies in the image of the embedding $T(\operatorname{en}_{\sigma})$, where $\operatorname{en}_{\sigma}:|\operatorname{supp}_{n}(\sigma)|\to n$ is the strictly increasing enumeration of the set $\operatorname{supp}_{n}(\sigma)\subseteq n=\{0,\dots,n-1\}$.

In second order arithmetic, the function $n\mapsto T(n)$ can be represented by the set $T^{0}=\{(n,\sigma)\,|\,\sigma\in T(n)\}$; the latter is a subset of $\mathbb{N}$ if we code each pair by a single number. Officially, this turns $\sigma\in T(n)$ into an abbreviation for $(n,\sigma)\in T^{0}$, which can be expressed by a formula that is $\Delta^{0}_{1}$ in $\mathbf{RCA}_{0}$. Assuming that finite sets and functions are coded by natural numbers, the action $f\mapsto T(f)$ on morphisms and the map $(n,\sigma)\mapsto\operatorname{supp}_{n}(\sigma)$ can be represented in the same way.

Above we have mentioned that certain functors on linear orders are determined by their restrictions to the category of natural numbers. Conversely, we now explain how a prae-dilator can be extended into a functor on linear orders. In $\mathbf{RCA}_{0}$ we define

[TABLE]

for any prae-dilator $T=(T,\operatorname{supp})$ and any linear order $X$. Informally speaking, the pair $\langle a,\sigma\rangle$ represents the element $T(\operatorname{en}_{a})(\sigma)\in T(X)$, where $\operatorname{en}_{a}:|a|\to X$ is the increasing function with image $a\subseteq X$ (note that $T(\operatorname{en}_{a})(\sigma)$ would make sense if $T$ was defined on all linear orders). Due to the condition $\operatorname{supp}_{|a|}(\sigma)=|a|$, the representation is unique (we would have $a=\operatorname{supp}_{X}(T(\operatorname{en}_{a})(\sigma))$ if $\operatorname{supp}$ was defined beyond the category of natural numbers). In order to define the appropriate order relation on $D^{T}(X)$, we introduce the following notation: Given an embedding $f:a\to b$ between finite orders, let $|f|:|a|\to|b|$ be the unique function that makes

[TABLE]

a commutative diagram. We can now stipulate

[TABLE]

where $\iota_{i}:a_{i}\hookrightarrow a_{0}\cup a_{1}$ are the inclusions. It is also possible to turn $D^{T}(\cdot)$ into a functor and to define natural support functions $\operatorname{supp}_{X}:D^{T}(X)\to[X]^{<\omega}$. In particular we can declare that $T$ is a dilator if and only if the order $D^{T}(X)$ is well-founded for any well-order $X$ (the two obvious definitions of well-ordering are equivalent over $\mathbf{RCA}_{0}$, see e. g. [3, Lemma 2.3.12]). From the viewpoint of a sufficiently strong set theory, each dilator $T$ gives rise to a function $f_{T}$ from ordinals to ordinals, with

[TABLE]

Here we view $\alpha$ as a linear order and write $\operatorname{otp}(X)$ for the order type of $X$. We can view $T$ as a representation of the function $f_{T}$ in second order arithmetic.

It is straightforward to specify a dilator $T$ with $f_{T}(\alpha)=\alpha+1$. In particular, the function $f_{T}$ does not need to be normal. The following condition, which was identified by Aczel [1, 2], ensures that we are concerned with a normal function:

Definition 2.2** ($\mathbf{RCA}_{0}$).**

A normal (prae-)dilator consists of a (prae-)dilator $T$ and a natural family of embeddings $\mu_{n}:n\to T(n)$ such that

[TABLE]

holds for all $\sigma\in T(n)$ and all $m<n$.

Note that we necessarily have $\operatorname{supp}_{1}(\mu_{1}(0))=1$, since $\operatorname{supp}_{1}(\mu_{1}(0))=\emptyset$ would yield $\mu_{1}(0)<_{T(1)}\mu_{1}(0)$. This allows us to define $D^{\mu}_{X}:X\to D^{T}(X)$ by

[TABLE]

One can show that we have

[TABLE]

Hence the elements $D^{\mu}_{X}(x)$ are cofinal in $D^{T}(X)$ if $X$ has limit type. In a sufficiently strong set theory one can deduce that $f_{T}$ is normal (cf. [5, Proposition 2.12]).

In the introduction we have considered a normal function $f$ with

[TABLE]

Our next goal is to construct a normal dilator $F$ that represents this function. Given an order $X$, we write

[TABLE]

for the extension of $X$ by a new minimum element $\bot$. To obtain a functor we map each embedding $h:X\rightarrow Y$ to the embedding $1+h:1+X\to 1+Y$ with

[TABLE]

In order to define a dilator $F$ we must specify a linear order $F(n)$ for each finite order $n=\{0,\dots,n-1\}$. It will later be convenient to have a more general definition, which explains $F(X)$ for any linear order $X$.

Definition 2.3** ($\mathbf{RCA}_{0}$).**

For each linear order $X$ we define

[TABLE]

Note that $F(X)$ contains no pairs of the form $\langle\bot,y\rangle$, since $y<_{1+X}\bot$ must fail. To turn $F(X)$ into a linear order we declare that $\bot$ is minimal and that we have

[TABLE]

For an embedding $h:X\to Y$, define $F(f):F(X)\to F(Y)$ by $F(f)(\bot)=\bot$ and

[TABLE]

Each order $X$ gives rise to a function $\operatorname{supp}^{F}_{X}:F(X)\to[X]^{<\omega}$ with

[TABLE]

Finally, we define functions $\mu^{F}_{X}:X\to F(X)$ by setting $\mu^{F}_{X}(x)=\langle x,\bot\rangle$.

Note that the relations $\sigma\in F(n)$, $\sigma<_{F(n)}\tau$, $F(h)(\sigma)=\tau$ with $h:n\to m$, $a=\operatorname{supp}^{F}_{n}(\sigma)$ and $\sigma=\mu^{F}_{n}(m)$ are $\Delta^{0}_{1}$-definable in $\mathbf{RCA}_{0}$. Hence the restriction of $F$ to the category of natural numbers exists as a set. It is straightforward to verify that Definitions 2.1 and 2.2 are satisfied (the condition $y<_{1+X}x$ in the definition of $F(X)$ is crucial for the latter):

Lemma 2.4** ($\mathbf{RCA}_{0}$).**

Restricting Definition 2.3 to the category of natural numbers yields a normal prae-dilator $F$.

To show that $F$ is a dilator we need to consider the ordered sets $D^{F}(X)$ from equation (1). As a preparation, we relate $D^{F}(X)$ to the order $F(X)$ constructed in Definition 2.3. Let us also recall that $\mu^{F}$ (or rather its restriction to the category of natural numbers) gives rise to a family of functions $D^{\mu^{F}}_{X}:X\to D^{F}(X)$, as defined by equation (3). For later use, we relate these to the functions $\mu^{F}_{X}:X\to F(X)$.

Lemma 2.5** ($\mathbf{RCA}_{0}$).**

For each order $X$ we have an isomorphism

[TABLE]

with $\eta_{X}\circ D^{\mu^{F}}_{X}=\mu^{F}_{X}$.

Proof.

Recall that $D^{F}(X)$ consists of pairs $\langle a,\sigma\rangle$, where $a$ is a finite suborder of $X$ and $\sigma\in F(|a|)$ satisfies $\operatorname{supp}^{F}_{|a|}(\sigma)=|a|$. We set

[TABLE]

writing $\operatorname{en}_{a}:|a|\to X$ for the increasing function with range $a$. It is straightforward to verify that $F$ is an endofunctor on the category of linear orders. Using this fact one can show that $\eta_{X}$ is an embedding, as in the proof of [4, Proposition 2.1]: Given sets $Y\subseteq Z$, we agree to write $\iota_{Y}^{Z}:Y\hookrightarrow Z$ for the inclusion. Assume that we have $\langle a,\sigma\rangle<_{D^{F}(X)}\langle b,\tau\rangle$, and note that this amounts to

[TABLE]

Given a finite order $c$, we write $\operatorname{en}^{0}_{c}:|c|\to c$ for the increasing enumeration. For the function $\operatorname{en}_{a}:a\to X$ from above, the definition of $|\cdot|$ yields

[TABLE]

Since $F(\iota_{a\cup b}^{X}\circ\operatorname{en}^{0}_{a\cup b})$ is an embedding, the above inequality implies

[TABLE]

This confirms that $\eta_{X}$ is an embedding and in particular injective. It remains to show surjectivity. As a representative example, consider $\langle x,y\rangle\in F(X)$ with $y\neq\bot$. According to Definition 2.3 we must have $y<_{X}x$. Hence $a:=\{x,y\}$ has two elements, and the function $\operatorname{en}_{a}:2\to X$ has values $\operatorname{en}_{a}(0)=y$ and $\operatorname{en}_{a}(1)=x$. Since $\sigma:=\langle 1,0\rangle\in F(2)$ satisfies $\operatorname{supp}^{F}_{2}(\sigma)=\{0,1\}=2$, we get $\langle a,\sigma\rangle\in D^{F}(X)$. By construction we have

[TABLE]

A similar argument shows that the image of $\eta_{X}$ contains $\bot$ and all elements of the form $\langle x,\bot\rangle$. In order to verify the remaining claim we consider $x\in X$ and write $\operatorname{en}_{\{x\}}:1\to X$ for the function with range $\{x\}$. In view of equation (3) we obtain

[TABLE]

as required. ∎

The normal function $f$ from the introduction satisfies $f(\alpha)\leq(1+\alpha)^{2}$. We can now recover this result on the level of the prae-dilator $F$.

Lemma 2.6** ($\mathbf{RCA}_{0}$).**

For each linear order $X$ we have an embedding of $D^{F}(X)$ into $(1+X)^{2}$, where the latter is equipped with the lexicographic order.

Proof.

In view of the previous lemma it suffices to exhibit an embedding of $F(X)$ into $(1+X)^{2}$. Indeed, we have defined $F(X)\backslash\{\bot\}$ as a suborder of $(1+X)^{2}$. In order to obtain the desired embedding it suffices to map $\bot\in F(X)$ to the minimum element $\langle\bot,\bot\rangle\in(1+X)^{2}$. This is possible because $\langle\bot,\bot\rangle$ does not lie in the suborder $F(X)\backslash\{\bot\}$, due to the condition $y<_{1+X}x$ in Definition 2.3. ∎

The following result concludes the reconstruction of $f$ in second order arithmetic:

Corollary 2.7** ($\mathbf{RCA}_{0}$).**

The normal prae-dilator $F$ is a normal dilator.

Proof.

In view of Lemma 2.4 it remains to show that $D^{F}(X)$ is well-founded for any well-order $X$. By the previous lemma this reduces to the claim that $(1+X)^{2}$ is well-founded. More generally, the usual proof that any product $X\times Y$ of well-orders is well-founded goes through in $\mathbf{RCA}_{0}$: Assume that there is a strictly decreasing sequence $(\langle x_{n},y_{n}\rangle)_{n\in\mathbb{N}}$ in $X\times Y$. Then the sequence $(x_{n})_{n\in\mathbb{N}}$ is non-increasing. Since $X$ is well-founded, there is an $N\in\mathbb{N}$ such that $x_{n}=x_{N}$ holds for all $n\geq N$ (otherwise a strictly decreasing sequence in $X$ could be constructed by recursion). Then $(y_{n})_{n\geq N}$ is a strictly decreasing sequence in $Y$, which contradicts the assumption that $Y$ is well-founded. ∎

3. From derivative to arithmetical comprehension

In the present section we recall how derivatives of normal functions are defined in the context of second order arithmetic. We then show how the inequality $2^{\alpha}\leq f^{\prime}(\alpha)$ from the introduction can be recovered in $\mathbf{RCA}_{0}$. Finally, we conclude that the base theory in a result of Rathjen and the present author can be lowered from $\mathbf{ACA}_{0}$ to $\mathbf{RCA}_{0}$.

If $g^{\prime}$ is the derivative of a normal function $g$, then we have $g\circ g^{\prime}=g^{\prime}$. To formulate this condition in second order arithmetic, we need to define the composition $T\circ S$ of normal prae-dilators. This is not entirely straightforward: In view of Definition 2.1 the orders $S(n)$ may be infinite, while $T$ is only defined on finite orders represented by natural numbers. In order to overcome this obstacle we use equation (1) to extend $T$ beyond the category of natural numbers, and set

[TABLE]

One can equip $T\circ S$ with the structure of a prae-dilator, as shown in [5, Section 2]. According to [5, Proposition 2.14] there is a family of isomorphisms

[TABLE]

If $S$ and $T$ are dilators, then equation (2) yields

[TABLE]

where the third equality relies on $D^{S}(\alpha)\cong\operatorname{otp}(D^{S}(\alpha))=f_{S}(\alpha)$ and the fact that $D^{T}$ is functorial. Hence the given composition of dilators represents the usual composition of functions on the ordinals. If $T=(T,\mu^{T})$ and $S=(S,\mu^{S})$ are normal prae-dilators, then we can invoke equation (3) to define $\mu^{T\circ S}_{n}:n\to(T\circ S)(n)$ by

[TABLE]

In [5, Lemma 2.16] it has been verified that this turns $T\circ S$ into a normal prae-dilator, and that we have

[TABLE]

We can now recall the following notion, which has been introduced in [5]:

Definition 3.1** ($\mathbf{RCA}_{0}$).**

Let $T$ be a normal prae-dilator. An upper derivative of $T$ consists of a normal prae-dilator $S$ and a natural transformation $\xi:T\circ S\Rightarrow S$ that satisfies $\xi\circ\mu^{T\circ S}=\mu^{S}$.

According to [5, Lemma 2.19], the natural transformation $\xi$ can be extended into a family of order embeddings $D^{\xi}_{X}:D^{T\circ S}(X)\to D^{S}(X)$ with

[TABLE]

If $S$ is a dilator, then the embedding $D^{\xi}_{\alpha}$ witnesses

[TABLE]

for any ordinal $\alpha$. The converse inequality is automatic when $f_{T}$ is a normal function. Hence $f_{S}$ does indeed enumerate fixed points of $f_{T}$. It is possible that some fixed points are omitted. In this case $f_{S}$ grows faster than the derivative of $f_{T}$, which justifies the term “upper derivative”. To characterize the actual derivative on the level of normal dilators one can consider initial objects in the category of upper derivatives, as shown in [5].

We can now state the main technical result of this paper. As explained in the introduction, the order $2^{X}$ consists of finite descending sequences with entries in $X$.

Theorem 3.2** ($\mathbf{RCA}_{0}$).**

Assume that $G$ and $\xi:F\circ G\Rightarrow G$ form an upper derivative of the normal dilator $F$ from Definition 2.3. Then there is an order embedding of $2^{X}$ into $D^{G}(X)$, for each linear order $X$.

Proof.

As preparation, we observe the following: By Lemma 2.5 and the results that we have recalled in the the first part of the present section, we get an embedding

[TABLE]

According to Definition 2.2, the normal prae-dilator $G$ comes with a natural transformation $\mu^{G}$. The latter extends into an embedding $D^{\mu^{G}}_{X}:X\to D^{G}(X)$, by equation (3). The values of the desired embedding

[TABLE]

will be defined by recursion along sequences in $2^{X}$. To ensure that the recursion goes through we will simultaneously verify that we have

[TABLE]

Officially, the recursive construction and the inductive verification should be untangled. To show that this is possible, we point out that it will always be decidable whether the prerequisites of our recursive clauses are satisfied. Whenever they fail, we can thus assign $\xi^{F}_{X}(\bot)\in D^{G}(X)$ as a default value. Once the recursion is completed, the inductive verification shows that the default value is never required. Let us also point out that the induction statement has complexity $\Pi^{0}_{1}$ (note that (6) involves a universal quantification over $x$). Since $\Sigma^{0}_{1}$-induction and $\Pi^{0}_{1}$-induction are equivalent (see e.g. [15, Corollary II.3.10]), this shows that the induction can be carried out in $\mathbf{RCA}_{0}$. Let us now specify the details: For the base of the recursion we use the minimum element $\bot$ of $F(D^{G}(X))$ and set

[TABLE]

To verify condition (6) we observe that equations (5) and (4) and Lemma 2.5 yield

[TABLE]

In view of $\bot<_{F(D^{G}(X))}\langle D^{\mu^{G}}_{X}(x),\bot\rangle$ we get $J(\langle\rangle)<_{D^{G}(X)}D^{\mu^{G}}_{X}(x)$ for any $x\in X$, as required by condition (6). In the recursion step we put

[TABLE]

To see that the argument $\langle D^{\mu^{G}}_{X}(x_{0}),J(\langle x_{1},\dots,x_{n}\rangle)\rangle$ does indeed lie in the domain $F(D^{G}(X))$ of $\xi^{F}_{X}$, we must establish the condition $J(\langle x_{1},\dots,x_{n}\rangle)<_{D^{G}(X)}D^{\mu^{G}}_{X}(x_{0})$ from Definition 2.3. By the definition of the order $2^{X}$ we have $x_{1}<_{X}x_{0}$ or $n=0$. Hence the required inequality holds by condition (6). Furthermore, condition (6) remains valid in the recursion step: For $x_{0}<_{X}x$ we have $D^{\mu^{G}}_{X}(x_{0})<_{D^{G}(X)}D^{\mu^{G}}_{X}(x)$. Together with the definition of $J(\langle x_{0},\dots,x_{n}\rangle)$ and the equality $D^{\mu^{G}}_{X}(x)=\xi^{F}_{X}(\langle D^{\mu^{G}}_{X}(x),\bot\rangle)$ from above, this does indeed imply the condition $J(\langle x_{0},\dots,x_{n}\rangle)<_{D^{G}(X)}D^{\mu^{G}}_{X}(x)$. It remains to show that $J$ is an order embedding. We establish

[TABLE]

by joint induction on $\sigma$ and $\tau$ (or by induction on the length of $\tau$, which leads to an induction statement of complexity $\Pi^{0}_{1}$). Let us first assume that we have

[TABLE]

with $\tau\neq\langle\rangle$. Since $\bot\in F(D^{G}(X))$ is minimal we do indeed get

[TABLE]

Now consider an inequality

[TABLE]

We must either have $x_{0}<_{X}y_{0}$, or $x_{0}=y_{0}$ and $\langle x_{1},\dots,x_{n}\rangle<_{2^{X}}\langle y_{1},\dots,y_{m}\rangle$. If the latter holds, then we get $J(\langle x_{1},\dots,x_{n}\rangle)<_{D^{G}(X)}J(\langle y_{1},\dots,y_{m}\rangle)$ by the induction hypothesis. In either case we obtain

[TABLE]

By applying $\xi^{F}_{X}$ to both sides we get $J(\sigma)<_{D^{G}(X)}J(\tau)$. ∎

Recall that a (normal) prae-dilator $S$ is a dilator if and only if the order $D^{S}(X)$ is well-founded for any well-order $X$. We can draw the following conclusion.

Corollary 3.3** ($\mathbf{RCA}_{0}$).**

Assume that any normal dilator $T$ has an upper derivative $(S,\xi)$ such that $S$ is a dilator. Then arithmetical comprehension holds.

Proof.

In view of Theorem 1.1 it suffices to show that $2^{X}$ is well-founded for any given well-order $X$. Construct $F$ as in Definition 2.3. From Lemma 2.4 and Corollary 2.7 we know that $F$ is a normal dilator. Hence the assumption of the present corollary yields an upper derivative $\xi:F\circ G\Rightarrow G$ such that $D^{G}(X)$ is well-founded. The previous theorem provides an order embedding of $2^{X}$ into $D^{G}(X)$, which witnesses that $2^{X}$ is well-founded as well. ∎

According to [5, Definition 2.26], a derivative of a normal prae-dilator is an upper derivative that is initial in a suitable sense. In [5, Section 4] it has been shown how to construct a derivative $(\partial T,\xi^{T})$ of a given normal prae-dilator $T$. The transformation of $T$ into $\partial T$ and $\xi^{T}$ can be implemented in $\mathbf{RCA}_{0}$ (in particular it is computable). Hence $\mathbf{RCA}_{0}$ proves that (upper) derivatives exist. What $\mathbf{RCA}_{0}$ cannot show is that $X\mapsto D^{\partial T}(X)$ preserves well-foundedness when $X\mapsto D^{T}(X)$ does. Indeed, Rathjen and the present author have shown that the latter is equivalent to $\Pi^{1}_{1}$-bar induction (which asserts that $\Pi^{1}_{1}$-induction is available along any well-order). As explained in the introduction, we can now lower the base theory over which this equivalence holds (Theorem 5.9 of [5] proves it over $\mathbf{ACA}_{0}$).

Corollary 3.4** ($\mathbf{RCA}_{0}$).**

The following are equivalent:

1. (1)

If $T$ is a normal dilator, then so is $\partial T$. 2. (2)

Any normal dilator $T$ has an upper derivative $(S,\xi)$ such that $S$ is a dilator. 3. (3)

The principle of $\Pi^{1}_{1}$-bar induction holds.

Proof.

To see that (1) implies (2) it suffices to know that $\partial T$ and $\xi^{T}$ form an upper derivative of $T$. This holds by [5, Proposition 4.11], which was proved in $\mathbf{RCA}_{0}$. The implication from (2) to (3) holds over $\mathbf{ACA}_{0}$, by the original proof of [5, Theorem 5.9]. Now Corollary 3.3 of the present paper tells us that (2) implies arithmetical comprehension, which means that all ingredients of the proof become available over $\mathbf{RCA}_{0}$. The implication from (3) to (1) holds by [5, Theorem 5.8], which was established in $\mathbf{RCA}_{0}$. ∎

Combining Corollaries 3.4 and 3.3 yields a somewhat indirect proof that $\Pi^{1}_{1}$-bar induction implies arithmetical comprehension. In fact, the latter is equivalent to the weaker principle of arithmetical transfinite induction, as shown by J. Hirst [9].

4. Ordinal exponentiation as a derivative

In the present section we show that the derivative of the normal function $f$ from the introduction is given by $f^{\prime}(\alpha)=\omega^{\omega^{\alpha}}$. We also specify a normal function $g$ with $g(\alpha)\leq 1+\alpha\cdot 2$ and $g^{\prime}(\alpha)=\omega^{1+\alpha}$. The relevance of this result has been discussed at the end of the introduction. In contrast to the previous sections, we do not aim to formalize this section in a weak base theory.

The normal function $f$ was defined by $f(\alpha)=1+\sum_{\gamma<\alpha}(1+\gamma)$, or more formally by the recursive clauses

[TABLE]

Recall that $\alpha>0$ is multiplicatively (resp. additively) principal if $\beta,\gamma<\alpha$ implies $\beta\cdot\gamma<\alpha$ (resp. $\beta+\gamma<\alpha$). The following determines the derivative of $f$.

Lemma 4.1**.**

We have $f(\alpha)=\alpha$ if and only if $\alpha$ is a multiplicatively principal limit ordinal.

Proof.

Assume that $f(\alpha)=\alpha$ holds. In view of $f(1)>f(0)=1$ we get $\alpha>1$. By the definition of $f$ we also see that $0<\beta<\alpha$ implies

[TABLE]

so that $\alpha$ is a limit. We can now infer that $\alpha$ is additively principal: Consider $\beta,\gamma<\alpha$ and set $\delta:=\max\{\beta,\gamma\}$. Since $\alpha$ is a limit, we get $\delta+1<\alpha$ and then

[TABLE]

By a straightforward induction on $\gamma$ we get $\beta\cdot\gamma\leq f(\beta+\gamma)$. Since $\alpha$ is additively principal, it follows that $\beta,\gamma<\alpha$ implies

[TABLE]

Now assume that $\alpha$ is a multiplicatively (and hence additively) principal limit ordinal. Then $\gamma<\alpha$ implies $1+\gamma^{2}<\alpha$. In the introduction we have noted that $f(\gamma)$ is bounded by $1+\gamma^{2}$. Hence we get

[TABLE]

The inequality $\alpha\leq f(\alpha)$ is automatic, since $f$ is strictly increasing. ∎

The derivative of $f$ can now be described as follows:

Corollary 4.2**.**

We have $f^{\prime}(\alpha)=\omega^{\omega^{\alpha}}$ for any ordinal $\alpha$.

Proof.

It is known that an infinite ordinal is multiplicatively principal if and only if it is of the form $\omega^{\omega^{\alpha}}$ (see e. g. [12, Exercise 3.3.15]). Hence the previous lemma implies that $\alpha\mapsto\omega^{\omega^{\alpha}}$ is the increasing enumeration of the fixed points of $f$. The claim follows by the definition of the derivative. ∎

In the rest of this section we construct a normal function $g$ with $g^{\prime}(\alpha)=\omega^{1+\alpha}$. Such a function can be defined by

[TABLE]

By induction on the limit ordinal $\lambda$ we get

[TABLE]

In particular we have $g(\lambda)<g(\lambda+1)$, which readily implies that $g$ is strictly increasing. We also obtain $g(\alpha)\leq 1+\alpha\cdot 2$ for any ordinal $\alpha$, as promised above. To characterize the derivative of $g$ we show the following:

Lemma 4.3**.**

We have $g(\alpha)=\alpha$ if and only if $\alpha$ is an additively principal limit ordinal.

Proof.

First assume that we have $g(\alpha)=\alpha$. In view of $g(0)=1$ we get $\alpha>0$. Since $g(\gamma+1)>\gamma+1$ holds for any successor, we learn that $\alpha$ must be a limit. In order to show that $\alpha$ is additively principal we consider arbitrary ordinals $\beta,\gamma<\alpha$. Setting $\delta:=\max\{\beta,\gamma\}$, we get

[TABLE]

Conversely, assume that $\alpha$ is an additively principal limit ordinal. Then $\gamma<\alpha$ implies $\gamma\cdot 2<\alpha$, which yields

[TABLE]

Yet again, the inequality $\alpha\leq g(\alpha)$ is automatic. ∎

We can now describe the derivative of $g$:

Corollary 4.4**.**

We have $g^{\prime}(\alpha)=\omega^{1+\alpha}$ for any ordinal $\alpha$.

Proof.

It is well-known that an ordinal is additively principal if and only if it is of the form $\omega^{\alpha}$ (consider Cantor normal forms). Excluding $\omega^{0}=1$, we see that the additively principal limit ordinals are those of the form $\omega^{1+\alpha}$. Now the claim follows by the previous lemma. ∎

To conclude, we explain why we have used $f$ rather than $g$ to lower the base theory of [5, Theorem 5.9]: In order to represent $g$ by a normal dilator we would need uniform notation systems for the values of this function. Elements of $g(\alpha+1)$ can be written as $\beta$ or $(\alpha+1)+\beta$ with $\beta<\alpha+1$, which suggests a relativized ordinal notation system. Canonical representations for elements of $g(\lambda)$ appear less obvious when $\lambda$ is a limit. For example, the ordinal $\omega+2\in g(\omega\cdot 2)$ could be written as $(\omega+1)+1\in g(\omega+1)$, as $(\omega+2)+0\in g(\omega+2)$ or as $\omega+2\in g(\omega+3)$. It would be interesting to know whether $g$ does have a reasonable representation as a normal dilator.