## A NOTE ON ORDINAL EXPONENTIATION AND DERIVATIVES OF NORMAL FUNCTIONS

## ANTON FREUND

Abstract. Michael Rathjen and the present author have shown that Π 1 1 -bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in ACA 0 . In this note we show that the base theory can be weakened to RCA 0 . Our argument makes crucial use of a normal function f with f ( α ) ≤ 1 + α 2 and f ′ ( α ) = ω ω α . We will also exhibit a normal function g with g α ( ) ≤ 1 + α · 2 and g ′ ( α ) = ω 1+ α .

## 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 ( λ ) = sup α&lt;λ f ( α ) whenever λ is a limit ordinal. For any normal function f , the class { α f α | ( ) = α } 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 ′ 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 ϕ 0 ( α ) = ω α (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 ω α 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 RCA 0 :

- · arithmetical comprehension (i. e. the principal axiom of ACA 0 ),
- · if ( X,&lt; X ) is a well-order, then so is

$$2 ^ { X } = \left \{ \langle x _ { 1 }, \dots, x _ { n } \rangle \, | \, x _ { 1 }, \dots, x _ { n } \in X \ a n d \, x _ { n } < _ { X } \dots < _ { X } x _ { 1 } \right \}$$

with the lexicographic order.

2010 Mathematics Subject Classification. 03B30, 03D60, 03E10, 03F15.

Key words and phrases. Normal function, derivative, ordinal exponentiation, dilator, reverse mathematics.

© 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.

Note that elements of 2 X correspond to ordinals in base-2 Cantor normal form. In particular, 2 X has order type 2 α (as usually defined in ordinal arithmetic) if X has order type α . The theorem is also valid with base ω (recall ω α = 2 ω α · ), 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 RCA 0 . The latter can handle primitive recursive constructions relative to an oracle. More specifically, the acronym RCA 0 alludes to the recursive comprehension axiom, which allows to form ∆ -definable subsets of 0 1 N . Furthermore, RCA 0 allows induction for induction formulas of complexity Σ . 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 ACA 0 (see [5, Theorem 5.9]):

- (1) Every normal function has a derivative.
- (2) The principle of Π 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 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 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 α (where f ′ is the derivative of f ):

- (i) We have f ( α ) ≤ 1 + α 2 ≤ (1 + α ) 2 .
- (ii) We have 2 α ≤ f ′ ( α ).

Part (i) is supposed to ensure that RCA 0 recognizes f as a normal function (since it proves that (1+ α ) 2 is well-founded for any well-order α ). Invoking (1) from above, we obtain access to the well-founded values f ′ ( α ) of the derivative. The inequality

in (ii) corresponds to an order embedding of 2 α into f ′ ( α ), which witnesses that 2 α 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

$$f ( \alpha ) = 1 + \sum _ { \gamma < \alpha } ( 1 + \gamma ). \\ e \, \text{sum corresponds to the recur}$$

More formally, this infinite sum corresponds to the recursive clauses

$$f ( 0 ) & = 1, \\ f ( \alpha + 1 ) & = f ( \alpha ) + 1 + \alpha, \\ f ( \lambda ) & = \sup _ { \alpha < \lambda } f ( \alpha ) \quad \text{ for } \lambda \, \lim i t, \\ \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \,.$$

which immediately reveal that f is normal. It might appear more natural to set f ( α +1) = f ( α ) + α in the successor case (at least for α &gt; 0), but the summand 1 will be crucial in the following sections. A straightforward induction on α shows that we have f ( α ) ≤ 1 + α 2 . The inequality 2 α ≤ f ′ ( α ) is also proved by induction on α : In view of 1 = f (0) ≤ f ′ (0) the claim holds for α = 0. In case α = 0 we have

/negationslash

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

Given β &lt; α and γ &lt; 2 β , the induction hypothesis yields

$$2 ^ { \beta } + \gamma < f ^ { \prime } ( \beta ) + 2 ^ { \beta } \leq f ( f ^ { \prime } ( \beta ) ) + 1 + f ^ { \prime } ( \beta ) = \\ & = f ( f ^ { \prime } ( \beta ) + 1 ) \leq f ( f ^ { \prime } ( \beta + 1 ) ) = f ^ { \prime } ( \beta + 1 ) \leq f ^ { \prime } ( \alpha ),$$

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 α ≤ f ′ ( α ) 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 ′ ( α ) = ω ω α . In ordinal arithmetic one is particularly interested in the function α → ω α , which is the most common starting function for the Veblen hierarchy (see e. g. [14]). In this context it is natural to ask whether α → ω α 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 ′ (0) = 0 &lt; ω 0 while g (0) &gt; 0 implies g (1) &gt; 1 and then g ′ (0) &gt; 1 = ω 0 . However, this value is the only obstruction: We will exhibit a normal function g with g α ( ) ≤ 1 + α · 2 and g ′ ( α ) = ω 1+ α .

## 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 , . . . , 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

$$[ \begin{matrix} 1 \end{matrix}$$

$$[ X ] ^ { < \omega } & = \text{``the set of finite subsets of } X \text{``}, \\ [ f ] ^ { < \omega } ( a ) & = \{ f ( x ) \, | \, x \in a \},$$

where the second clause refers to f : X → Y and a ∈ [ X ] &lt;ω . The cardinality of a finite set a will be denoted by | a | ∈ N (which can in turn stand for the finite order { 0 , . . . , | 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 ( RCA . 0 ) A prae-dilator consists of

- (i) a functor T from natural numbers to linear orders, such that each order T n ( ) = ( T n , &lt; ( ) T n ( ) ) has field T n ( ) ⊆ N , and
- (ii) a natural transformation supp : T ⇒ · [ ] &lt;ω that satisfies the following support condition: Each σ ∈ T n ( ) lies in the image of the embedding T (en σ ), where en σ : | supp n ( σ ) | → n is the strictly increasing enumeration of the set supp n ( σ ) ⊆ n = 0 { , . . . , n - } 1 .

↦

↦

↦

In second order arithmetic, the function n → T n ( ) can be represented by the set T 0 = { ( n, σ ) | σ ∈ T n ( ) } ; the latter is a subset of N if we code each pair by a single number. Officially, this turns σ ∈ T n ( ) into an abbreviation for ( n, σ ) ∈ T 0 , which can be expressed by a formula that is ∆ 0 1 in RCA 0 . Assuming that finite sets and functions are coded by natural numbers, the action f → T f ( ) on morphisms and the map ( n, σ ) → supp n ( σ ) 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 RCA 0 we define

$$( 1 ) \quad \ D ^ { T } ( X ) = \left \{ \langle a, \sigma \rangle \, | \, a \in [ X ] ^ { < \omega } \text{ and } \sigma \in T ( | a | ) \text{ and } \text{ supp} _ { | a | } ( \sigma ) = | a | \right \}$$

for any prae-dilator T = ( T, supp) and any linear order X . Informally speaking, the pair 〈 a, σ 〉 represents the element T (en a )( σ ) ∈ T X ( ), where en a : | a | → X is the increasing function with image a ⊆ X (note that T (en a )( σ ) would make sense if T was defined on all linear orders). Due to the condition supp | a | ( σ ) = | a | , the representation is unique (we would have a = supp X ( T (en a )( σ )) if 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 → b between finite orders, let | f | : | a | →| | b be the unique function that makes

$$\lll \Gamma + \lll \lll _ { 1 } \cdot \lll _ { 2 } \lll _ { 3 } \lll _ { 4 } \lll _ { 5 } \\ | a | & \xrightarrow { \cong } a \\ | f | \Big \downarrow \\ | b | & \xrightarrow { \cong } b$$

a commutative diagram. We can now stipulate

$$\langle a _ { 0 }, \sigma _ { 0 } \rangle < _ { D ^ { T } ( X ) } \langle a _ { 1 }, \sigma _ { 1 } \rangle \ \colon \Leftrightarrow \ T ( | \iota _ { 0 } | ) ( \sigma _ { 0 } ) < _ { T ( | a _ { 0 } \cup a _ { 1 } | ) } T ( | \iota _ { 1 } | ) ( \sigma _ { 1 } ),$$

where ι i : a i ↪ → a 0 ∪ a 1 are the inclusions. It is also possible to turn D T ( ) · into a functor and to define natural support functions supp X : D T ( X ) → [ X ] &lt;ω . 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 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

$$f _ { T } ( \alpha ) = \text{otp} ( D ^ { T } ( \alpha ) ).$$

Here we view α as a linear order and write 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 ( α ) = α + 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 ( RCA . 0 ) A normal (prae-)dilator consists of a (prae-)dilator T and a natural family of embeddings µ n : n → T n ( ) such that

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

holds for all σ ∈ T n ( ) and all m&lt;n .

Note that we necessarily have supp ( 1 µ 1 (0)) = 1, since supp 1 ( µ 1 (0)) = ∅ would yield µ 1 (0) &lt; T (1) µ 1 (0). This allows us to define D µ X : X → D T ( X ) by

$$D _ { X } ^ { \mu } ( x ) = \langle \{ x \}, \mu _ { 1 } ( 0 ) \rangle.$$

One can show that we have

$$\langle a, \sigma \rangle < _ { D ^ { T } ( X ) } D ^ { \mu } _ { X } ( x ) \ \Leftrightarrow \ a \subseteq X \restriction x = \{ x ^ { \prime } \in X \, | \, x ^ { \prime } < _ { X } x \}.$$

Hence the elements D µ 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

$$f ( \alpha ) = 1 + \sum _ { \gamma < \alpha } ( 1 + \gamma ). \\ \ t r n e t \ a \text{ normal dilator } F \text{ that}$$

Our next goal is to construct a normal dilator F that represents this function.

Given an order X , we write

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

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

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

In order to define a dilator F we must specify a linear order F n ( ) for each finite order n = { 0 , . . . , 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 ( RCA . 0 ) For each linear order X we define

$$F ( X ) = 1 + \sum _ { x \in 1 + X } ( 1 + X ) \upharpoonright x = \{ \perp \} \cup \{ \langle x, y \rangle \in ( 1 + X ) ^ { 2 } \, | \, y < _ { 1 + X } x \}. \\ \intertext { N o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t ot o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o c t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t to t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t st t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o to t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t i t i t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t s t t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o o o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t t t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t ot t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t O t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t xt o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o xt o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t ot ot o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t o t ot o { \Gamma \colon d e x }$$

Note that F X ( ) contains no pairs of the form 〈⊥ , y 〉 , since y &lt; 1+ X ⊥ must fail. To turn F X ( ) into a linear order we declare that ⊥ is minimal and that we have

$$\langle x _ { 0 }, y _ { 0 } \rangle < _ { F ( X ) } \langle x _ { 1 }, y _ { 1 } \rangle \quad \Leftrightarrow \quad \begin{cases} \text{either } x _ { 0 } < _ { X } x _ { 1 }, \\ \text{or } x _ { 0 } = x _ { 1 } \text{ and } y _ { 0 } < _ { 1 + X } y _ { 1 }. \end{cases}$$

For an embedding h : X → Y , define F f ( ) : F X ( ) → F Y ( ) by F f ( )( ⊥ ) = ⊥ and

$$F ( h ) ( \langle x, y \rangle ) = \langle h ( x ), ( 1 + h ) ( y ) \rangle.$$

Each order X gives rise to a function supp F X : F X ( ) → [ X ] &lt;ω with

$$\text{supp} _ { X } ^ { F } ( \perp ) = \emptyset \quad \text{and} \quad \text{supp} _ { X } ^ { F } ( \langle x, y \rangle ) = \begin{cases} \{ x \} & \text{if $y=\perp$,} \\ \{ x, y \} & \text{if $y\in X$.} \end{cases}$$

Finally, we define functions µ F X : X → F X ( ) by setting µ F X ( x ) = 〈 x, ⊥〉 .

Note that the relations σ ∈ F n ( ), σ &lt; F n ( ) τ , F h ( )( σ ) = τ with h : n → m , a = supp F n ( σ ) and σ = µ F n ( m ) are ∆ -definable in 0 1 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 &lt; 1+ X x in the definition of F X ( ) is crucial for the latter):

Lemma 2.4 ( 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 µ F (or rather its restriction to the category of natural numbers) gives rise to a family of functions D µ F X : X → D F ( X ), as defined by equation (3). For later use, we relate these to the functions µ F X : X → F X ( ).

Lemma 2.5 ( RCA . 0 ) For each order X we have an isomorphism

$$\eta _ { X } \colon D ^ { F } ( X ) \xrightarrow { \cong } F ( X )$$

with η X ◦ D µ F X = µ F X .

Proof. Recall that D F ( X ) consists of pairs 〈 a, σ 〉 , where a is a finite suborder of X and σ ∈ F ( | a | ) satisfies supp F | a | ( σ ) = | a | . We set

$$\eta _ { X } ( \langle a, \sigma \rangle ) = F ( \text{en} _ { a } ) ( \sigma ),$$

writing en a : | a | → 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 η X is an embedding, as in the proof of [4, Proposition 2.1]: Given

sets Y ⊆ Z , we agree to write ι Z Y : Y ↪ → Z for the inclusion. Assume that we have 〈 a, σ 〉 &lt; D F ( X ) 〈 b, τ 〉 , and note that this amounts to

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

Given a finite order c , we write en 0 c : | c | → c for the increasing enumeration. For the function en a : a → X from above, the definition of | · | yields

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

Since F ι ( X a ∪ b ◦ en 0 a ∪ b ) is an embedding, the above inequality implies

$$\eta _ { X } ( \langle a, \sigma \rangle ) = F ( \text{en} _ { a } ) ( \sigma ) = F ( \iota _ { a \cup b } ^ { X } \circ \text{en} _ { a \cup b } ^ { 0 } ) \circ F ( | \iota _ { a } ^ { a \cup b } | ) ( \sigma ) < _ { F ( X ) } \\ < _ { F ( X ) } F ( \iota _ { a \cup b } ^ { X } \circ \text{en} _ { a \cup b } ^ { 0 } ) \circ F ( | \iota _ { b } ^ { a \cup b } | ) ( \tau ) = \eta _ { X } ( \langle b, \tau \rangle ).$$

/negationslash

This confirms that η X is an embedding and in particular injective. It remains to show surjectivity. As a representative example, consider 〈 x, y 〉 ∈ F X ( ) with y = ⊥ . According to Definition 2.3 we must have y &lt; X x . Hence a := { x, y } has two elements, and the function en a : 2 → X has values en a (0) = y and en (1) = a x . Since σ := 〈 1 0 , 〉 ∈ F (2) satisfies supp F 2 ( σ ) = { 0 1 , } = 2, we get 〈 a, σ 〉 ∈ D F ( X ).

By construction we have

$$\eta _ { X } ( \langle a, \sigma \rangle ) = F ( \text{en} _ { a } ) ( \langle 1, 0 \rangle ) = \langle \text{en} _ { a } ( 1 ), ( 1 + \text{en} _ { a } ) ( 0 ) \rangle = \langle x, y \rangle.$$

A similar argument shows that the image of η X contains ⊥ and all elements of the form 〈 x, ⊥〉 . In order to verify the remaining claim we consider x ∈ X and write en { x } : 1 → X for the function with range { x } . In view of equation (3) we obtain

$$\eta _ { X } \circ D _ { X } ^ { \mu ^ { F } } ( x ) = \eta _ { X } ( \langle \{ x \}, \mu _ { 1 } ^ { F } ( 0 ) \rangle ) & = F ( \text{en} _ { \{ x \} } ) ( \langle 0, \perp \rangle ) = \\ & = \langle \text{en} _ { \{ x \} } ( 0 ), ( 1 + \text{en} _ { \{ x \} } ) ( \perp \rangle ) = \langle x, \perp \rangle = \mu _ { X } ^ { F } ( x ), \\ \text{as required.}$$

as required.

The normal function f from the introduction satisfies f ( α ) ≤ (1 + α ) 2 . We can now recover this result on the level of the prae-dilator F .

Lemma 2.6 ( 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 ( ) \{⊥} as a suborder of (1 + X ) 2 . In order to obtain the desired embedding it suffices to map ⊥ ∈ F X ( ) to the minimum element 〈⊥ ⊥〉 ∈ , (1 + X ) 2 . This is possible because 〈⊥ ⊥〉 , does not lie in the suborder F X ( ) \{⊥} , due to the condition y &lt; 1+ X x in Definition 2.3. /square

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

Corollary 2.7 ( 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 × Y of wellorders is well-founded goes through in RCA 0 : Assume that there is a strictly decreasing sequence ( 〈 x , y n n 〉 ) n ∈ N in X × Y . Then the sequence ( x n n ) ∈ N is nonincreasing. Since X is well-founded, there is an N ∈ N such that x n = x N holds for all n ≥ N (otherwise a strictly decreasing sequence in X could be constructed by

recursion). Then ( y n n ) ≥ N is a strictly decreasing sequence in Y , which contradicts the assumption that Y is well-founded. /square

## 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 α ≤ f ′ ( α ) from the introduction can be recovered in RCA 0 . Finally, we conclude that the base theory in a result of Rathjen and the present author can be lowered from

## ACA 0 to RCA 0 .

If g ′ is the derivative of a normal function g , then we have g ◦ g ′ = g ′ . To formulate this condition in second order arithmetic, we need to define the composition T ◦ 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

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

One can equip T ◦ 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

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

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

$$f _ { T \circ S } ( \alpha ) = \text{otp} ( D ^ { T \circ S } ( \alpha ) ) = \text{otp} ( D ^ { T } \circ D ^ { S } ( \alpha ) ) = \text{otp} ( D ^ { T } ( f _ { S } ( \alpha ) ) ) = f _ { T } \circ f _ { S } ( \alpha ),$$

where the third equality relies on D S ( α ) ∼ = otp( D S ( α )) = f S ( α ) 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, µ T ) and S = ( S, µ S ) are normal prae-dilators, then we can invoke equation (3) to define µ T ◦ S n : n → ( T ◦ S )( n ) by

$$\mu _ { n } ^ { T \circ S } = D _ { S ( n ) } ^ { \mu ^ { T } } \circ \mu _ { n } ^ { S }.$$

In [5, Lemma 2.16] it has been verified that this turns T ◦ S into a normal praedilator, and that we have

$$D _ { X } ^ { \mu ^ { T \circ S } } = \zeta _ { X } ^ { T, S } \circ D _ { D ^ { S } ( X ) } ^ { \mu ^ { T } } \circ D _ { X } ^ { \mu ^ { S } }.$$

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

Definition 3.1 ( 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 ξ : T ◦ S ⇒ S that satisfies ξ ◦ µ T ◦ S = µ S .

According to [5, Lemma 2.19], the natural transformation ξ can be extended into a family of order embeddings D ξ X : D T ◦ S ( X ) → D S ( X ) with

$$D _ { X } ^ { \xi } \circ D _ { X } ^ { \mu ^ { T \circ S } } = D _ { X } ^ { \mu ^ { S } }.$$

If S is a dilator, then the embedding D ξ α witnesses

$$f _ { T } \circ f _ { S } ( \alpha ) = \text{otp} ( D ^ { T \circ S } ( \alpha ) ) \leq \text{otp} ( D ^ { S } ( \alpha ) ) = f _ { S } ( \alpha ),$$

for any ordinal α . 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 ( RCA . 0 ) Assume that G and ξ : F ◦ G ⇒ 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

$$\xi _ { X } ^ { F } \coloneqq D _ { X } ^ { \xi } \circ \zeta _ { X } ^ { F, G } \circ \eta _ { D ^ { G } ( X ) } ^ { - 1 } \colon F ( D ^ { G } ( X ) ) \to D ^ { G } ( X ).$$

According to Definition 2.2, the normal prae-dilator G comes with a natural transformation µ G . The latter extends into an embedding D µ G X : X → D G ( X ), by equation (3). The values of the desired embedding

$$J \colon 2 ^ { X } \rightarrow D ^ { G } ( X )$$

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

$$( 6 ) \quad \ J ( \langle x _ { 1 }, \dots, x _ { n } \rangle ) < _ { D ^ { G } ( X ) } D _ { X } ^ { \mu ^ { G } } ( x ) \quad \text{if we have } x _ { 1 } < _ { X } x \text{ or } n = 0.$$

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 ξ F X ( ⊥ ∈ ) 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 Π 0 1 (note that (6) involves a universal quantification over x ). Since Σ -induction and Π -induction 0 1 0 1 are equivalent (see e.g. [15, Corollary II.3.10]), this shows that the induction can be carried out in RCA 0 . Let us now specify the details: For the base of the recursion we use the minimum element ⊥ of F D ( G ( X )) and set

$$J ( \langle \rangle ) = \xi _ { X } ^ { F } ( \perp ).$$

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

$$D _ { X } ^ { \mu ^ { G } } ( x ) = D _ { X } ^ { \xi } \circ D _ { X } ^ { \mu ^ { F \circ G } } ( x ) = D _ { X } ^ { \xi } \circ \zeta _ { X } ^ { F, G } \circ D _ { D ^ { G } ( X ) } ^ { \mu ^ { F } } \circ D _ { X } ^ { \mu ^ { G } } ( x ) =$$

$$& D _ { X } ^ { \mu ^ { G } } ( x ) = D _ { X } ^ { \xi } \circ D _ { X } ^ { \mu ^ { F \circ G } } ( x ) = D _ { X } ^ { \xi } \circ \zeta _ { X } ^ { F, G } \circ D _ { D ^ { G } ( X ) } ^ { \mu ^ { F } } \circ D _ { X } ^ { \mu ^ { G } } ( x ) = \\ & = D _ { X } ^ { \xi } \circ \zeta _ { X } ^ { F, G } \circ \eta _ { D ^ { G } ( X ) } ^ { - 1 } \circ \mu _ { D ^ { G } ( X ) } ^ { F } \circ D _ { X } ^ { \mu ^ { G } } ( x ) = \xi _ { X } ^ { F } \circ \mu _ { D ^ { G } ( X ) } ^ { F } \circ D _ { X } ^ { \mu ^ { G } } ( x ) = \xi _ { X } ^ { F } ( \langle D _ { X } ^ { \mu ^ { G } } ( x ), \perp ) ).$$

In view of ⊥ &lt; F D ( G ( X )) 〈 D µ G X ( x , ) ⊥〉 we get J ( 〈〉 ) &lt; D G ( X ) D µ G X ( x ) for any x ∈ X , as required by condition (6). In the recursion step we put

$$J ( \langle x _ { 0 }, \dots, x _ { n } \rangle ) = \xi _ { X } ^ { F } ( \langle D _ { X } ^ { \mu ^ { G } } ( x _ { 0 } ), J ( \langle x _ { 1 }, \dots, x _ { n } \rangle ) \rangle ).$$

To see that the argument 〈 D µ G X ( x 0 ) , J ( 〈 x , . . . , x 1 n 〉 〉 ) does indeed lie in the domain F D ( G ( X )) of ξ F X , we must establish the condition J ( 〈 x , . . . , x 1 n 〉 ) &lt; D G ( X ) D µ G X ( x 0 ) from Definition 2.3. By the definition of the order 2 X we have x 1 &lt; 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 &lt; X x we have

D µ G X ( x 0 ) &lt; D G ( X ) D µ G X ( x ). Together with the definition of J ( 〈 x , . . . , x 0 n 〉 ) and the equality D µ G X ( x ) = ξ F X ( 〈 D µ G X ( x , ) ⊥〉 ) from above, this does indeed imply the condition J ( 〈 x , . . . , x 0 n 〉 ) &lt; D G ( X ) D µ G X ( x ). It remains to show that J is an order embedding. We establish

$$\sigma < _ { 2 ^ { X } } \tau \ \Rightarrow \ J ( \sigma ) < _ { D ^ { G } ( X ) } J ( \tau )$$

by joint induction on σ and τ (or by induction on the length of τ , which leads to an induction statement of complexity Π ). Let us first assume that we have 0 1

$$\sigma = \langle \rangle < _ { 2 ^ { x } } \langle y _ { 0 }, \dots, y _ { m } \rangle = \tau$$

with τ = 〈〉 . Since ⊥ ∈ F D ( G ( X )) is minimal we do indeed get

/negationslash

$$J ( \sigma ) = \xi _ { X } ^ { F } ( \bot ) < _ { D ^ { G } ( X ) } \xi _ { X } ^ { F } ( \langle D _ { X } ^ { \mu ^ { G } } ( y _ { 0 } ), J ( \langle y _ { 1 }, \dots, y _ { m } \rangle ) \rangle ) ) = J ( \tau ).$$

Now consider an inequality

$$\sigma = \langle x _ { 0 }, \dots, x _ { n } \rangle < _ { 2 } x \, \langle y _ { 0 }, \dots, y _ { m } \rangle = \tau.$$

We must either have x 0 &lt; X y 0 , or x 0 = y 0 and 〈 x , . . . , x 1 n 〉 &lt; 2 X 〈 y , . . . , y 1 m 〉 . If the latter holds, then we get J ( 〈 x , . . . , x 1 n 〉 ) &lt; D G ( X ) J ( 〈 y , . . . , y 1 m 〉 ) by the induction hypothesis. In either case we obtain

$$\langle D _ { X } ^ { \mu ^ { G } } ( x _ { 0 } ), J ( \langle x _ { 1 }, \dots, x _ { n } \rangle ) \rangle < _ { F ( D ^ { G } ( X ) ) } \langle D _ { X } ^ { \mu ^ { G } } ( y _ { 0 } ), J ( \langle y _ { 1 }, \dots, y _ { m } \rangle ) \rangle.$$

By applying ξ F to both sides we get J σ ( ) &lt; G J τ ( ). /square

X D ( X )

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 ( RCA . 0 ) Assume that any normal dilator T has an upper derivative ( S, ξ ) 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 ξ : F ◦ G ⇒ 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. /square

↦

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 ( ∂T,ξ T ) of a given normal prae-dilator T . The transformation of T into ∂T and ξ T can be implemented in RCA 0 (in particular it is computable). Hence RCA 0 proves that (upper) derivatives exist. What RCA 0 cannot show is that X → D ∂T ( X ) preserves well-foundedness when X → D T ( X ) does. Indeed, Rathjen and the present author have shown that the latter is equivalent to Π 1 1 -bar induction (which asserts that Π -induction is available along any 1 1 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 ACA 0 ).

↦

## Corollary 3.4 ( RCA . 0 ) The following are equivalent:

- (1) If T is a normal dilator, then so is ∂T .
- (2) Any normal dilator T has an upper derivative ( S, ξ ) such that S is a dilator.
- (3) The principle of Π 1 1 -bar induction holds.

Proof. To see that (1) implies (2) it suffices to know that ∂T and ξ T form an upper derivative of T . This holds by [5, Proposition 4.11], which was proved in RCA 0 . The implication from (2) to (3) holds over 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 RCA 0 . The implication from (3) to (1) holds by [5, Theorem 5.8], which was established in RCA 0 . /square

Combining Corollaries 3.4 and 3.3 yields a somewhat indirect proof that Π 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 ′ ( α ) = ω ω α . We also specify a normal function g with g α ( ) ≤ 1 + α · 2 and g ′ ( α ) = ω 1+ α . 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 ( α ) = 1+ ∑ γ&lt;α (1+ γ ), or more formally by the recursive clauses

$$\nu _ { \alpha < \lambda }.$$

$$f ( 0 ) & = 1, \\ f ( \alpha + 1 ) & = f ( \alpha ) + 1 + \alpha, \\ f ( \lambda ) & = \sup _ { \alpha < \lambda } f ( \alpha ) \quad \text{ for } \lambda \, \lim i t.$$

Recall that α &gt; 0 is multiplicatively (resp. additively) principal if β, γ &lt; α implies β · γ &lt; α (resp. β + γ &lt; α ). The following determines the derivative of f .

Lemma 4.1. We have f ( α ) = α if and only if α is a multiplicatively principal limit ordinal.

Proof. Assume that f ( α ) = α holds. In view of f (1) &gt; f (0) = 1 we get α &gt; 1. By the definition of f we also see that 0 &lt; β &lt; α implies

$$\beta + 1 \leq f ( \beta ) + 1 < f ( \beta ) + 1 + \beta = f ( \beta + 1 ) \leq f ( \alpha ) = \alpha,$$

so that α is a limit. We can now infer that α is additively principal: Consider β, γ &lt; α and set δ := max { β, γ } . Since α is a limit, we get δ +1 &lt; α and then

$$\beta + \gamma \leq f ( \delta ) + 1 + \delta = f ( \delta + 1 ) < f ( \alpha ) = \alpha.$$

By a straightforward induction on γ we get β · γ ≤ f ( β + γ ). Since α is additively principal, it follows that β, γ &lt; α implies

$$\beta \cdot \gamma \leq f ( \beta + \gamma ) < f ( \alpha ) = \alpha.$$

Now assume that α is a multiplicatively (and hence additively) principal limit ordinal. Then γ &lt; α implies 1 + γ 2 &lt; α . In the introduction we have noted that f ( γ ) is bounded by 1 + γ 2 . Hence we get

$$f ( \alpha ) = \sup _ { \gamma < \alpha } f ( \gamma ) \leq \sup _ { \gamma < \alpha } ( 1 + \gamma ^ { 2 } ) \leq \alpha.$$

The inequality α ≤ f ( α ) is automatic, since f is strictly increasing.

The derivative of f can now be described as follows:

Corollary 4.2. We have f ′ ( α ) = ω ω α for any ordinal α .

/square

↦

Proof. It is known that an infinite ordinal is multiplicatively principal if and only if it is of the form ω ω α (see e. g. [12, Exercise 3.3.15]). Hence the previous lemma implies that α → ω ω α is the increasing enumeration of the fixed points of f . The claim follows by the definition of the derivative. /square

In the rest of this section we construct a normal function g with g ′ ( α ) = ω 1+ α . Such a function can be defined by

$$g ( 0 ) & = 1, \\ g ( \alpha + 1 ) & = ( \alpha + 1 ) \cdot 2, \\ g ( \lambda ) & = \sup _ { \alpha < \lambda } g ( \alpha ) \quad \text{for } \lambda \, \lim i t. \\ \cdot \, \. \, \. \, \. \, \.$$

By induction on the limit ordinal λ we get

$$g ( \lambda ) \leq \sup _ { \alpha < \lambda } \alpha \cdot 2 \leq \lambda \cdot 2.$$

In particular we have g λ ( ) &lt; g λ ( + 1), which readily implies that g is strictly increasing. We also obtain g α ( ) ≤ 1 + α · 2 for any ordinal α , as promised above. To characterize the derivative of g we show the following:

Lemma 4.3. We have g α ( ) = α if and only if α is an additively principal limit ordinal.

Proof. First assume that we have g α ( ) = α . In view of g (0) = 1 we get α &gt; 0. Since g γ ( +1) &gt; γ +1 holds for any successor, we learn that α must be a limit. In order to show that α is additively principal we consider arbitrary ordinals β, γ &lt; α . Setting δ := max { β, γ } , we get

$$\beta + \gamma < ( \delta + 1 ) \cdot 2 = g ( \delta + 1 ) \leq g ( \alpha ) = \alpha.$$

Conversely, assume that α is an additively principal limit ordinal. Then γ &lt; α implies γ · 2 &lt; α , which yields

$$g ( \alpha ) \leq \sup _ { \gamma < \alpha } \gamma \cdot 2 \leq \alpha.$$

Yet again, the inequality α ≤ g α (

) is automatic. /square

We can now describe the derivative of g :

Corollary 4.4. We have g ′ ( α ) = ω 1+ α for any ordinal α .

Proof. It is well-known that an ordinal is additively principal if and only if it is of the form ω α (consider Cantor normal forms). Excluding ω 0 = 1, we see that the additively principal limit ordinals are those of the form ω 1+ α . Now the claim follows by the previous lemma. /square

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 α ( +1) can be written as β or ( α + 1) + β with β &lt; α + 1, which suggests a relativized ordinal notation system. Canonical representations for elements of g λ ( ) appear less obvious when λ is a limit. For example, the ordinal ω +2 ∈ g ω ( · 2) could be written as ( ω + 1) + 1 ∈ g ω ( + 1), as ( ω + 2) + 0 ∈ g ω ( + 2) or as ω + 2 ∈ g ω ( + 3). It would be interesting to know whether g does have a reasonable representation as a normal dilator.

## References

- 1. Peter Aczel, Mathematical Problems in Logic , PhD thesis, Oxford, 1966.
- 2. , Normal functors on linear orderings , Journal of Symbolic Logic 32 (1967), p. 430, abstract to a paper presented at the annual meeting of the Association for Symbolic Logic, Houston, Texas, 1967.
- 3. Anton Freund, Type-Two Well-Ordering Principles, Admissible Sets, and Π 1 1 -Comprehension , PhD thesis, University of Leeds, 2018, available via http://etheses.whiterose.ac.uk/20929/ .
- 4. , Computable aspects of the Bachmann-Howard principle , Journal of Mathematical Logic 20 (2020), no. 2, article no. 2050006, 26 pp.
- 5. Anton Freund and Michael Rathjen, Derivatives of normal functions in reverse mathematics , Annals of Pure and Applied Logic 172 (2021), no. 2, article no. 102890, 49 pp.
- 6. Jean-Yves Girard, Π 1 2 -logic, part 1: Dilators , Annals of Pure and Applied Logic 21 (1981), 75-219.
- 7. , Proof Theory and Logical Complexity, Volume I , Studies in Proof Theory, Bibliopolis, Napoli, 1987.
- 8. Jeffry L. Hirst, Reverse mathematics and ordinal exponentiation , Annals of Pure and Applied Logic 66 (1994), 1-18.
- 9. , Ordinal inequalities, transfinite induction, and reverse mathematics , The Journal of Symbolic Logic 64 (1999), no. 2, 769-774.
- 10. Saunders Mac Lane, Categories for the Working Mathematician , 2 nd ed., Graduate Texts in Mathematics, vol. 5, Springer, 1998.
- 11. Alberto Marcone and Antonio Montalb´n, a The Veblen functions for computability theorists , Journal of Symbolic Logic 76 (2011), 575-602.
- 12. Wolfram Pohlers, Proof Theory. The First Step into Impredicativity , Springer, Berlin, 2009.
- 13. Michael Rathjen and Pedro Francisco Valencia Vizca´ ıno, Well ordering principles and bar induction , Gentzen's centenary: The quest for consistency (Reinhard Kahle and Michael Rathjen, eds.), Springer, Berlin, 2015, pp. 533-561.
- 14. Kurt Sch¨tte, u Proof Theory , Grundlehren der Mathematischen Wissenschaften, vol. 225, Springer, Berlin, 1977.
- 15. Stephen G. Simpson, Subsystems of Second Order Arithmetic , Perspectives in Logic, Cambridge University Press, 2009.

Fachbereich Mathematik, Technische Universit¨t Darmstadt, Schlossgartenstr. 7, a 64289 Darmstadt, Germany

Email address : freund@mathematik.tu-darmstadt.de
Anton Freund
A note on ordinal exponentiation and derivatives of normal functions
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}$.