Derivatives of normal functions in reverse mathematics

TL;DR

This paper explores the derivative of normal functions on ordinals within reverse mathematics, establishing the logical strength needed for their well-foundedness preservation, linking it to significant subsystems like ACA₀.

Contribution

It provides a new construction of derivatives of normal dilators and characterizes the logical strength of their well-foundedness preservation in reverse mathematics.

Findings

Existence and properties of derivatives are provable in RCA₀.

Preservation of well-foundedness by derivatives is equivalent to ACA₀.

Main result links well-foundedness preservation to Pi¹₁-bar induction.

Abstract

Consider a normal function $f$ on the ordinals (i. e. a function $f$ that is strictly increasing and continuous at limit stages). By enumerating the fixed points of $f$ we obtain a faster normal function $f'$, called the derivative of $f$. The present paper investigates this important construction from the viewpoint of reverse mathematics. Within this framework we must restrict our attention to normal functions $f:\aleph_1\rightarrow\aleph_1$ that are represented by dilators (i. e. particularly uniform endofunctors on the category of well-orders, as introduced by J.-Y. Girard). Due to a categorical construction of P. Aczel, each normal dilator $T$ has a derivative $\partial T$. We will give a new construction of the derivative, which shows that the existence and fundamental properties of $\partial T$ can already be established in the theory $\mathbf{RCA}_0$. The latter does not prove, however, that $\partial T$ preserves well-foundedness. Our main result shows that the statement ``for every normal dilator $T$, its derivative $\partial T$ preserves well-foundedness'' is $\mathbf{ACA}_0$-provably equivalent to $\Pi^1_1$-bar induction (and hence to $\Sigma^1_1$-dependent choice and to $\Pi^1_2$-reflection for $\omega$-models).

Equations

$$\phi (\gamma )\leftrightarrow \text{“Tγ is well-founded"}.$$

$${\forall }_{\beta <\gamma }\text{“Tβ is well-founded"}\to \text{“Tγ is well-founded"}.$$

$${\forall }_{\beta <\gamma }\mathrm{otp}({\mathcal{T}}_{\beta })\le \delta \to \mathrm{otp}({\mathcal{T}}_{\gamma })\le h(\gamma ,\delta )$$

$$\mathrm{otp}({\mathcal{T}}_{\gamma })\le g(\gamma +1)$$

$$\mathrm{otp}({\mathcal{T}}_{\gamma })\le h(\gamma ,g(\gamma ))\le h_0(g(\gamma ))\le f(g(\gamma )+1)\le f(g(\gamma +1))=g(\gamma +1).$$

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

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

$$X\upharpoonright x=\{x^{\prime }\in X|x^{\prime }{<}_{X}x\}$$

$${\mathrm{en}}_b\circ |f|=f\circ {\mathrm{en}}_a.$$

$$|{\mathrm{supp}}_n^T(\sigma )|\stackrel{\text{mathmakebox}[2em]{\mathrm{en}}_{\sigma }}{\to }{\mathrm{supp}}_n^T(\sigma )\stackrel{\text{mathmakebox}[2em]{\iota }_{\sigma }}{\hookrightarrow }n=\{0,\dots ,n-1\}$$

$$T^0$$

$$T^1$$

$${\mathrm{supp}}^T=\{⟨n,\sigma ,a⟩|{\mathrm{supp}}_n^T(\sigma )=a\}.$$

$${\omega }^X=\{⟨x_{k-1},\dots ,x_0⟩|x_0{\le }_X\cdots {\le }_X{x}_{k-1}\}$$

$${\omega }^f(⟨x_{k-1},\dots ,x_0⟩)=⟨f(x_{k-1}),\dots ,f(x_0)⟩.$$

$${\mathrm{supp}}_X^{\omega }(⟨x_{k-1},\dots ,x_0⟩)=\{x_{k-1},\dots ,x_0\},$$

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

$$⟨a,\sigma ⟩{<}_{D_X^T}⟨b,\tau ⟩\iff T_{|{\iota }_a^{a\cup b}|}(\sigma ){<}_{T_{|a\cup b|}}{T}_{|{\iota }_b^{a\cup b}|}(\tau ),$$

$$D_f^T(⟨a,\sigma ⟩)=⟨[f{]}^{<\omega }(a),\sigma ⟩.$$

$${\mathrm{supp}}_X^{D^T}(⟨a,\sigma ⟩)=a$$

$${\iota }_{⟨a,\sigma ⟩}:{\mathrm{supp}}_X^{D^T}(⟨a,\sigma ⟩)=a\hookrightarrow X$$

$${\eta }_n^T(⟨a,\sigma ⟩)=T_{{\iota }_a\circ {\mathrm{en}}_a}(\sigma ),$$

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

$$\begin{gathered} {\eta }_n^T(⟨a,\sigma ⟩)=T_{{\iota }_a\circ {\mathrm{en}}_a}(\sigma )=T_{{\iota }_{a\cup b}\circ {\mathrm{en}}_{a\cup b}}\circ T_{|{\iota }_a^{a\cup b}|}(\sigma ){<}_{T_n} \\ {<}_{T_n}{T}_{{\iota }_{a\cup b}\circ {\mathrm{en}}_{a\cup b}}\circ T_{|{\iota }_b^{a\cup b}|}(\tau )=T_{{\iota }_b\circ {\mathrm{en}}_b}(\tau )={\eta }_n^T(⟨b,\tau ⟩). \end{gathered}$$

$$f\circ {\iota }_a\circ {\mathrm{en}}_a={\iota }_{[f{]}^{<\omega }(a)}\circ {\mathrm{en}}_{[f{]}^{<\omega }(a)},$$

$$\begin{gathered} {\eta }_m^T\circ D_f^T(⟨a,\sigma ⟩)={\eta }_m^T(⟨[f{]}^{<\omega }(a),\sigma ⟩)=T_{{\iota }_{[f{]}^{<\omega }(a)}\circ {\mathrm{en}}_{[f{]}^{<\omega }(a)}}(\sigma )= \\ =T_f\circ T_{{\iota }_a\circ {\mathrm{en}}_a}(\sigma )=T_f\circ {\eta }_n^T(⟨a,\sigma ⟩). \end{gathered}$$

$$[{\iota }_a\circ {\mathrm{en}}_a{]}^{<\omega }({\mathrm{supp}}_{|a|}^T({\sigma }_0))={\mathrm{supp}}_n^T(T_{{\iota }_a\circ {\mathrm{en}}_a}({\sigma }_0))={\mathrm{supp}}_n^T(\sigma )=a$$

$$T_n=\{0,\dots ,n-1\}\cup \{\Omega \}$$

$$T_f(\sigma )=\{\begin{array}{ll}f(\sigma )& \text{if σ∈{0,…,n−1}},\\ \Omega & \text{if σ=Ω},\end{array}{\mathrm{supp}}_n^T(\sigma )=\{\begin{array}{ll}\{\sigma \}& \text{if σ∈{0,…,n−1}},\\ \varnothing & \text{if σ=Ω}.\end{array}$$

$$D_X^T=\{⟨\{x\},0⟩|x\in X\}\cup \{⟨\varnothing ,\Omega ⟩\}\text{(with 0∈1⊆T1 and Ω∈T0)}$$

$$X\upharpoonright x=\{y\in X|y{<}_{X}x\},$$

$$a{<}_X^{\mathrm{fin}}b\iff {\forall }_{x\in a}{\exists }_{y\in b}x{<}_{X}y.$$

Full text

††footnotetext: © 2020. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/. It is the accepted version of a paper published in the Annals of Pure and Applied Logic 172(2) 2021, article no. 102890, 49 pp., doi:10.1016/j.apal.2020.102890.

1. Introduction

For the purpose of this paper, a normal function is a function $f:\aleph_{1}\rightarrow\aleph_{1}$ that is strictly increasing and continuous at limit stages, i. e. we demand that

1. (i)

$\alpha<\beta$ implies $f(\alpha)<f(\beta)$ and that 2. (ii)

$f(\lambda)=\sup_{\alpha<\lambda}f(\alpha)$ holds for any limit ordinal $\lambda$.

Equivalently, $f$ is the unique strictly increasing enumeration of a closed and unbounded (club) subset of $\aleph_{1}$. It is easy to see that the fixed points of any normal function $f$ do again form an $\aleph_{1}$-club. The normal function that enumerates these fixed points is called the derivative of $f$ and is denoted by $f^{\prime}$. Let us agree to call a normal function $g$ an upper derivative of $f$ if $f(g(\alpha))=g(\alpha)$ holds for any ordinal $\alpha<\aleph_{1}$. Note that such a function $g$ must majorize the derivative $f^{\prime}$ of $f$. As an example we consider the function $f(\alpha)=\omega^{\alpha}$ from ordinal arithmetic. In this case $f^{\prime}(\alpha)=\varepsilon_{\alpha}$ is the $\alpha$-th $\varepsilon$-number. The notion of normal function plays an important role in proof theory (see e. g. [19, Chapter V]) and has interesting computability-theoretic properties (due to [16]). More generally, one can consider normal functions on the class of ordinals. A fundamental example from set theory is the function $f(\alpha)=\aleph_{\alpha}$ that enumerates the infinite cardinals. However, such normal functions are beyond the scope of the present paper.

The above construction of derivatives via clubs uses the fact that $\aleph_{1}$ is a regular cardinal. One can also build derivatives by transfinite recursion, which relies on collection or replacement. In the present paper we construct derivatives in a much weaker setting. In very informal terms, we show that the following statements are equivalent over a suitable base theory:

1. (10)

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

Every normal function has an upper derivative. 3. (30)

Transfinite induction holds for any $\Pi^{1}_{1}$-formula.

To establish this equivalence we will give precise sense to the following argument: To see that (10) implies (20) it suffices to observe that any derivative is an upper derivative. To prove the direction from (20) to (30) we must establish induction for a $\Pi^{1}_{1}$-formula $\varphi(\gamma)$ up to an arbitrary ordinal $\alpha$. Using the Kleene normal form theorem one obtains countable trees $\mathcal{T}_{\gamma}$ with

[TABLE]

The assumption that $\varphi$ is progressive along the ordinals can then be expressed as

[TABLE]

Assume that this statement is witnessed by a binary function $h$ on the ordinals, in the sense that we have

[TABLE]

for any ordinals $\gamma$ and $\delta$, where $\operatorname{otp}(\mathcal{T})$ denotes the order type of $\mathcal{T}$. To avoid the dependency on $\gamma$ we set $h_{0}(\delta)=\sup_{\gamma<\alpha}h(\gamma,\delta)$ (alternatively one could set $h_{0}(\delta)=\sup_{\gamma\leq\delta}h(\gamma,\delta)$, avoiding the reference to the fixed bound $\alpha$). Now form a normal function $f$ with $h_{0}(\delta)\leq f(\delta+1)$, e. g. by setting $f(\delta)=\sum_{\gamma<\delta}1+h_{0}(\gamma)$. Then statement (20) allows us to consider an upper derivative $g$ of $f$. Let us show that we have

[TABLE]

for all $\gamma<\alpha$. For $\beta<\gamma$ we may inductively assume $\operatorname{otp}(\mathcal{T}_{\beta})\leq g(\beta+1)\leq g(\gamma)$. By the above we obtain

[TABLE]

So $g$ witnesses that $\mathcal{T}_{\gamma}$ is well-founded for any $\gamma<\alpha$. This yields $\forall_{\gamma<\alpha}\varphi(\gamma)$, which is the conclusion of transfinite induction. To see that (30) implies (10) we will construct notation systems for the values $f^{\prime}(\alpha)$, relative to a given normal function $f$. The crucial fact that the notation system for $f^{\prime}(\alpha)$ is well-founded (and hence represents an ordinal) will be established by transfinite induction on $\alpha$.

In order to make the result from the previous paragraph precise we will use the framework of reverse mathematics. This research program uncovers equivalences between different mathematical and foundational statements in the language of second order arithmetic (see [21] for an introduction). As the base theory for our investigation we take $\mathbf{ACA}_{0}$. In second order arithmetic the above statement (30) corresponds to the following assertion:

1. (3)

Induction for $\Pi^{1}_{1}$-formulas is available along any countable well-order.

We will refer to this assertion as $\Pi^{1}_{1}$-bar induction, in order to distinguish it from the principle of transfinite induction along a specific (class- or set-sized) well-order. Let us recall that $\Pi^{1}_{1}$-bar induction is well-established in reverse mathematics: Simpson [20] has shown that it is equivalent to $\Sigma^{1}_{1}$-dependent choice and to $\Pi^{1}_{2}$-reflection for $\omega$-models, also over $\mathbf{ACA}_{0}$.

To formalize statements (10) and (20) in second-order arithmetic we will rely on J.-Y. Girard’s notion of dilator [12, 13]. For the purpose of the present paper, a (coded) prae-dilator is a particularly uniform functor $n\mapsto T_{n}$ from natural numbers to linear orders (full details can be found in Section 2 below). Girard has observed that the uniformity allows to extend $T$ beyond the natural numbers. In [6, 9] the first author has given a detailed description of linearly ordered notation systems $D^{T}_{X}$ that are computable in $T$ and the linear order $X$. This yields an endofunctor $X\mapsto D^{T}_{X}$ of linear orders, which one may call a class-sized prae-dilator. If $D^{T}_{X}$ is well-founded for every well-order $X$, then $T$ is called a (coded) dilator. In this case $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$ defines a function on the ordinals. A condition under which this function is normal has been identified by P. Aczel [1, 2] (even before Girard had introduced dilators in the full sense). This leads to a notion of normal prae-dilator, which will be defined in Section 2. In the same section we will characterize (upper) derivatives on the level of normal prae-dilators. Once all this is made precise, we can take the following as our formalization of statement (20) in second order arithmetic:

1. (2)

Any normal dilator $T$ has an upper derivative $S$ such that $X\mapsto D^{S}_{X}$ preserves well-foundedness (so that $S$ is again a normal dilator).

The advantage of this principle is that it is relatively easy to state and does not depend on a specific construction of derivatives. Its disadvantage is that it confounds the following two questions: How strong is the assertion that any normal dilator has an upper derivative? And how much strength is added by the demand that the upper derivative preserves well-foundedness? We want to disentangle these questions in our formalization of statement (10). To see how this works, let us recall that Aczel [1, 2] has explicitly constructed a derivative $\partial T$ of a given normal prae-dilator $T$. In Section 4 we will show that $\partial T_{n}$ can be represented by a term system. In view of this representation $\mathbf{RCA}_{0}$ proves that $\partial T$ exists and is a derivative of $T$. What $\mathbf{RCA}_{0}$ cannot show is that $D^{\partial T}$ preserves well-foundedness whenever $D^{T}$ does. This suggests to formalize statement (10) as the following assertion:

1. (1)

If $T$ is a normal dilator, then $D^{\partial T}_{X}$ is well-founded for any well-order $X$.

As $\mathbf{RCA}_{0}$ proves that any derivative is an upper derivative it will be immediate that (1) implies (2). This means that the entire strength of these two principles is concentrated in the preservation of well-foundedness, which answers the questions that we have raised after the formulation of principle (2).

Let us summarize the content of the following sections: As explained above, Section 2 introduces (upper) derivatives on the level of normal prae-dilators and gives a precise formalization of statement (2). In Section 3 we prove that (2) implies (3), by giving precise meaning to the argument from the beginning of this introduction. Section 4 contains the construction of $\partial T$ in $\mathbf{RCA}_{0}$, which yields the implication from (1) to (2). In Section 5 we prove that (3) implies (1), using $\Pi^{1}_{1}$-induction along $X$ to establish that $D^{\partial T}_{X}$ is well-founded. At the end of the paper we will thus have shown that (1), (2) and (3) are equivalent over $\mathbf{ACA}_{0}$ (see Theorem 5.9 for the official statement of this result). In a separate paper by the first author [11] it is shown that the base theory can be lowered to $\mathbf{RCA}_{0}$, since the existence of derivatives implies arithmetical comprehension. The first author has also shown that $\Pi^{1}_{1}$-induction along the natural numbers is equivalent to the weaker principle that every normal dilator has at least one well-founded fixed point [10].

The length of our paper is due to the fact that we wanted to be precise about the formalization of dilators in second order arithmetic. The text includes several informal summaries, so that the reader can follow the main lines of the argument without reading all technical verifications. To get a good first idea, we recommend to read Section 2 up to (and including) Summary 2.1, skip the rest of Section 2, and then read Section 3 up to Summary 3.5.

In the rest of this introduction we put our result into context. Let us first discuss implications for the predicative foundation of mathematics: The predicative stance originated with H. Weyl’s Das Kontinuum [23] from 1908, and may be characterized by the imposition of a constraint on set formation that countenances only that which is implicit in accepting the natural number structure as a completed totality. Based on a proposal due to G. Kreisel, the modern logical analysis of predicativity (given the natural numbers) was carried out by S. Feferman [5] and K. Schütte [18] in 1964. It is couched in terms of provability in an autonomous transfinite progression of ramified theories of sets which are based on classical logic and assume the existence of the set of natural numbers. The existence of further sets is regimented by a hierarchy of levels to be generated in an autonomous way. At each level, sets are asserted to exist only via definitions in which quantification over sets must be restricted to lower levels. The further condition of autonomy requires that one may ascend to a level $\alpha$ only if the existence of a well-ordering of order type $\alpha$ has been established at some level $\beta<\alpha$. Feferman and Schütte independently showed that the least non-autonomous ordinal for this progression of theories is the recursive ordinal $\Gamma_{0}$. Set-theoretically, the constructible sets up to $\Gamma_{0}$ form the minimal model of the aforementioned progression. A connection with our result arises because derivatives of normal functions (and transfinite hierarchies of derivatives) provide the intuition behind the usual notation system for $\Gamma_{0}$ (see e. g. [19]). This does not imply, however, that the abstract notion of derivative (relative to an arbitrary normal function) is predicatively acceptable. Indeed our result shows that it is not: We prove that the existence of normal functions is equivalent to $\Pi^{1}_{1}$-bar induction and hence to $\Sigma^{1}_{1}$-dependent choice (all over $\mathbf{ACA}_{0}$). Now the least ordinal $\tau$ such that the constructible sets up to $\tau$ form a model of $\Sigma^{1}_{1}$-dependent choice is the first non-recursive ordinal $\omega_{1}^{\operatorname{CK}}$ (see [15]), which is much larger than $\Gamma_{0}$. As a consequence, the principle of $\Sigma^{1}_{1}$-dependent choice does not possess a prima facie predicative justification. By the result of our paper the same applies to the principle that the derivative of every dilator preserves well-foundedness. On the other hand, all sufficiently concrete consequences of these principles hold in predicative mathematics: The extension of $\mathbf{ACA}_{0}$ by $\Sigma^{1}_{1}$-dependent choice is $\Pi^{1}_{2}$-conservative over the theory $\mathbf{(\Pi^{1}_{0}\textbf{-}CA)_{\omega^{\omega}}}$, which allows for $\omega^{\omega}$ iterations of arithmetical comprehension (due to A. Cantini [4]). The latter is a predicative theory in its entirety.

Let us also compare our result to a theorem of T. Arai [3]. Roughly speaking, this theorem states that the following are equivalent over $\mathbf{ACA}_{0}$:

• •

The order $D^{\partial T}_{X}$ is well-founded for every well-order $X$.

• •

Any set is contained in a countable coded $\omega$-model of the statement that “$D^{T}_{X}$ is well-founded for every well-order $X$”.

This formulation of Arai’s result should be read with quite some reservation: Arai does not represent normal functions by dilators. Instead his result relies on the assumption that we are given formulas that define term systems for $D^{T}_{X}$ and $D^{\partial T}_{X}$, which must satisfy certain conditions. In particular this approach does not allow to quantify over dilators, as required for our result. On an informal level Arai’s result can be read as a pointwise version of ours: Recall that $\Pi^{1}_{1}$-bar induction is equivalent to $\omega$-model reflection for $\Pi^{1}_{2}$-formulas. Assume that we want to establish this reflection principle for a formula $\varphi$. Girard has shown that the notion of dilator is $\Pi^{1}_{2}$-complete (see D. Norman’s proof in [14, Annex 8.E], which will also play an important role in Section 4 below). Thus one may hope to construct a normal prae-dilator $T$ such that $\varphi$ is equivalent to the statement that “$D^{T}_{X}$ is well-founded for every well-order $X$”. Using our principle (1) one could conclude that “$D^{\partial T}_{X}$ is well-founded for every well-order $X$”. By Arai’s result this would yield the desired $\omega$-models of $\varphi$. When we started working on the present paper we planned to derive the equivalence between (1), (2) and (3) from Arai’s result, by making the given argument precise. However, this has met with so many technical obstacles that it turned out easier to give a completely new proof.

To conclude this introduction we compare our result to a theorem of the first author [6, 7, 8, 9], which says that the following are equivalent over $\mathbf{RCA}_{0}$:

• •

Every dilator has a well-founded Bachmann-Howard fixed point.

• •

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

To explain what this means we point out that the first principle quantifies over arbitrary dilators $T$, rather than just over normal ones. This includes cases where we have $\operatorname{otp}(D^{T}_{\alpha})>\alpha$ for any ordinal $\alpha$, so that $D^{T}$ cannot have a well-founded fixed point. The best we can hope for is a function $\vartheta:D^{T}_{\alpha}\rightarrow\alpha$ that is “almost” order-preserving (see [7] for a precise definition). If such a function exists, then $\alpha$ is called a Bachmann-Howard fixed point of $T$. This name has been chosen since the conditions on $\vartheta$ are inspired by properties of the collapsing function used to define the Bachmann-Howard ordinal (cf. in particular [17]). It is worth noting that the notion of Bachmann-Howard fixed point is most interesting for dilators that are not normal (see the proof of [9, Proposition 3.3] for an instructive example). As is well-known, $\Pi^{1}_{1}$-comprehension is much stronger than $\Pi^{1}_{1}$-bar induction. Thus the results of [6] and the present paper help to explain why collapsing functions, rather than derivatives, are the crucial feature of strong ordinal notation systems.

Acknowledgements. We would like to thank the anonymous referee for their detailed comments, which have been very helpful in making our paper more readable.

2. Normal dilators in second order arithmetic

In the present section we define and investigate (prae-) dilators in the setting of reverse mathematics. Our approach is based on the work of Girard [12] and on details worked out by the first author [6, 9]. We will also characterize normal prae-dilators and their (upper) derivatives.

Let us fix some category-theoretic terminology: To turn the class of (countable) linear orders into a category we take the order embeddings (strictly increasing functions) as morphisms. The forgetful functor to the underlying set of an order will be left implicit. Conversely, a subset of an order will often be considered as a suborder. The finite subset functor $[\cdot]^{<\omega}$ on the category of sets is given by

[TABLE]

We will often write the arguments of a functor $T$ as subscripts, so that a morphism $f:X\rightarrow Y$ is transformed into $T_{f}:T_{X}\rightarrow T_{Y}$. When we want to avoid iterated subscripts we revert to the notation $T(f):T(X)\rightarrow T(Y)$.

Since the formalization of dilators in second order arithmetic is somewhat technical, we first give an informal summary. Guided by this summary, the reader can skim through the rest of the section without considering all technical details.

Summary 2.1**.**

In a sufficiently expressive meta-theory, a class-sized prae-dilator can be defined as a pair $(T,\operatorname{supp}^{T})$ of

• •

a functor $T$ from linear orders to linear orders and

• •

a natural transformation $\operatorname{supp}^{T}:T\Rightarrow[\cdot]^{<\omega}$ that satisfies the following support condition: for any order $X$, each element $\sigma\in T_{X}$ lies in the range of the morphism $T_{\iota_{\sigma}}$, where $\iota_{\sigma}:\operatorname{supp}^{T}_{X}(\sigma)\hookrightarrow X$ is the inclusion.

If $T_{X}$ is well-founded for every well-order $X$, then $T$ is called a class-sized dilator. The specification “class-sized” will often be omitted. It is instructive to consider Example 2.3 below. In [6, Remark 2.2.2] it has been verified that the given definition of dilator coincides with the original one by Girard [12]. However, our prae-dilators are not quite equivalent to Girard’s pre-dilators, as the latter must satisfy an additional monotonicity condition that is automatic in the well-founded case. Any dilator $T$ induces a function $\alpha\mapsto\operatorname{otp}(T_{\alpha})$ on the ordinals. To ensure that this function is normal one demands that $T$ preserves initial segments. More precisely, we write

[TABLE]

for an order $(X,<_{X})$ and $x\in X$. A normal (prae-) dilator consists of

• •

a (prae-) dilator $(T,\operatorname{supp}^{T})$ and

• •

a natural family of functions $\mu^{T}_{X}:X\to T_{X}$ with the following property: for any inclusion $\iota_{x}:X\!\restriction\!x\hookrightarrow X$, the morphism $T_{\iota_{x}}$ has range $T_{X}\!\restriction\!\mu^{T}_{X}(x)$.

If $T$ is a normal dilator, then $\alpha\mapsto\operatorname{otp}(T_{\alpha})$ is a normal function on the ordinals, as shown in Proposition 2.14 below. Recall that a normal function $g$ is an upper derivative of $f$ if we have $f\circ g(\alpha)=g(\alpha)$ for every ordinal $\alpha$. To ensure this equality it suffices to have an embedding of $f\circ g(\alpha)$ into $g(\alpha)$. In the categorical setting it is natural to demand compatible embeddings: A morphism between normal prae-dilators $(T,\mu^{T})$ and $(S,\mu^{S})$ is given by a natural transformation $\nu:T\Rightarrow S$ such that we have $\nu_{X}\circ\mu^{T}_{X}=\mu^{S}_{X}$ for any order $X$. Now an upper derivative of a normal prae-dilator $T$ can be defined as a pair $(S,\xi)$ of

• •

a normal prae-dilator $S$ and

• •

a morphism $\xi:T\circ S\Rightarrow S$ of normal prae-dilators.

The derivative of a normal function is the upper derivative with the smallest possible values. On the level of dilators this is naturaly expressed via the notion of initial object: Consider two upper derivatives $(S^{1},\xi^{1})$ and $(S^{2},\xi^{2})$ of a normal prae-dilator $T$. A morphism $\nu:S^{1}\Rightarrow S^{2}$ of normal prae-dilators is called a morphism of upper derivatives if we have $\nu_{x}\circ\xi^{1}_{X}=\xi^{2}_{X}\circ T_{\nu_{X}}$ for every order $X$. Now an upper derivative $(S,\xi)$ of $T$ is called a derivative if any other upper derivative $(S^{\prime},\xi^{\prime})$ admits a unique morphism $\nu:S\Rightarrow S^{\prime}$ of upper derivatives. Just as all initial objects, derivatives of normal prae-dilators are unique up to natural isomorphism. If $(S,\xi)$ is the derivative of a normal dilator $T$, then $\alpha\mapsto\operatorname{otp}(S_{\alpha})$ is the usual derivative of the normal function $\alpha\mapsto\operatorname{otp}(T_{\alpha})$, as we will show in Corollary 5.11. Together with the good categorical properties, this shows that we have found the “right” definition of derivative on the level of dilators.

In the rest of this section we make the previous summary precise and formalize it in reverse mathematics. The formalization relies on Girard’s observation that dilators are essentially determined by their restrictions to finite orders. Let us fix some terminology: The category of natural numbers consists of the finite orders $n=\{0,\dots,n-1\}$ (ordered as usual) and all embeddings between them. Note that this yields a small category that is equivalent to the category of all finite orders. The equivalence is witnessed by the increasing enumerations $\operatorname{en}_{a}:|a|\rightarrow a$, where $|a|=\{0,\dots,|a|-1\}$ denotes the cardinality of the finite order $a$. For each embedding $f:a\rightarrow b$ there is a unique increasing function $|f|:|a|\rightarrow|b|$ with

[TABLE]

Thus $|\cdot|$ and $\operatorname{en}$ become a functor and a natural isomorphism. We continue to use the finite subset functor $[\cdot]^{<\omega}$, even though $[n]^{<\omega}$ coincides with the full power set of $n=\{0,\dots,n-1\}$. Hereditarily finite sets with the natural numbers as urelements can be coded by natural numbers. It is straightforward to see that basic relations and operations on these sets are primitive recursive in the codes. This allows us to introduce the following notion in the theory $\mathbf{RCA}_{0}$, as in [9]:

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

A coded prae-dilator consists of

1. (i)

a functor $T$ from the category of natural numbers to the category of linear orders with fields $T_{n}\subseteq\mathbb{N}$ and 2. (ii)

a natural transformation $\operatorname{supp}^{T}:T\Rightarrow[\cdot]^{<\omega}$ such that any $\sigma\in T_{n}$ lies in the range of $T_{\iota_{\sigma}\circ\operatorname{en}_{\sigma}}$, where

[TABLE]

factors the unique morphism with range $\operatorname{supp}^{T}_{n}(\sigma)\subseteq n$.

More precisely, the functor $T$ is represented by the sets

[TABLE]

of natural numbers. The natural transformation $\operatorname{supp}^{T}$ is represented by the set

[TABLE]

Thus an expression such as $\sigma\in T_{n}$ is an abbreviation for $\langle 0,n,\sigma\rangle\in T^{0}$, which is a $\Delta^{0}_{1}$-formula in $\mathbf{RCA}_{0}$. The statement that $T$ is a coded prae-dilator is easily seen to be arithmetical in the sets $T^{0},T^{1},\operatorname{supp}^{T}\subseteq\mathbb{N}$.

Example 2.3**.**

For any order $X$ we consider the set

[TABLE]

with the lexicographic order (it may help to think of $\langle x_{k-1},\dots,x_{0}\rangle$ as the formal Cantor normal form $\omega^{x_{k-1}}+\dots+\omega^{x_{0}}$). To obtain a functor we map each morphism $f:X\rightarrow Y$ to the embedding $\omega^{f}:\omega^{X}\rightarrow\omega^{Y}$ with

[TABLE]

If we define $\operatorname{supp}^{\omega}_{X}:\omega^{n}\rightarrow[X]^{<\omega}$ by

[TABLE]

then we get a class-sized prae-dilator in the sense of Summary 2.1. Its restriction to the category of finite orders is a coded prae-dilator in the sense of Definition 2.2.

Let us discuss how the class-sized prae-dilator $X\mapsto\omega^{X}$ from the previous example can be reconstructed from its coded restriction. The idea is to view an element $\langle n_{k-1},\dots,n_{0}\rangle\in\omega^{n}$ as a term. In order to obtain an element of $\omega^{X}$, the “variables” $n_{i}$ in this term are substituted by elements $x_{i}\in X$, in increasing order. For example, the pair $\langle\{x_{0},x_{1}\},\langle 1,1,0\rangle\,\rangle$ with $x_{0}<x_{1}$ represents the element $\langle x_{1},x_{1},x_{0}\rangle\in\omega^{X}$. To make the representations unique we require that the variables are as small as possible. Thus $\langle\{x_{0},x_{1}\},\langle 3,3,1\rangle\,\rangle$ would not be a valid representation. In order to formulate this requirement in general we will rely on the observation that we have $\langle 1,1,0\rangle\in\omega^{2}=\omega^{|\{x_{0},x_{1}\}|}$. One should also demand that all given elements of $X$ are substituted for a variable. Thus $\langle\{x_{0},x_{1},x_{2}\},\langle 1,1,0\rangle\,\rangle$ with $x_{0}<_{X}x_{1}<_{X}x_{2}$ would not be a valid representation. This can be expressed via the condition $\operatorname{supp}^{\omega}_{|\{x_{0},x_{1}\}|}(\langle 1,1,0\rangle)=\{0,1\}=2=|\{x_{0},x_{1}\}|$. In general, the class-sized extension $D^{T}$ of a coded prae-dilator $T$ can be defined as follows (cf. [9]):

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

Consider a coded prae-dilator $T=(T,\operatorname{supp}^{T})$. For each order $X$ we define a set $D^{T}_{X}$ and a binary relation $<_{D^{T}_{X}}$ on $D^{T}_{X}$ by

[TABLE]

where $\iota_{a}^{a\cup b}:a\hookrightarrow a\cup b$ and $\iota_{b}^{a\cup b}:b\hookrightarrow a\cup b$ denote the inclusions between suborders of $X$. Given an embedding $f:X\rightarrow Y$, we define $D^{T}_{f}:D^{T}_{X}\rightarrow D^{T}_{Y}$ by

[TABLE]

To define a family of functions $\operatorname{supp}^{D^{T}}_{X}:D^{T}_{X}\Rightarrow[X]^{<\omega}$ we set

[TABLE]

for each order $X$.

In order to see that $D^{T}_{f}(\langle a,\sigma\rangle)$ still satisfies the uniqueness conditions (i. e. that we have $\sigma\in T_{|[f]^{<\omega}(a)|}$ and $\operatorname{supp}^{T}_{|[f]^{<\omega}(a)|}(\sigma)=|[f]^{<\omega}(a)|$) it suffices to note that $[f]^{<\omega}(a)$ has the same cardinality as $a$. The following shows that $D^{T}$ is a class-sized prae-dilator in the sense of Summary 2.1 (in part (ii) of the proposition one could replace $\iota_{\langle a,\sigma\rangle}$ by $\iota_{\langle a,\sigma\rangle}\circ\operatorname{en}_{a}$, since $\operatorname{en}_{a}:|a|\rightarrow a$ is an isomorphism).

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

If $T$ is a coded prae-dilator, then

1. (i)

the maps $X\mapsto(D^{T}_{X},<_{D^{T}_{X}})$ and $f\mapsto D^{T}_{f}$ form an endofunctor on the category of linear orders and 2. (ii)

the map $X\mapsto\operatorname{supp}^{D^{T}}_{X}$ is a natural transformation between $D^{T}$ and $[\cdot]^{<\omega}$, with the property that any $\langle a,\sigma\rangle\in D^{T}_{X}$ lies in the range of $D^{T}_{\iota_{\langle a,\sigma\rangle}}$, where

[TABLE]

is the inclusion.

Proof.

In [9, Lemma 2.4] the same has been shown in a stronger base theory (we point out that the uniqueness conditions are crucial for the linearity of $<_{D^{T}_{X}}$). It is straightforward to check that the proof goes through in $\mathbf{RCA}_{0}$. ∎

While $D^{T}$ is a class-sized object, its restriction $D^{T}\!\restriction\!\mathbb{N}$ to the category of natural numbers can be constructed in $\mathbf{RCA}_{0}$. The following is similar to [9, Proposition 2.5]. Nevertheless we give a detailed proof, since we want to refer to it later.

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

If $T$ is a coded prae-dilator, then so is $D^{T}\!\restriction\!\mathbb{N}$. In this case we get a natural isomorphism $\eta^{T}:D^{T}\!\restriction\!\mathbb{N}\Rightarrow T$ by setting

[TABLE]

where $\iota_{a}:a\hookrightarrow n$ is the inclusion.

Proof.

The previous proposition implies that $D^{T}\!\restriction\!\mathbb{N}$ is a coded prae-dilator. To see that $\eta^{T}_{n}$ is order preserving we consider an inequality $\langle a,\sigma\rangle<_{D^{T}_{n}}\langle b,\tau\rangle$. According to Definition 2.4 this amounts to $T_{|\iota_{a}^{a\cup b}|}(\sigma)<_{T_{|a\cup b|}}T_{|\iota_{b}^{a\cup b}|}(\tau)$. Write $\iota_{a\cup b}:a\cup b\hookrightarrow n$ and observe

[TABLE]

Applying $T_{\iota_{a\cup b}\circ\operatorname{en}_{a\cup b}}$ to both sides of the above inequality we obtain

[TABLE]

To establish naturality we consider an order preserving function $f:n\rightarrow m$. Write $\iota_{[f]^{<\omega}(a)}:[f]^{<\omega}(a)\hookrightarrow m$ and observe that we have

[TABLE]

as both sides are order isomorphisms between $|a|=|[f]^{<\omega}(a)|$ and $[f]^{<\omega}(a)\subseteq n$. We can deduce

[TABLE]

By the definition of coded prae-dilator any $\sigma\in T_{n}$ can be written as $\sigma=T_{\iota_{a}\circ\operatorname{en}_{a}}(\sigma_{0})$ with $a=\operatorname{supp}^{T}_{n}(\sigma)$ and $\sigma_{0}\in T_{|a|}$. In view of

[TABLE]

we have $\operatorname{supp}^{T}_{|a|}(\sigma_{0})=|a|$ and hence $\langle a,\sigma_{0}\rangle\in D^{T}_{n}$. Since $\eta^{T}_{n}(\langle a,\sigma_{0}\rangle)=\sigma$ holds by construction we can conclude that $\eta^{T}_{n}$ is surjective. ∎

As indicated in the introduction, the following notion plays a crucial role (there is no ambiguity since the two obvious definitions of well-foundedness are equivalent in $\mathbf{RCA}_{0}$, see e. g. [6, Lemma 2.3.12]):

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

A coded prae-dilator $T$ is called a coded dilator if $D^{T}_{X}$ is well-founded for every well-order $X$.

In a sufficiently expressive meta-theory, we can now discuss the reconstruction of a class-sized prae-dilator $T$. Assuming that $T$ preserves countability, we may assume $T_{n}\subseteq\mathbb{N}$ for every number $n$. Then the restriction $T\!\restriction\!\mathbb{N}$ is a coded prae-dilator. The equivalence from Lemma 2.6 is readily extended into a natural isomorphism between $D^{T\restriction\mathbb{N}}$ and $T$ (see [9, Proposition 2.5]). In view of $D^{T\restriction\mathbb{N}}_{X}\cong T_{X}$ it is immediate that $T\!\restriction\!\mathbb{N}$ is a coded dilator if $T$ is a class-sized dilator. The converse is somewhat more subtle, since Definition 2.7 only quantifies over well-orders with field $X\subseteq\mathbb{N}$. Girard [12, Theorem 2.1.15] has shown that it suffices to test the preservation of well-foundedness on countable orders. Thus it is true that $D^{T}$ is a class-sized dilator for any coded dilator $T$. In second order arithmetic we can consider the orders $T_{X}$ and the isomorphisms $D^{T\restriction\mathbb{N}}_{X}\cong T_{X}$ when $T$ is a specific class-sized prae-dilator with a computable construction. This can be useful when $T_{X}$ has a more transparent description than $D^{T\restriction\mathbb{N}}_{X}$ (as in the example above, where the term $\langle x_{1},x_{1},x_{0}\rangle\in\omega^{X}$ is more intelligible than the expression $\langle\{x_{0},x_{1}\},\langle 1,1,0\rangle\,\rangle\in D^{\omega}_{X}$). On the other hand, second order arithmetic cannot reason about class-sized prae-dilators in general (i. e. quantify over them). Thus we will mostly be concerned with coded prae-dilators, which are more important on a theoretical level. We will often omit the specification “coded” to improve readability.

Arguing in a sufficiently strong set theory, each coded dilator $T$ induces a function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$ on the ordinals. To see that this function does not need to be normal we consider the coded dilator that maps $n$ to the order

[TABLE]

with a new biggest element $\Omega$. Its action on a morphism $f:n\rightarrow m$ and the support functions $\operatorname{supp}^{T}_{n}:T_{n}\rightarrow[n]^{<\omega}$ are given by

[TABLE]

It is straightforward to check that

[TABLE]

is isomorphic to $X\cup\{\Omega\}$ (where $\Omega$ is still the biggest element). Thus we have $\operatorname{otp}(D^{T}_{\alpha})=\alpha+1$, which means that the function induced by $T$ is not continuous at limit stages and does not have any fixed points.

To analyze the given counterexample we observe that the functor $T$ from the previous paragraph does not preserve initial segments: Given that the range of $f:n\rightarrow m$ is an initial segment of $m$, we cannot infer that the range of $T_{f}$ is an initial segment of $T_{n}$ (since it contains the element $\Omega$). Indeed, Aczel [1, 2] and Girard [12] have identified preservation of initial segments as the crucial condition that reconciles categorical continuity, i. e. preservation of direct limits, and the usual notion of continuity at limit ordinals (paraphrasing Girard). More precisely, Aczel focuses on initial segments of the form

[TABLE]

where $x$ is an element of the linear order $X=(X,<_{X})$. It will be convenient to have the following notation: For $a,b\in[X]^{<\omega}$ we abbreviate

[TABLE]

The relation $\leq^{\operatorname{fin}}_{X}$ is defined in the same way, with $\leq_{X}$ at the place of $<_{X}$. We omit the subscript when we refer to the usual order on the natural numbers or on the ordinals. In the case of a singleton we write $a<^{\operatorname{fin}}_{X}y$ rather than $a<^{\operatorname{fin}}_{X}\{y\}$. Note that this makes $a<^{\operatorname{fin}}_{X}x$ equivalent to $a\subseteq X\!\restriction\!x$. The following is fundamental:

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

If $T$ is a coded prae-dilator, then we have

[TABLE]

for any order embedding $f:X\rightarrow Y$.

Proof.

For the inclusion $\subseteq$ it suffices to recall $D^{T}_{f}(\langle b,\sigma\rangle)=\langle[f]^{<\omega}(b),\sigma\rangle$. Conversely, induction on the size of $a\subseteq\operatorname{rng}(f)$ yields a finite $b\subseteq X$ with $[f]^{<\omega}(b)=a$. Then $\langle a,\sigma\rangle\in D^{T}_{Y}$ is the image of $\langle b,\sigma\rangle\in D^{T}_{X}$ (observe $|b|=|a|$). ∎

Preservation of initial segments can now be characterized as follows:

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

Consider a coded prae-dilator $T$ and a linear order $X$. The following are equivalent for any elements $x\in X$ and $\rho\in D^{T}_{X}$:

1. (i)

We have $\operatorname{rng}(D^{T}_{\iota_{x}})=D^{T}_{X}\!\restriction\!\rho$, where $\iota_{x}:X\!\restriction\!x\hookrightarrow X$ is the inclusion. 2. (ii)

For any $\langle a,\sigma\rangle\in D^{T}_{X}$ we have

[TABLE]

We will see that a coded dilator with the following property does induce a normal function on the ordinals.

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

A normal prae-dilator consists of a (coded) prae-dilator $T$ and a natural family of order embeddings $\mu^{T}_{n}:n\rightarrow T_{n}$ such that we have

[TABLE]

for all numbers $m<n$ and all elements $\sigma\in T_{n}$.

Note that the family of functions $\mu^{T}_{n}$ can be represented by the set

[TABLE]

of natural numbers. As an example we recall the coded dilator $n\mapsto\omega^{n}$ considered above. It is straightforward to verify that we obtain a normal dilator by setting

[TABLE]

for all numbers $m<n$. Recall that $\langle m\rangle$ corresponds to the formal Cantor normal form $\omega^{m}$. This suggests to think of $\mu^{\omega}_{n}$ as the restriction of the normal function $\alpha\mapsto\omega^{\alpha}$ to the finite ordinal $n$. A formal version of this idea can be found in the proof of Proposition 2.14 below. Before we can formulate it we must extend $\mu^{T}$ beyond the category of natural numbers. This relies on the following observation:

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

If $T=(T,\mu^{T})$ is a normal prae-dilator, then we have

[TABLE]

for all numbers $m<n$.

Proof.

Define $\iota:1\rightarrow n$ by $\iota(0)=m$. By the naturality of $\mu^{T}$ and $\operatorname{supp}^{T}$ we get

[TABLE]

So it remains to show that we cannot have $\operatorname{supp}^{T}_{n}(\mu^{T}_{n}(m))=\emptyset$. The latter would imply $\operatorname{supp}^{T}_{n}(\mu^{T}_{n}(m))<^{\operatorname{fin}}m$ and hence $\mu^{T}_{n}(m)<_{T_{n}}\mu^{T}_{n}(m)$, which is impossible. ∎

In particular the lemma yields $\operatorname{supp}^{T}_{|\{x\}|}(\mu^{T}_{1}(0))=|\{x\}|$, which secures the uniqueness condition needed for the following construction:

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

Let $T$ be a normal prae-dilator. For each order $X$ we define $D^{\mu^{T}}_{X}:X\rightarrow D^{T}_{X}$ by setting

[TABLE]

for all elements $x\in X$.

The reader may have noticed that only the value $\mu^{T}_{1}(0)$ was needed in order to extend $\mu^{T}$ to arbitrary linear orders. To state the equivalence from Definition 2.10 for all numbers $n$ it is nevertheless convenient to consider the entire family of functions $\mu^{T}_{n}:n\rightarrow T_{n}$ as given. The following shows that we have reconstructed the normal prae-dilators from Summary 2.1.

Proposition 2.13** ($\mathbf{RCA}_{0}$).**

If $T$ is a normal prae-dilator, then the functions $D^{\mu^{T}}_{X}:X\rightarrow D^{T}_{X}$ form a natural family of order embeddings. Furthermore we have

[TABLE]

for any order $X$ and any element $\langle a,\sigma\rangle\in D^{T}_{X}$.

Proof.

To show that $D^{\mu^{T}}_{X}$ is an embedding we consider $x_{0}<_{X}x_{1}$. For $j\in\{0,1\}$ we write $\iota_{j}:\{x_{j}\}\hookrightarrow\{x_{0},x_{1}\}$. Using the naturality of $\mu^{T}$ and the fact that $\mu^{T}_{2}$ is order preserving we get

[TABLE]

According to Definition 2.4 this yields

[TABLE]

as desired. To see that $D^{\mu^{T}}$ is natural we compute

[TABLE]

It remains to establish the stated equivalence: First assume that we have

[TABLE]

Write $\iota_{0}:a\hookrightarrow a\cup\{x\}$ and $\iota_{1}:\{x\}\hookrightarrow a\cup\{x\}$ for the inclusions. By definition of the order on $D^{T}_{X}$ we have

[TABLE]

Using the equivalence from Definition 2.10 we can deduce

[TABLE]

This implies $a<^{\operatorname{fin}}_{X}x$, as desired. To establish the converse implication one follows the argument backwards, noting that $a<^{\operatorname{fin}}_{X}x$ implies $[|\iota_{0}|]^{<\omega}(|a|)<^{\operatorname{fin}}|\iota_{1}|(0)$. ∎

Working in a sufficiently strong set theory, we can now prove that normal dilators do induce normal functions. This result is due to Aczel [1, Theorem 2.11].

Proposition 2.14**.**

Assume that $T$ is a normal dilator. Then $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$ is a normal function on the ordinals.

Proof.

As a preparation we observe the following: Writing $\iota_{x}:X\!\restriction\!x\hookrightarrow X$ for the inclusion, we can combine Corollary 2.9 and Proposition 2.13 to see that the range of $D^{T}_{\iota_{x}}$ is equal to $D^{T}_{X}\!\restriction\!D^{\mu^{T}}_{X}(x)$. Since $D^{T}_{\iota_{x}}$ is an order embedding this yields

[TABLE]

for any order $X$ and any $x\in X$. Now we prove that $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$ is strictly increasing: If we have $\alpha<\beta$, then $\alpha$ is isomorphic (and, with the usual set-theoretic definition of ordinals, even equal) to $\beta\!\restriction\!\alpha$. As $D^{T}$ is functorial (see Proposition 2.5) we get $D^{T}_{\alpha}\cong D^{T}_{\beta\restriction\alpha}$. Together with the above observation this yields

[TABLE]

To conclude that $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$ is a normal function we must establish

[TABLE]

when $\lambda$ is a limit ordinal. Given an element $\langle a,\sigma\rangle\in D^{T}_{\lambda}$, pick an ordinal $\alpha<\lambda$ with $a<^{\operatorname{fin}}\alpha$. Then Lemma 2.8 tells us that $\langle a,\sigma\rangle$ lies in the range of $D^{T}_{\iota_{\alpha}}$. By the above we obtain

[TABLE]

Since $\langle a,\sigma\rangle\in D^{T}_{\lambda}$ was arbitrary this implies the claim. ∎

The notion of upper derivative has already been described in Summary 2.1. It order to make it precise, we need to consider compositions of and natural transformations between coded prae-dilators. Compositions are particularly technical in the coded case, since we cannot form $T(S_{n})$ when $T$ is coded and $S_{n}$ is infinite. The reader may wish to skim through the following considerations (up to and including Lemma 2.21) without considering all technical details.

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

Let $T$ and $S$ be coded prae-dilators. For each number $n$ and each morphism $f:n\rightarrow m$ we put

[TABLE]

where $D^{T}(S_{n})$ is ordered according to Definition 2.4. We also define a family of functions $\operatorname{supp}^{T\circ S}_{n}:(T\circ S)_{n}\rightarrow[n]^{<\omega}$ by setting

[TABLE]

for each number $n$.

It is straightforward to see that $\mathbf{RCA}_{0}$ proves the existence of $T\circ S$. Crucially, the extension $D^{T\circ S}$ recovers the composition of $D^{T}$ and $D^{S}$:

Proposition 2.16** ($\mathbf{RCA}_{0}$).**

If $T$ and $S$ are coded (prae-) dilators, then so is $T\circ S$. We get a natural collection of isomorphisms $\zeta^{T,S}_{X}:D^{T}(D^{S}_{X})\rightarrow D^{T\circ S}_{X}$ by setting

[TABLE]

where $\iota_{j}:a_{j}\hookrightarrow a_{1}\cup\dots\cup a_{k}$ are the inclusion maps. Furthermore we have

[TABLE]

for any element $\sigma\in D^{T}(D^{S}_{X})$.

Proof.

One readily verifies that $T\circ S$ is a functor, using Proposition 2.5. The naturality of $\operatorname{supp}^{T\circ S}$ follows from the naturality of $\operatorname{supp}^{S}$. To see that the support condition from Definition 2.2 is satisfied we consider an arbitrary $\langle a,\tau\rangle\in(T\circ S)_{n}$. Abbreviate $c=\operatorname{supp}^{T\circ S}_{n}(\langle a,\tau\rangle)$ and observe that $\operatorname{supp}^{S}_{n}(\sigma)\subseteq c$ holds for any $\sigma\in a$. Using the support condition for $S$ we get $\sigma\in\operatorname{rng}(S_{\iota_{c}\circ\operatorname{en}_{c}})$, where $\iota_{c}:c\hookrightarrow n$ is the inclusion. Induction on $|a|$ yields a finite set $b\subseteq S_{|c|}$ with $[S_{\iota_{c}\circ\operatorname{en}_{c}}]^{<\omega}(b)=a$. Since $S_{\iota_{c}\circ\operatorname{en}_{c}}$ is an embedding we have $|b|=|a|$ and hence $\langle b,\tau\rangle\in D^{T}(S_{|c|})$. In view of

[TABLE]

we learn that $\langle a,\tau\rangle$ lies in the range of $(T\circ S)_{\iota_{c}\circ\operatorname{en}_{c}}$, as required. If $T$ and $S$ are coded dilators, then $D^{T}(D^{S}_{X})$ is well-founded for any well-order $X$. The claim that $T\circ S$ is a coded dilator will follow once we have proved $D^{T}(D^{S}_{X})\cong D^{T\circ S}_{X}$. To show that the given equation for $\zeta^{T,S}_{X}$ defines such an isomorphism we first check that

[TABLE]

implies

[TABLE]

Assuming that the pairs $\langle a_{j},\sigma_{j}\rangle$ are all distinct, we see that $\sigma\in D^{T}(D^{S}_{X})$ requires $\tau\in T_{k}$ and $\operatorname{supp}^{T}_{k}(\tau)=k$. Definition 2.4 also shows that $\langle a_{i},\sigma_{i}\rangle<_{D^{S}_{X}}\langle a_{j},\sigma_{j}\rangle$ implies $S_{|\iota_{i}|}(\sigma_{i})<_{S_{|c|}}S_{|\iota_{j}|}(\sigma_{j})$, where we abbreviate $c=a_{1}\cup\dots\cup a_{k}$. Thus the set $\{S_{|\iota_{1}|}(\sigma_{1}),\dots,S_{|\iota_{k}|}(\sigma_{k})\}$ is still of cardinality $k$, which yields

[TABLE]

To conclude $\zeta^{T,S}_{X}(\sigma)\in D^{T\circ S}_{X}$ it remains to establish $\operatorname{supp}^{T\circ S}_{|c|}(\rho)=|c|$. In view of $\sigma\in D^{T}(D^{S}_{X})$ we must have $\langle a_{j},\sigma_{j}\rangle\in D^{S}_{X}$ and hence $\operatorname{supp}^{S}_{|a_{j}|}(\sigma_{j})=|a_{j}|$. Together with the naturality of $\operatorname{supp}^{S}$ we indeed get

[TABLE]

It is straightforward to check that $\zeta^{T,S}$ is natural, i. e. that we have

[TABLE]

for any embedding $f:X\rightarrow Y$. Using naturality, the claim that $\zeta^{T,S}_{X}$ is order preserving can be reduced to the case where $X=n$ is a natural number. There it follows from the observation that $\zeta^{T,S}_{n}$ factors as

[TABLE]

where $\eta^{S}_{n}$ and $\eta^{T\circ S}_{n}$ are the isomorphisms from Lemma 2.6. To establish that $\zeta^{T,S}_{X}$ is surjective we consider an arbitrary element $\langle c,\langle\{\rho_{1},\dots,\rho_{k}\},\tau\rangle\rangle\in D^{T\circ S}_{X}$. Define $a_{j}=[\operatorname{en}_{c}]^{<\omega}(\operatorname{supp}^{S}_{|c|}(\rho_{i}))$ and write $\iota_{j}:a_{j}\hookrightarrow c$ for the inclusions. Using the support condition for $S$ we get an element $\sigma_{j}\in S_{|a_{j}|}$ with $\rho_{j}=S_{|\iota_{j}|}(\sigma_{j})$. In view of

[TABLE]

we have $\langle a_{i},\sigma_{i}\rangle\in D^{S}_{X}$. One can check that $\langle\{\langle a_{1},\sigma_{1}\rangle,\dots,\langle a_{k},\sigma_{k}\rangle\},\tau\rangle\in D^{T}(D^{S}_{X})$ is the desired preimage under $\zeta^{T,S}_{X}$. The support formula given in the lemma follows by unravelling definitions. ∎

We should also consider compositions in the normal case:

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

Let $T=(T,\mu^{T})$ and $S=(S,\mu^{S})$ be normal prae-dilators. We define a family of functions $\mu^{T\circ S}_{n}:n\rightarrow(T\circ S)_{n}=D^{T}(S_{n})$ by setting

[TABLE]

for all numbers $m<n$.

We verify the expected property:

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

If $(T,\mu^{T})$ and $(S,\mu^{S})$ are normal prae-dilators, then so is $(T\circ S,\mu^{T\circ S})$. Furthermore we have

[TABLE]

for any order $X$, where $\zeta^{T,S}_{X}$ is the isomorphism from Proposition 2.16.

Proof.

Proposition 2.16 tells us that $T\circ S$ is a prae-dilator. The fact that $\mu^{T\circ S}$ is a natural transformation is readily deduced from Proposition 2.13. To verify the equivalence from Definition 2.10 we consider an arbitrary element $\rho=\langle\{\sigma_{1},\dots,\sigma_{k}\},\tau\rangle$ of $(T\circ S)_{n}=D^{T}(S_{n})$. By Proposition 2.13 and the normality of $S$ we get

[TABLE]

The equality asserted in the lemma can be verified by unravelling definitions. ∎

Let us now look at natural transformations between coded prae-dilators. To define their extensions beyond the natural numbers we will use the following result of Girard (the given proof is similar to that of [12, Proposition 2.3.15]):

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

Any natural transformation $\nu:T\Rightarrow S$ between coded prae-dilators satisfies ${\operatorname{supp}^{S}}\circ\nu=\operatorname{supp}^{T}$.

Proof.

Consider a number $n$ and an element $\sigma\in T_{n}$. By the support condition from Definition 2.2 we have $\sigma=T_{\iota_{\sigma}\circ\operatorname{en}_{\sigma}}(\sigma_{0})$ for some $\sigma_{0}\in T_{m}$, with $m=|\operatorname{supp}^{T}_{n}(\sigma)|$. Using the naturality of $\nu$ and $\operatorname{supp}^{S}$ we get

[TABLE]

Aiming at a contradiction, let us now assume that there is a $k\in\operatorname{supp}^{T}_{n}(\sigma)$ that does not lie in $\operatorname{supp}^{S}_{n}(\nu_{n}(\sigma))$. Consider the functions $f_{1},f_{2}:n\rightarrow n+1$ with

[TABLE]

Observe that we have

[TABLE]

as well as

[TABLE]

Thus $T_{f_{1}}(\sigma)$ and $T_{f_{2}}(\sigma)$ are distinguished by their supports. Since $\nu_{n+1}$ is injective we obtain

[TABLE]

By Definition 2.2 we may write $\nu_{n}(\sigma)=S_{\iota_{\nu_{n}(\sigma)}\circ\operatorname{en}_{\nu_{n}(\sigma)}}(\tau_{0})$. Since $k$ is not contained in $\operatorname{rng}(\iota_{\nu_{n}(\sigma)})=\operatorname{supp}^{S}_{n}(\nu_{n}(\sigma))$ we have

[TABLE]

Thus we get

[TABLE]

which contradicts the inequality established above. ∎

Let us remark that ${\operatorname{supp}^{S}}\circ\nu=\operatorname{supp}^{T}$ is equivalent to the assertion that $\nu$ is Cartesian (i. e. that the naturality squares for $\nu$ are pullbacks). Thus the latter holds for any natural transformation between prae-dilators, as pointed out by P. Taylor [22] (the first author would like to thank Thomas Streicher for this reference and for enlightening explanations). For us the lemma is important since it ensures that the uniqueness condition $\operatorname{supp}^{T}_{|a|}(\sigma)=|a|$ from Definition 2.4 is preserved under natural transformations, which justifies the definition of $D^{\nu}$:

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

Given coded prae-dilators $T$ and $S$, any natural transformation $\nu:T\Rightarrow S$ is called a morphism of coded prae-dilators. If $T=(T,\mu^{T})$ and $S=(S,\mu^{S})$ are normal and we have $\nu\circ\mu^{T}=\mu^{S}$, then $\nu$ is called a morphism of normal prae-dilators. To extend $\nu$ beyond the category of natural numbers we define $D^{\nu}_{X}:D^{T}_{X}\rightarrow D^{S}_{X}$ by setting

[TABLE]

for each linear order $X$.

Let us verify that the extension of a morphism has the expected property:

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

If $\nu:T\Rightarrow S$ is a morphism of (normal) prae-dilators, then the maps $D^{\nu}_{X}:D^{T}_{X}\rightarrow D^{S}_{X}$ form a natural transformation (and $D^{\nu}_{X}\circ D^{\mu^{T}}_{X}=D^{\mu^{S}}_{X}$ holds for every order $X$). Furthermore we have ${\operatorname{supp}^{D^{S}}_{X}}\circ D^{\nu}_{X}=\operatorname{supp}^{D^{T}}_{X}$.

Proof.

To see that each function $D^{\nu}_{X}:D^{T}_{X}\rightarrow D^{S}_{X}$ is order preserving it suffices to observe that $T_{|\iota_{a}^{a\cup b}|}(\sigma)<_{T_{|a\cup b|}}T_{|\iota_{b}^{a\cup b}|}(\tau)$ implies

[TABLE]

using the naturality of $\nu$ and the fact that $\nu_{|a\cup b|}$ is order preserving. The naturality of $D^{\nu}$ follows from the fact that we have $|[f]^{<\omega}(a)|=|a|$ for any order preserving function $f$. If $\nu$ is a morphism of normal prae-dilators, then we get

[TABLE]

The relation between the supports is immediate in view of Definition 2.4. ∎

As suggested by the last line of equations, one can show that the general condition $\nu_{n}\circ\mu^{T}_{n}=\mu^{S}_{n}$ follows from the special case $n=1$ (write $m<n$ as $m=\iota(0)$ with $\iota:1\rightarrow n$ and use naturality). In practice it is just as straightforward to verify the condition for arbitrary $n$. We now have all ingredients to define upper derivatives on the level of coded prae-dilators:

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

Let $T$ be a normal prae-dilator. An upper derivative of $T$ consists of a normal prae-dilator $S$ and a morphism $\xi:T\circ S\Rightarrow S$ of normal prae-dilators.

With the previous definition we have completed our formalization of statement (2) from the introduction (where $S$ stands for $(S,\xi)$). Of course we want to know that we have recovered the notion of upper derivative for normal functions. This fact can be established in a sufficiently strong set theory:

Proposition 2.23**.**

Consider normal dilators $T$ and $S$. If there is a natural transformation $\xi:T\circ S\Rightarrow S$, then the normal function $\alpha\mapsto\operatorname{otp}(D^{S}_{\alpha})$ is an upper derivative of the normal function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$.

Before we prove the proposition, let us remark that $X\mapsto D^{T}_{X}$ automatically preserves well-foundedness if $X\mapsto D^{S}_{X}$ does, since

[TABLE]

is an embedding ($\zeta^{T,S}$ is the natural isomorphism from Proposition 2.16).

Proof.

In view of Proposition 2.14 it suffices to establish $\operatorname{otp}(D^{T}_{\gamma})\leq\gamma$ for any value $\gamma=\operatorname{otp}(D^{S}_{\alpha})\cong D^{S}_{\alpha}$. The required inequality is witnessed by the embeddings

[TABLE]

where the first isomorphism uses the functoriality of $D^{T}$ (cf. Proposition 2.5). ∎

To conclude the discussion of upper derivatives we record an immediate consequence of Lemmas 2.18 and 2.21. The equality in the corollary has an intuitive meaning, which will become clear in the proof of Theorem 2.29.

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

Assume that $(S,\xi)$ is an upper derivative of a normal prae-dilator $T$. Then we have

[TABLE]

for any order $X$.

As a final topic of this section we consider derivatives of normal prae-dilators. On the level of normal functions the derivative is the upper derivative with the smallest possible values. In a categorical setting this is naturally expressed via the notion of initial object. To make this precise we need the following construction:

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

Given coded prae-dilators $T,S^{1},S^{2}$ and a natural transformation $\nu:S^{1}\Rightarrow S^{2}$, we define a family of functions $T(\nu)_{n}:(T\circ S^{1})_{n}\rightarrow(T\circ S^{2})_{n}$ by setting

[TABLE]

for each number $n$.

We verify the expected properties:

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

Let $T$ be a (normal) prae-dilator. If $\nu:S^{1}\Rightarrow S^{2}$ is a morphism of (normal) prae-dilators, then so is $T(\nu):T\circ S^{1}\Rightarrow T\circ S^{2}$. Furthermore we have

[TABLE]

for each order $X$, where $\zeta^{T,S^{i}}$ are the natural isomorphisms from Proposition 2.16.

Proof.

Using Proposition 2.5 and the naturality of $\nu$ one readily shows that $T(\nu)$ is a natural family of embeddings. If $\nu$ is a morphism of normal prae-dilators, then we invoke the naturality of $D^{\mu^{T}}$ (due to Proposition 2.13) to get

[TABLE]

which shows that $T(\nu)$ is a morphism of normal prae-dilators. The equality asserted in the lemma can be verified by unravelling definitions. ∎

Let us introduce a last ingredient for the definition of derivatives:

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

Consider a normal prae-dilator $T$ with upper derivatives $(S^{1},\xi^{1})$ and $(S^{2},\xi^{2})$. A morphism of upper derivatives is a morphism $\nu:S^{1}\Rightarrow S^{2}$ of normal prae-dilators that satisfies $\nu\circ\xi^{1}=\xi^{2}\circ T(\nu)$.

Finally, we can characterize derivatives on the level of coded prae-dilators:

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

A derivative of a normal prae-dilator $T$ is an upper derivative $(S,\xi)$ of $T$ that is initial in the following sense: For any upper derivative $(S^{\prime},\xi^{\prime})$ of $T$ there is a unique morphism $\nu:S\Rightarrow S^{\prime}$ of upper derivatives.

Due to the form of the given definition it is clear that the derivative of a normal prae-dilator is unique up to isomorphism of upper derivatives. Other properties of the derivative are harder to establish. In Sections 4 and 5 we will show that the assumptions of the following theorem hold when $(S,\xi)$ is a derivative of $T$. This leads to an unconditional version of the result, which will be stated as Corollary 5.11.

Theorem 2.29**.**

Let $(S,\xi)$ be an upper derivative of a normal dilator $T$. Assume that the maps $\xi_{n}:(T\circ S)_{n}\rightarrow S_{n}$ are surjective (so that $\xi$ is an isomorphism), that

[TABLE]

is an equalizer diagram for every $n$, and that $X\mapsto D^{S}_{X}$ preserves well-foundedness. Then $\alpha\mapsto\operatorname{otp}(D^{S}_{\alpha})$ is the derivative of the normal function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$.

Before we prove the theorem we motivate the equalizer condition: By Definition 2.17 and the fact that $\xi$ is a morphism of normal prae-dilators we get

[TABLE]

So the assumption that the equalizer diagrams commute is automatic. After Definition 2.10 we have explained that $\mu^{T}$ can be seen as an internal version of the function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$. Intuitively speaking, the equalizer condition thus demands that any ordinal $\alpha$ with $\operatorname{otp}(D^{T}_{\alpha})=\alpha$ lies in the range of $\alpha\mapsto\operatorname{otp}(D^{S}_{\alpha})$.

Proof.

As a preparation we lift the assumptions of the theorem to the level of class-sized dilators: In view of Definition 2.20 it is straightforward to show that each function $D^{\xi}_{X}:D^{T\circ S}_{X}\rightarrow D^{S}_{X}$ is an isomorphism. From Corollary 2.24 we know that

[TABLE]

is a commutative diagram. To show that it defines an equalizer we consider an arbitrary element $\langle a,\sigma\rangle\in D^{S}_{X}$. Invoking Definitions 2.12 and 2.20, as well as the proof of Proposition 2.16, we see

[TABLE]

If this value is equal to $\langle a,\sigma\rangle$, then we have $\xi_{|a|}\circ D^{\mu^{T}}_{S_{|a|}}(\sigma)=\sigma$. Thus the equalizer condition from the theorem yields $\sigma=\mu^{S}_{|a|}(m)$ for some $m<|a|$. According to Definition 2.4 and Lemma 2.11 we must have

[TABLE]

This forces $m=0$ and $|a|=1$, say $a=\{x\}$. We can conclude

[TABLE]

as required to make the above an equalizer diagram. Based on these preparations we can now prove the actual claim of the theorem: Write $f$ for the normal function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$ and $f^{\prime}$ for its derivative. Proposition 2.23 yields $\operatorname{otp}(D^{S}_{\beta})\geq f^{\prime}(\beta)$. We may thus define an order embedding $f^{\prime}_{S}:\beta\rightarrow D^{S}_{\beta}$ by stipulating

[TABLE]

To make use of the equalizer diagram from the beginning of the proof we need

[TABLE]

Since $D^{\xi}_{\beta}\circ\zeta^{T,S}_{\beta}:D^{T}(D^{S}_{\beta})\rightarrow D^{S}_{\beta}$ is an isomorphism this reduces to

[TABLE]

By the proof of Proposition 2.14 and the functoriality of $D^{T}$, the left side is indeed equal to

[TABLE]

Now the universal property of equalizers yields an embedding $g:\beta\rightarrow\beta$ that satisfies $D^{\mu^{S}}_{\beta}\circ g=f^{\prime}_{S}$. Since $g$ is a strictly increasing function on the ordinals we have $\alpha\leq g(\alpha)$. Thus, again invoking the proof of Proposition 2.14, we get

[TABLE]

We have already seen $\operatorname{otp}(D^{S}_{\alpha})\geq f^{\prime}(\alpha)$. So we can conclude that $\alpha\mapsto\operatorname{otp}(D^{S}_{\alpha})$ coincides with the derivative $f^{\prime}$ of the normal function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$, as desired. ∎

In Example 4.14 we will exhibit an upper derivative $(S,\xi)$ that satisfies the equalizer condition but fails to be a derivative in the sense of Definition 2.28. This shows that the equalizer condition does not suffice to characterize derivatives on the categorical level. The relevance of Example 4.14 is somewhat diminished by the fact that $X\mapsto D^{S}_{X}$ does not preserve well-foundedness.

3. From upper derivative to $\Pi^{1}_{1}$-bar induction

In this section we prove that bar induction for $\Pi^{1}_{1}$-formulas follows from the principle that every normal dilator has an upper derivative that preserves well-foundedness (i. e. that is again a normal dilator). To establish this result we follow the informal argument given at the beginning of the introduction.

The first major goal of the section is to reconstruct the functions $h$ and $f$ from the informal argument in terms of dilators. Since the notion of dilator is $\Pi^{1}_{2}$-complete (due to Girard) it makes sense that this is possible. Indeed our reconstruction of $h$ is inspired by Norman’s proof of $\Pi^{1}_{2}$-completeness (see [14, Annex 8.E]). To get a usable result we will have to adapt his argument to the specific form of bar induction. Our reconstruction of $f$ can be read as a proof that the more restrictive class of normal dilators is $\Pi^{1}_{2}$-complete as well.

Let us begin with some terminology: Given a set $Y$, we write $Y^{<\omega}$ for the tree of finite sequences with entries in $Y$. If $Y=(Y,<_{Y})$ is a linear order, then the Kleene-Brouwer order (also known as Lusin-Sierpiński order) on $Y^{<\omega}$ is defined by

[TABLE]

In the second clause $(\sigma)_{j}$ refers to the $j$-th entry of $\sigma$, for $j<\operatorname{len}(\sigma)$ below the length of $\sigma$ (note that such a $j$ exists when neither sequence is an end extension of the other). If we want to emphasize that $\mathcal{T}$ is ordered as a subtree of $Y^{<\omega}$, then we say that it carries the Kleene-Brouwer order with respect to $Y$. The symbol $<_{\operatorname{KB}}$ will be reserved for the Kleene-Brouwer order with respect to $\mathbb{N}$ (ordered as usual). Recall that a branch of $\mathcal{T}\subseteq Y^{<\omega}$ is given by a function $f:\mathbb{N}\rightarrow Y$ such that we have $f[n]\in\mathcal{T}$ for all $n\in\mathbb{N}$, where the sequence

[TABLE]

lists the first $n$ values of $f$. It is well-known that $\mathbf{ACA}_{0}$ proves the characteristic property of the Kleene-Brouwer order: If $Y$ is a well-order, then $\mathcal{T}$ has no branch if, and only if, the Kleene-Brouwer order with respect to $Y$ is well-founded on $\mathcal{T}$ (to adapt the proof from [21, Lemma V.1.3], which treats the case $Y=\mathbb{N}$, one observes that $\mathbb{N}$ embeds into any infinite suborder $Y_{0}\subseteq Y$, e. g. as an initial segment).

Given an order $X=(X,<_{X})$, an $X$-indexed family of orders is given as a set

[TABLE]

where $Y_{x}=(Y_{x},<_{Y_{x}})$ is an order for each $x\in X$. The dependent sum $\Sigma_{x\in X}Y_{x}$ (or shorter $\Sigma Y$) is the order with underlying set $Y$ and order relation given by

[TABLE]

For $x\in X$ we write $\Sigma_{x^{\prime}<_{X}x}Y_{x^{\prime}}$ (or shorter $\Sigma_{x}Y$) for the suborder that contains all pairs $\langle x^{\prime},y\rangle\in\Sigma Y$ with $x^{\prime}<_{X}x$. If $X$ is a well-order, then $\Sigma Y$ is well-founded if, and only if, $Y_{x}$ is well-founded for every $x\in X$, provably in $\mathbf{RCA}_{0}$ (the first components of a descending sequence in $\Sigma Y$ must become constant with some value $x\in X$, from which point on the second components form a descending sequence in $Y_{x}$). The product $X\times Y$ of two orders is explained as the special case where we have $Y_{x}=Y$ for all $x\in X$. Let us mention one other construction that will be needed later: Given an order $Y=(Y,<_{Y})$, we write

[TABLE]

for the extension of $Y$ by a new minimal element (i. e. we have $\bot<_{Y^{\bot}}y<_{Y^{\bot}}y^{\prime}$ for any $y,y^{\prime}\in Y$ with $y<_{Y}y^{\prime}$). If $f:Y\rightarrow Z$ is an embedding, then we get an embedding $f^{\bot}:Y^{\bot}\rightarrow Z^{\bot}$ by setting

[TABLE]

One readily verifies that the construction is functorial (and in fact a dilator), in the sense that we have $(g\circ f)^{\bot}=g^{\bot}\circ f^{\bot}$ for functions $f,g$ of suitable (co-)domain.

We will be particularly interested in dependent sums of the form $\Sigma\mathcal{T}=\Sigma_{x\in X}\mathcal{T}_{x}$, where $X$ is a well-order and each $\mathcal{T}_{x}$ is a subtree of $\mathbb{N}^{<\omega}$, with the usual Kleene-Brouwer order. In this situation we call $\mathcal{T}$ an $X$-indexed family of $\mathbb{N}$-trees. As in the informal argument from the introduction, the idea is that the well-foundedness of $\mathcal{T}_{x}$ corresponds to the fact that some $\Pi^{1}_{1}$-formula $\varphi$ holds at $x\in X$. Above we have seen that $\Sigma_{x}\mathcal{T}$ is well-founded if, and only if, $\mathcal{T}_{y}$ is well-founded for all $y<_{X}x$. Thus it makes sense to call $\mathcal{T}$ progressive at $x\in X$ if we have

[TABLE]

If $\mathcal{T}$ is progressive at every $x\in X$, then it is called progressive along $X$.

Let us now describe our reconstruction of the function $h$: The ordinal $\alpha$ and the induction formula $\varphi$ that appear in the informal argument from the introduction correspond to a well-order $X$ and an $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees. In order to represent the function $\delta\mapsto h(\gamma,\delta)$ with $\gamma<\alpha$ we will construct a prae-dilator $H[x]$ such that $\mathcal{T}$ is progressive at $x\in X$ if, and only if, $H[x]$ is a dilator (we write $H[x]$ for both the class-sized dilator and its coded restriction, cf. the discussion after Definition 2.7). Considering the contrapositive of the implication from left to right, we see that we should ensure the following: If $H[x]_{Z}\cong D^{H[x]}_{Z}$ is ill-founded for some well-order $Z$, then $\Sigma_{x}\mathcal{T}$ must be well-founded while $\mathcal{T}_{x}$ is not. Inspired by Norman’s proof of $\Pi^{1}_{2}$-completeness, the idea is to define $H[x]_{Z}$ as a tree: Along each potential branch one searches for an embedding of $\Sigma_{x}\mathcal{T}$ into $Z$ and, simultaneously, for a descending sequence in $\mathcal{T}_{x}$. This leads to the following construction:

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

Consider a well-order $X$, an $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees and an element $x\in X$. For each order $Z$ we define $H[x]_{Z}=H[X,\mathcal{T},x]_{Z}$ as the tree of all sequences

[TABLE]

that satisfy the following:

1. (i)

Whenever $j_{1},j_{2}<k$ code elements $j_{i}=\langle y_{i},\sigma_{i}\rangle\in\Sigma_{x}\mathcal{T}$, we have $z_{j_{i}}\in Z$ (i. e. $z_{j_{i}}\neq\bot$) and

[TABLE] 2. (ii)

We have $\langle s_{0},\dots,s_{k-1}\rangle\in\mathcal{T}_{x}$.

The order on $H[x]_{Z}$ is the Kleene-Brouwer order with respect to $Z^{\bot}\times\mathbb{N}$. For an embedding $f:Z\rightarrow Y$ we define $H[x]_{f}:H[x]_{Z}\rightarrow H[x]_{Y}$ by

[TABLE]

To define a family of functions $\operatorname{supp}^{H[x]}_{Z}:H[x]_{Z}\rightarrow[Z]^{<\omega}$ we set

[TABLE]

for each order $Z$.

The following is readily verified:

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

The orders and functions that we have constructed in the previous definition form a prae-dilator $H[x]=H[X,\mathcal{T},x]$.

Since the previous result is formulated in $\mathbf{RCA}_{0}$, it is officially concerned with the coded restriction of $H[x]$ to the category of natural numbers. The following technical observation shows that the class-sized and coded versions of $H[x]$ can be identified (cf. the discussion after Definition 2.7).

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

For each order $Z$ we get an isomorphism $D^{H[x]}_{Z}\cong H[x]_{Z}$ by stipulating

[TABLE]

where $\iota_{a}\circ\operatorname{en}_{a}:|a|\rightarrow Z$ is the unique embedding with range $a\in[Z]^{<\omega}$.

Proof.

To verify the claim one follows the proof of Lemma 2.6. ∎

We can now deduce the connection with the premise of $\Pi^{1}_{1}$-bar induction. As mentioned before, this part of our argument is similar to Norman’s proof that the notion of dilator is $\Pi^{1}_{2}$-complete (see [14, Annex 8.E]). We choose the base theory $\mathbf{ACA}_{0}$ since we will apply the characteristic property of the Kleene-Brouwer order:

Proposition 3.4** ($\mathbf{ACA}_{0}$).**

An $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees is progressive at $x\in X$ if, and only if, $H[x]=H[X,\mathcal{T},x]$ is a dilator.

Proof.

By Lemma 3.2 we already know that $H[x]$ is a prae-dilator. Thus we need to show that the implication

[TABLE]

holds if, and only if, $H[x]_{Z}\cong D^{H[x]}_{Z}$ is well-founded for every well-order $Z$. Aiming at the contrapositive of the first direction, assume that $Z$ is a well-order such that $H[x]_{Z}$ is ill-founded. By the characteristic property of the Kleene-Brouwer order we get a branch in the tree $H[x]_{Z}\subseteq(Z^{\bot}\times\mathbb{N})^{<\omega}$. In view of Definition 3.1 the first components of this branch form an embedding of $\Sigma_{x}\mathcal{T}$ into the well-order $Z$, which witnesses the premise of the above implication. The second components of our branch form a branch in the tree $\mathcal{T}_{x}$, so that the latter is ill-founded. Thus our implication fails and the first direction is established. For the other direction we assume that $H[x]$ is a dilator. Assuming the premise of the above implication, it follows that $H[x]_{\Sigma_{x}\mathcal{T}}$ is a well-order. To establish the conclusion of our implication, we construct an embedding of $\mathcal{T}_{x}$ into $H[x]_{\Sigma_{x}\mathcal{T}}$. Define $e:\mathbb{N}\to(\Sigma_{x}\mathcal{T})^{\bot}$ by

[TABLE]

It is straightforward to verify that

[TABLE]

is the required embedding. ∎

So far we have reconstructed the function $h$ from the informal argument from the introduction. In the rest of this section we reconstruct the normal function $f$ and conclude the proof of $\Pi^{1}_{1}$-bar induction. Since the formalization in second order arithmetic is somewhat technical, we begin with an informal exposition:

Summary 3.5**.**

In the informal argument from the introduction we have transformed $h$ into a function $h_{0}$ with $h_{0}(\delta)=\sup_{\gamma\leq\delta}h(\gamma,\delta)$. The supremum does not seem to be available on the level of dilators, but it can be bounded by a transfinite sum: For each order $Z$ we consider the order

[TABLE]

Here $H[x]=H[X,\mathcal{T},x]$ is constructed with respect to a fixed well-order $X$ and an $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees that is progressive along $X$. It is straightforward to turn $H^{0}$ into a prae-dilator, and Proposition 3.4 implies that $H^{0}$ is a dilator. The informal argument proceeds with a normal function $f$ with $f(\delta)=\sum_{\gamma<\delta}1+h_{0}(\gamma)$. If $\delta$ is represented by $Z$, then $\gamma<\delta$ corresponds to $Z\!\restriction\!z=\{z^{\prime}\in Z\,|\,z^{\prime}<_{Z}z\}$ for some $z\in Z$. Hence $f$ can be represented by a dilator $F$ with

[TABLE]

Elements of $F_{Z}$ have the form $\langle z,\bot\rangle$ or $\langle z,x,\sigma\rangle$ (with one pair of parentheses omitted) for $z\in Z$, $x\in X$ and $\sigma\in H[x]_{Z\restriction z}$. One can check that $F$ becomes normal if we define $\mu^{F}_{Z}:Z\to F_{Z}$ by $\mu^{F}_{Z}(z)=\langle z,\bot\rangle$ (cf. Proposition 3.7 below). We point out that the definition of $F$ resembles Girard’s construction of a flower $\int T$ from a given dilator $T$ (cf. [12, Example 2.4.9]). In our setting, the conclusion of $\Pi^{1}_{1}$-bar induction amounts to the claim that $\Sigma_{x\in X}\mathcal{T}_{x}$ is well-founded. We want to deduce this claim from the assumption that $F$ has an upper derivative

[TABLE]

such that $G$ preserves well-foundedness. Since $X$ is a well-order, it suffices to construct an embedding

[TABLE]

In a sufficiently strong meta theory, the value $J(\langle x,\sigma\rangle)$ can be constructed by recursion on $x$: The normal dilator $G$ comes with an embedding $\mu^{G}_{X}:X\to G_{X}$. Inductively we assume that we already have values $J(\langle y,\sigma\rangle)\in G_{X}\!\restriction\!\mu^{G}_{X}(x)$ for all $\langle y,\sigma\rangle\in\Sigma_{y<_{X}x}\mathcal{T}_{y}=\Sigma_{x}\mathcal{T}$. We can then define $J_{x}:\mathbb{N}\to(G_{X}\!\restriction\!\mu^{G}_{X}(x))^{\bot}$ by

[TABLE]

Assuming that $J$ is order preserving on $\Sigma_{x}\mathcal{T}$, we have

[TABLE]

Using the function $\xi_{X}:F(G_{X})\to G_{X}$, we can now define $J(\langle x,\langle s_{0},\dots,s_{k-1}\rangle\rangle)$ as

[TABLE]

For $x<_{X}x^{\prime}$ the argument of $\xi_{X}$ is below $\langle\mu^{G}_{X}(x^{\prime}),\bot\rangle=\mu^{F}_{G(X)}\circ\mu^{G}_{X}(x^{\prime})=\mu^{F\circ G}_{X}(x^{\prime})$. Since $\xi:F\circ G\Rightarrow G$ is a morphism of normal dilators, this implies

[TABLE]

as we have assumed in the recursive construction. In the proof of Theorem 3.12 we will see that $J$ can be constructed by primitive recursion, since each value $J(\langle x,\sigma\rangle)$ does only depend on a finite (and effectively bounded) collection of previous values.

In the rest of this section we provide a detailed formalization of the argument from Summary 3.5. The first step is to define $F$ as a coded dilator. As explained in the previous section, this means that $F$ acts on finite orders of the form $n=\{0,\dots,n-1\}$. It will be very convenient to have a more uniform presentation of the orders $(\Sigma_{x\in X}H[x]_{n})^{\bot}$. For this purpose we extend the $X$-indexed family of prae-dilators $H[x]$ to a family indexed by $X^{\bot}$: Define $H[\bot]=H[X,\mathcal{T},\bot]$ as the constant prae-dilator with values

[TABLE]

where $\star$ is some new symbol. Its action on morphisms and the support functions are given by $H[\bot]_{f}(\star)=\star$ and $\operatorname{supp}^{H[\bot]}_{n}(\star)=\emptyset$. Then we have

[TABLE]

where the isomorphism sends $\bot$ to $\langle\bot,\star\rangle$ and leaves $\langle x,\tau\rangle$ with $x\in X$ unchanged. The point is that all elements of the right side are pairs, which will save us many case distinctions. Invoking Definition 2.4 we see that $D^{H[\bot]}_{Z}$ consists of the single element $\langle\emptyset,\star\rangle$. Thus $H[\bot]$ is a dilator and we have

[TABLE]

We now define the coded prae-dilator $F$ that reconstructs the function $f$ from the informal argument. The crucial point is that $F$ is normal, as we shall see below.

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

Consider a well-order $X$ and an $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees. For each number $n$ we define

[TABLE]

Omitting one pair of parentheses, we write the elements of $F_{n}$ in the form $\langle N,x,\sigma\rangle$ with $N\in n=\{0,\dots,n-1\}$, $x\in X^{\bot}$ and $\sigma\in H[x]_{N}$. The order on $F_{n}$ is the usual order on a dependent sum, which coincides with the lexicographic order on the triples $\langle N,x,\sigma\rangle$. Given an embedding $f:n\rightarrow m$, we write $f\!\restriction\!N:N\rightarrow f(N)$ for the restriction of $f$. Then we define $F_{f}:F_{n}\rightarrow F_{m}$ by

[TABLE]

The functions $\operatorname{supp}^{F}_{n}:F_{n}\rightarrow[n]^{<\omega}$ are given as

[TABLE]

Finally we define a family of functions $\mu^{F}_{n}:n\rightarrow F_{n}$ by setting

[TABLE]

for all numbers $N<n$.

Let us verify the following:

Proposition 3.7** ($\mathbf{RCA}_{0}$).**

The orders and functions from the previous definition form a normal prae-dilator $F=F[X,\mathcal{T}]$.

Proof.

Using Lemma 3.2 it is straightforward to show that $F$ is a functor and that $\operatorname{supp}^{F}$ is a natural transformation. To conclude that $F$ is a prae-dilator we must verify the support condition from clause (ii) of Definition 2.2. To do so we consider an arbitrary $\sigma=\langle N,x,\tau\rangle\in F_{n}$. We abbreviate $a:=\operatorname{supp}^{H[x]}_{N}(\tau)\subseteq\{0,\dots,N-1\}$ and write $\iota_{\sigma}\circ\operatorname{en}_{\sigma}:|a|+1\rightarrow n$ for the embedding with range $\operatorname{supp}^{F}_{n}(\sigma)=a\cup\{N\}$. Since the restriction $(\iota_{\sigma}\circ\operatorname{en}_{\sigma})\!\restriction\!|a|:|a|\rightarrow N$ has range $a$, the support condition for $H[x]$ yields a $\tau_{0}\in H[x]_{|a|}$ with $\tau=H[x]_{(\iota_{\sigma}\circ\operatorname{en}_{\sigma})\restriction|a|}(\tau_{0})$. By construction we have $\langle|a|,x,\tau_{0}\rangle\in F_{|a\cup\{N\}|}$ and $\sigma=F_{\iota_{\sigma}\circ\operatorname{en}_{\sigma}}(\langle|a|,x,\tau_{0}\rangle)$, which completes the proof of the support condition for $F$. One readily verifies that $\mu^{F}$ is a natural family of embeddings (for naturality we recall $H[\bot]_{f\restriction N}(\star)=\star$). In view of Definition 2.10 it remains to establish

[TABLE]

for arbitrary $\sigma\in F_{n}$ and $N<n$. For the first direction we recall that $\langle\bot,\star\rangle$ is the smallest element of $\Sigma_{x\in X^{\bot}}H[x]_{N}$. Thus any $\sigma<_{F_{n}}\mu^{F}_{n}(N)=\langle N,\bot,\star\rangle$ must have the form $\sigma=\langle N^{\prime},x,\tau\rangle$ with $N^{\prime}<N$. In view of $\operatorname{supp}^{H[x]}_{N^{\prime}}(\tau)\in[N^{\prime}]^{<\omega}$ we get

[TABLE]

For the converse we also write $\sigma=\langle N^{\prime},x,\tau\rangle$. In view of $N^{\prime}\in\operatorname{supp}^{F}_{n}(\sigma)$ the right side of the desired equivalence implies $N^{\prime}<N$ and thus $\sigma<_{F_{n}}\mu^{F}_{n}(N)$. ∎

Lemma 3.3 provides a transparent description of the orders $D^{H[x]}_{Z}$ (recall that the latter consist of pairs $\langle a,\tau\rangle$ with $a\in[Z]^{<\omega}$ and $\tau\in H[x]_{|a|}$, see Definition 2.4). We now describe $D^{F}_{Z}$ relative to these orders:

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

Given an order $Z$, we put

[TABLE]

The order on $F_{Z}$ is the indicated product order, which coincides with the lexicographic order on the triples $\langle z,x,\langle a,\tau\rangle\rangle$ (we again omit a pair of angle parentheses).

Note that the previous definition of $F_{Z}$ is similar but not quite identical to the informal construction in Summary 3.5. The following proof consists in a technical verification, which can be skipped at first reading.

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

For each order $Z$ the clause

[TABLE]

defines an isomorphism $\chi^{F}_{Z}:F_{Z}\rightarrow D^{F}_{Z}$.

Proof.

To see that $\chi^{F}_{Z}$ has values in $D^{F}_{Z}$ we consider an arbitrary $\langle z,x,\langle a,\tau\rangle\rangle\in F_{Z}$. In view of Definition 2.4 we have $\tau\in H[x]_{|a|}$ and $\operatorname{supp}^{H[x]}_{|a|}(\tau)=|a|$. This yields

[TABLE]

The condition $a<^{\operatorname{fin}}_{Z}z$ ensures $|a\cup\{z\}|=|a|+1$. Thus we indeed have

[TABLE]

To prove that $\chi^{F}_{Z}$ is order preserving we consider an inequality

[TABLE]

We write $\iota_{j}:a_{j}\cup\{z_{j}\}\hookrightarrow a_{0}\cup a_{1}\cup\{z_{0},z_{1}\}=:c$ with $j\in\{0,1\}$ for the inclusions. Furthermore, let $\operatorname{en}_{c}:|c|\rightarrow c$ and $\operatorname{en}_{j}:|a_{j}\cup\{z_{j}\}|\rightarrow a_{j}\cup\{z_{j}\}$ denote the increasing enumerations. As in the previous section, the function $|\iota_{j}|:|a_{j}\cup\{z_{j}\}|\rightarrow|c|$ is determined by the property that it is order preserving and makes the following diagram commute:

[TABLE]

According to Definition 2.4 the desired inequality between the values of $\chi^{F}_{Z}$ is equivalent to

[TABLE]

By the definition of $F$ the latter amounts to

[TABLE]

To establish this inequality we first assume that the given inequality between the arguments of $\chi^{F}_{Z}$ holds because of $z_{0}<_{Z}z_{1}$. In view of the condition $a_{j}<^{\operatorname{fin}}_{Z}z_{j}$ we have $\operatorname{en}_{j}(|a_{j}|)=z_{j}$ and thus

[TABLE]

This implies $|\iota_{0}|(|a_{0}|)<|\iota_{1}|(|a_{1}|)$, so that the required inequality holds. A similar argument shows that $z_{0}=z_{1}$ implies $|\iota_{0}|(|a_{0}|)=|\iota_{1}|(|a_{1}|)$. The case where we have $z_{0}=z_{1}$ and $x_{0}<_{X}x_{1}$ is now immediate. Finally assume $z_{0}=z_{1}$, $x_{0}=x_{1}=:x$ and

[TABLE]

It is straightforward to check that the restriction $|\iota_{j}|\!\restriction\!|a_{j}|$ makes the following diagram commute, where the vertical arrows are the increasing enumerations:

[TABLE]

In view of Definition 2.4 we can conclude

[TABLE]

which implies the required inequality. To show that $\chi^{F}_{Z}$ is surjective we consider an arbitrary $\langle b,\langle N,x,\tau\rangle\rangle\in D^{F}_{Z}$. According to Definition 2.4 we must have

[TABLE]

which forces $|b|=N+1$ and $\operatorname{supp}^{H[x]}_{N}(\tau)=N$. In particular $b$ is non-empty, so that we can write $b=a\cup\{z\}$ with $a<^{\operatorname{fin}}_{Z}z$. In view of $|a|=N$ we get $\langle a,\tau\rangle\in D^{H[x]}_{Z}$ and then $\langle z,x,\langle a,\tau\rangle\rangle\in F_{Z}$, as well as $\chi^{F}_{Z}(\langle z,x,\langle a,\tau\rangle\rangle)=\langle b,\langle N,x,\tau\rangle\rangle$. ∎

By combining previous results we obtain the following:

Corollary 3.10** ($\mathbf{ACA}_{0}$).**

Consider a well-order $X$. An $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees is progressive along $X$ if, and only if, $F[X,\mathcal{T}]$ is a normal dilator.

Proof.

In view of Proposition 3.4, Proposition 3.7 and the previous lemma it suffices to show that $Z\mapsto F_{Z}$ preserves well-foundedness if, and only if, $Z\mapsto D^{H[x]}_{Z}$ preserves well-foundedness for all $x\in X$. If the latter holds, then

[TABLE]

is well-founded for any well-order $Z$ (recall that $D^{H[\bot]}_{Z}=\{\langle\emptyset,\star\rangle\}$ consists of a single element, so that it is well-founded in any case). Since $F_{Z}$ is contained in that order it must be well-founded itself. To establish the other direction we show the following: For any $x\in X$ the order $D^{H[x]}_{Z}$ can be embedded into $F_{Z^{\top}}$, where $Z^{\top}=Z\cup\{\top\}$ extends $Z$ by a new maximal element. Let us write $\iota:Z\hookrightarrow Z^{\top}$ for the inclusion. Definition 2.4 and Proposition 2.5 tell us that $D^{H[x]}_{\iota}(\langle a,\tau\rangle)=\langle[\iota]^{<\omega}(a),\tau\rangle=\langle a,\tau\rangle$ defines an embedding of $D^{H[x]}_{Z}$ into $D^{H[x]}_{Z^{\top}}$. Since any $a\in[Z]^{<\omega}$ satisfies $a<^{\operatorname{fin}}_{Z^{\top}}\top$ we see that $\langle a,\tau\rangle\mapsto\langle\top,x,\langle a,\tau\rangle\rangle$ is the desired embedding of $D^{H[x]}_{Z}$ into $F_{Z^{\top}}$. ∎

With the previous result we have completed our reconstruction of the functions $h$ and $f$ that appear in the informal argument from the introduction. The latter proceeds by considering an upper derivative $g$ of $f$. It then invokes induction on $\gamma$ to show that each tree $\mathcal{T}_{\gamma}$ can be embedded into the ordinal $g(\gamma+1)\leq g(\alpha)$. To avoid the use of transfinite induction (or recursion) we now give a particularly careful construction of embeddings. This construction will involve the finite orders

[TABLE]

with the same order relation as on $\Sigma_{x}\mathcal{T}$. Let us also recall that $\mathcal{T}_{x}$ carries the Kleene-Brouwer order $<_{\operatorname{KB}}$ with respect to $\mathbb{N}$.

Proposition 3.11** ($\mathbf{RCA}_{0}$).**

Consider a well-order $X$ and an $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees. There is a function $E:\Sigma\mathcal{T}\rightarrow\mathbb{N}$ such that the following holds for any element $x\in X$, any $\sigma,\sigma_{1},\sigma_{2}\in\mathcal{T}_{x}$ and any order $Z$:

1. (i)

Given a (finite) embedding $e:\Sigma_{x}\mathcal{T}\cap\operatorname{len}(\sigma)\rightarrow Z$, we have

[TABLE] 2. (ii)

If $e_{1}:\Sigma_{x}\mathcal{T}\cap\operatorname{len}(\sigma_{1})\rightarrow Z$ and $e_{2}:\Sigma_{x}\mathcal{T}\cap\operatorname{len}(\sigma_{2})\rightarrow Z$ coincide on the intersection of their domains, then we have

[TABLE]

Proof.

We begin by defining $E(\langle x,\sigma\rangle)$ for given $x\in X$ and $\sigma=\langle s_{0},\dots,s_{k-1}\rangle\in\mathcal{T}_{x}$. For $j\in\Sigma_{x}\mathcal{T}\cap k$ we define $n_{j}<|\Sigma_{x}\mathcal{T}\cap k|$ by stipulating that $j$ is the $n_{j}$-th element of $\Sigma_{x}\mathcal{T}\cap k$. For all $j<k$ outside of $\Sigma_{x}\mathcal{T}$ we set $n_{j}=\bot$. Now we put

[TABLE]

To establish (i) we first need $E(\langle x,\sigma\rangle)\in H[x]_{|\operatorname{rng}(e)|}$. Since $e$ is injective its range has the same cardinality as $\Sigma_{x}\mathcal{T}\cap k$ (continuing the notation from above, so that $k=\operatorname{len}(\sigma)$). Thus we do have $n_{j}\in|\operatorname{rng}(e)|^{\bot}$ for all $j<k$. Clause (i) of Definition 3.1 is satisfied by construction. Clause (ii) says nothing but $\sigma\in\mathcal{T}_{x}$. To complete the verification of (i) we need

[TABLE]

For the crucial inclusion $\supseteq$ it suffices to observe that any $n\in|\operatorname{rng}(e)|=|\Sigma_{x}\mathcal{T}\cap k|$ is the position of some $j\in\Sigma_{x}\mathcal{T}\cap k$. To prove property (ii) we compose with the order isomorphism from Lemma 3.3. If $j$ is the $n_{j}$-th element of $\Sigma_{x}\mathcal{T}\cap k$, then $e(j)$ is the $n_{j}$-th element of $\operatorname{rng}(e)$. Thus (still with the same notation as above) we see that $\langle\operatorname{rng}(e),E(\langle x,\sigma\rangle)\rangle$ corresponds to

[TABLE]

where $e_{\bot}:k\rightarrow Z^{\bot}$ extends $e$ by the values $e_{\bot}(j)=\bot$ for $j\notin\Sigma_{x}\mathcal{T}$. With this description it is straightforward to check property (ii): Assume that we have

[TABLE]

and that $e_{1}:\Sigma_{x}\mathcal{T}\cap k\rightarrow Z$ and $e_{2}:\Sigma_{x}\mathcal{T}\cap l\rightarrow Z$ coincide below $\min\{k,l\}$. Since $H[x]_{Z}$ carries the Kleene-Brouwer order with respect to $Z^{\bot}\times\mathbb{N}$ we get

[TABLE]

Up to the isomorphism $H[x]_{Z}\cong D^{H[x]}_{Z}$ this is just as required. ∎

Using the previous result, we now show that the embedding $J$ from Summary 3.5 can be constructed in a weak meta-theory.

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

Consider a well-order $X$ and an $X$-indexed family $\mathcal{T}$ of $\mathbb{N}$-trees. Assume that $G$ and $\xi:F\circ G\Rightarrow G$ form an upper derivative of the normal prae-dilator $F=F[X,\mathcal{T}]$. Then $\Sigma\mathcal{T}$ can be embedded into the order $D^{G}_{X}$.

Proof.

As a preparation we specify two functions that are implicit in the given data: By combining Proposition 2.16, Lemma 2.21 and Lemma 3.9 we get an embedding

[TABLE]

From Definitions 2.10, 2.12 and 2.22 we know that $G=(G,\mu^{G})$ must be a normal prae-dilator and does, as such, give rise to an order preserving function

[TABLE]

We now show that the desired embedding

[TABLE]

can be constructed by a finitary course-of-values recursion. For this purpose we assume that the code of any $\langle x,\sigma\rangle\in\Sigma\mathcal{T}$ is at least as big as the length of the sequence $\sigma$. The value $J(\langle x,\sigma\rangle)$ may then depend on the finite function

[TABLE]

After describing the construction of $J$ we will set up an induction which ensures that $e_{x,\sigma}$ is an embedding. When this is the case Proposition 3.11 yields an element

[TABLE]

In view of Definition 3.8 we can now state the recursive clause for $J$ as

[TABLE]

To conclude the proof we show the following by simultaneous induction on $j$:

1. (i)

If $j$ codes an element of $\Sigma\mathcal{T}$, then we have $J(j)\in D^{G}_{X}$. 2. (ii)

If $j_{1},j_{2}\leq j$ code elements of $\Sigma\mathcal{T}$, then we have

[TABLE] 3. (iii)

If $j$ codes an element of $\Sigma_{x}\mathcal{T}$, then we have $J(j)<_{D^{G}_{X}}D^{\mu^{G}}_{X}(x)$.

To verify the induction step for (i) we write $j=\langle x,\sigma\rangle$. Parts (i) and (ii) of the induction hypothesis guarantee that $e_{x,\sigma}$ is an embedding with values in $D^{G}_{X}$, as promised above. We have seen that this yields $J^{0}(\langle x,\sigma\rangle)\in D^{H[x]}(D^{G}_{X})$. In view of Definition 3.8 we also need

[TABLE]

This holds by part (iii) of the induction hypothesis. To establish the induction step for (ii) we consider an inequality

[TABLE]

If we have $x_{1}<_{X}x_{2}$, then we get $D^{\mu^{G}}_{X}(x_{1})<_{D^{G}_{X}}D^{\mu^{G}}_{X}(x_{2})$ and thus

[TABLE]

As $\xi^{F}$ is order preserving this implies $J(j_{1})<_{D^{G}_{X}}J(j_{2})$. Now assume that $j_{1}<_{\Sigma\mathcal{T}}j_{2}$ holds because we have $x_{1}=x_{2}=:x$ and $\sigma_{1}<_{\operatorname{KB}}\sigma_{2}$ (recall that $\mathcal{T}_{x}$ carries the usual Kleene-Brouwer order). Since $e_{x,\sigma_{1}}$ and $e_{x,\sigma_{2}}$ are restrictions of the same function, they coincide on the intersection of their domains. Thus Proposition 3.11 yields

[TABLE]

which again implies $J(j_{1})<_{D^{G}_{X}}J(j_{2})$. Finally we prove the induction step for (iii). As a preparation we recall that $D^{H[\bot]}(D^{G}_{X})$ consists of the single element $\langle\emptyset,\star\rangle$. In view of Lemma 3.9, Definition 3.6 and Definition 2.12 we have

[TABLE]

Together with Corollary 2.24 we get

[TABLE]

To deduce (iii) we observe that any $j\in\Sigma_{x}\mathcal{T}$ has the form $j=\langle y,\sigma\rangle$ with $y<_{X}x$. The latter implies

[TABLE]

By the above this yields

[TABLE]

as required. ∎

The following result completes our reconstruction of the informal argument and establishes the implication (2)$\Rightarrow$(3) that we have discussed in the introduction. The notions that appear in statement (2) have been made precise in Section 2.

Corollary 3.13**.**

For each $\Pi^{1}_{1}$-formula $\varphi(x)$ (possibly with further free variables) the following is provable in $\mathbf{ACA}_{0}$: If every normal dilator $F$ has an upper derivative $(G,\xi)$ such that $G$ is a dilator, then $\varphi$ satisfies bar induction, i. e. we have

[TABLE]

for any well-order $X=(X,<_{X})$.

Proof.

By the Kleene normal form theorem (see [21, Lemma V.1.4]) there is a bounded arithmetical formula $\theta(\sigma,x)$ such that $\mathbf{ACA}_{0}$ proves

[TABLE]

Here the universal quantifier ranges over all functions $f:\mathbb{N}\rightarrow\mathbb{N}$. Let us recall that $f[n]=\langle f(0),\dots,f(n-1)\rangle$ denotes the sequence that contains the first $n$ values of such a function. Given a sequence $\sigma=\langle\sigma_{0},\dots,\sigma_{\operatorname{len}(\sigma)-1}\rangle$ and a number $n\leq\operatorname{len}(\sigma)$, we similarly write $\sigma[n]=\langle\sigma_{0},\dots,\sigma_{n-1}\rangle$. We can now define an $X$-indexed family $\mathcal{T}=\{\langle x,\sigma\rangle\,|\,x\in X\text{ and }\sigma\in\mathcal{T}_{x}\}$ of $\mathbb{N}$-trees by setting

[TABLE]

for every $x\in X$. Observe that $\forall_{n}\neg\theta(f[n],x)$ is equivalent to the assertion that $f$ is a branch in $\mathcal{T}_{x}$. Thus we have

[TABLE]

where $\mathcal{T}_{x}$ carries the usual Kleene-Brouwer order with respect to $\mathbb{N}$. Let us now assume that the premise of the desired induction statement holds. Then $\mathcal{T}$ is progressive along $X$, using the terminology that we have introduced at the beginning of this section. Consider the prae-dilator $F=F[X,\mathcal{T}]$ that is constructed according to Definition 3.6. From Corollary 3.10 we learn that $F$ is a normal dilator. By the assumption of the present corollary we get a dilator $G$ and a natural transformation $\xi:F\circ G\rightarrow G$ that form an upper derivative of $F$. Theorem 3.12 tells us that $\Sigma\mathcal{T}$ can be embedded into the order $D^{G}_{X}$. The latter is well-founded, because $X$ is a well-order and $G$ is a dilator. Hence $\Sigma\mathcal{T}$ is well-founded as well. It follows that $\mathcal{T}_{x}$ is well-founded for every $x\in X$, which yields the conclusion $\forall_{x\in X}\varphi(x)$ of the desired induction statement. ∎

4. Constructing the derivative

In the present section we show how to construct a derivative $\partial T$ of a given normal prae-dilator $T$. We will see that $\mathbf{RCA}_{0}$ proves the existence of $\partial T$, as well as the fact that it is a derivative. As a consequence we obtain the implication (1)$\Rightarrow$(2) from the introduction. What $\mathbf{RCA}_{0}$ cannot show is that $\partial T$ is a dilator (i. e. that $X\mapsto D^{\partial T}_{X}$ preserves well-foundedness) whenever $T$ is one: Due to Corollary 3.13 this statement implies $\Pi^{1}_{1}$-bar induction. The converse implication, which amounts to (3)$\Rightarrow$(1) from the introduction, will be established in Section 5.

The construction of $\partial T$ can also be exploited to establish general results about derivatives. This relies on the fact that derivatives are essentially unique, as observed after Definition 2.28. We will use this approach to show that the assumptions of Theorem 2.29 are automatic when $(S,\xi)$ is a derivative of $T$.

As mentioned in the introduction, a categorical construction of derivatives has already been given by Aczel [1, 2]. In the following we give a rather informal presentation of his approach in the terminology of the present paper (in particular we are rather liberal about the distinction between coded and class-sized dilators, cf. the discussion after Definition 2.7). Given a normal dilator $T=(T,\mu^{T})$ and an order $X$, Aczel’s idea was to define the value $\partial T_{X}$ as the direct limit of the diagram

[TABLE]

As a direct limit, $\partial T_{X}$ comes with compatible embeddings $j^{n}_{X}:T^{n}_{X}\rightarrow\partial T_{X}$. By the universal property the functions

[TABLE]

glue to an embedding of $\partial T_{X}$ into $T(\partial T_{X})$. The latter is an isomorphism since $T$ preserves direct limits. Thus $\partial T_{X}$ is a fixed-point of $T$, as one would expect if $\partial T$ is to be a derivative. Furthermore, Aczel could show that $\partial T$ preserves well-foundedness if $T$ does. This is a non-trivial matter, since well-foundedness is not preserved under direct limits in general. The proof that it is preserved under the specific limit constructed above makes crucial use of the assumption that $T$ preserves initial segments (cf. the discussion before Lemma 2.8). Finally, Aczel has shown that $\alpha\mapsto\operatorname{otp}(\partial T_{\alpha})$ is the derivative of the normal function $\alpha\mapsto\operatorname{otp}(T_{\alpha})$. Let us mention that he did not give an explicit characterization of derivatives on the level of functors, i. e. he did not formulate an analogue of Definition 2.28.

In order to recover Aczel’s construction in $\mathbf{RCA}_{0}$ we need to approach the direct limit in a particularly finitistic way. Our idea is to represent $\partial T_{X}$ by a system of terms. To see how this works, recall that we want to ensure the existence of an isomorphism $\xi_{X}:T(\partial T_{X})\rightarrow\partial T_{X}$. In view of Lemma 2.6 (and the discussion after Definition 2.7) any element of $T(\partial T_{X})$ corresponds to a pair $\langle a,\sigma\rangle\in D^{T}(\partial T_{X})$, where $a\subseteq\partial T_{X}$ is finite and $\sigma\in T_{|a|}$ satisfies $\operatorname{supp}^{T}_{|a|}(\sigma)=|a|$. Assuming that the elements of $a$ are already represented by terms, we can add a term $\xi\langle a,\sigma\rangle\in\partial T_{X}$ that represents the value of $\langle a,\sigma\rangle$ under $\xi_{X}$. To make this idea precise we switch back to the rigorous framework of coded prae-dilators, as introduced in Section 2. In particular we want to construct $\partial T$ as a coded prae-dilator, which leads us to focus on the values $\partial T_{n}$ for the finite orders $n=\{0,\dots,n-1\}$. Let us first specify the underlying set of the order $\partial T_{n}$:

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

Consider a normal prae-dilator $T=(T,\operatorname{supp}^{T},\mu^{T})$. For each number $n$ we define a term system $\partial T_{n}$ by the following inductive clauses:

1. (i)

We have a term $\mu_{m}\in\partial T_{n}$ for every number $m<n$. 2. (ii)

Given a finite set $a\subseteq\partial T_{n}$ of terms and a $\sigma\in T_{|a|}$ with $\operatorname{supp}^{T}_{|a|}(\sigma)=|a|$, we get a term $\xi\langle a,\sigma\rangle\in\partial T_{n}$, provided that the following holds: If we have $a=\{\mu_{m}\}$ for some $m<n$, then $\sigma$ must be different from $\mu^{T}_{1}(0)\in T_{1}$.

Note that the term systems $\partial T_{n}$ are uniformly computable (with respect to $n$), so that $\mathbf{RCA}_{0}$ proves the existence of the set

[TABLE]

This is crucial if we want to extend $\partial T$ into a coded prae-dilator (cf. the discussion after Definition 2.2). In order to understand the proviso in clause (ii) one should think of $\mu_{m}$ as a notation for $f^{\prime}(m)$, where $f$ is the normal function induced by $T$ and $f^{\prime}$ is its derivative. In the proof of Proposition 2.14 we have seen that $D^{\mu^{T}}$ amounts to an internal version of the function $f$. Together with Definition 2.12 we see that $\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle=D^{\mu^{T}}_{\partial T_{n}}(\mu_{m})$ corresponds to $f(f^{\prime}(m))$. Since the latter is equal to $f^{\prime}(m)$ the terms $\xi\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$ and $\mu_{m}$ would represent the same ordinal. To keep our notations unique, the first of these terms has been excluded in clause (ii). A formal version of this intuitive explanation will play a role in the proof of Theorem 4.13. The following notion of term length will be used to define the order on $\partial T_{n}$:

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

For each $n$ we define a length function $L^{\partial T}_{n}:\partial T_{n}\rightarrow\mathbb{N}$ by recursion over the build-up of terms, setting

[TABLE]

where $\ulcorner s\urcorner$ denotes the code (Gödel number) of the term $s$.

Note that $\ulcorner s\urcorner$ coincides with $s$ if Definition 4.1 is already arithmetized. The role of the Gödel numbers is to justify certain applications of induction and recursion over the length of terms: In view of $\ulcorner s\urcorner\leq L^{\partial T}_{n}(s)$ a quantifier of the form

[TABLE]

is bounded. Thus such a quantifier does not lead out of the $\Sigma^{0}_{1}$-formulas, for which induction is available in $\mathbf{RCA}_{0}$. To construct a binary relation $<_{\partial T_{n}}$ on $\partial T_{n}$, the following definition decides $s<_{\partial T_{n}}t$ by recursion on $L^{\partial T}_{n}(s)+L^{\partial T}_{n}(t)$. In case we have $s=\xi\langle a,\sigma\rangle$ and $t=\xi\langle b,\tau\rangle$ we can assume that the restriction of $<_{\partial T_{n}}$ to $a\cup b$ is already determined (note that $r\in a$ yields $2\cdot L^{\partial T}_{n}(r)<L^{\partial T}_{n}(s)$, so that we can decide $r<_{\partial T_{n}}r$). In particular we can check whether $<_{\partial T_{n}}$ is a linear order on the finite set $a\cup b$. If it is, then we may refer to the functions $|\iota_{a}^{a\cup b}|$ and $|\iota_{b}^{a\cup b}|$ from Definition 2.4. More explicitly, we can write $\operatorname{en}_{a}:|a|\rightarrow a$ and $\operatorname{en}_{a\cup b}:|a\cup b|\rightarrow a\cup b$ for the unique increasing enumerations with respect to $<_{\partial T_{n}}$. Then the function $|\iota_{a}^{a\cup b}|:|a|\rightarrow|a\cup b|$ is characterized by the fact that it satisfies $\operatorname{en}_{a\cup b}\circ|\iota_{a}^{a\cup b}|=\iota_{a}^{a\cup b}\circ\operatorname{en}_{a}$, where $\iota_{a}^{a\cup b}:a\hookrightarrow a\cup b$ is the inclusion. Before Lemma 2.8 we have seen that a linear order $<_{X}$ on a set $X$ induces relations $<^{\operatorname{fin}}_{X}$ and $\leq^{\operatorname{fin}}_{X}$ between finite subsets of $X$. In the following we use $<^{\operatorname{fin}}_{\partial T_{n}}$ and $\leq^{\operatorname{fin}}_{\partial T_{n}}$ as abbreviations, without assuming that $<_{\partial T_{n}}$ is linear on the relevant parts of $X$. In particular we have

[TABLE]

for any element $s\in\partial T_{n}$ and any finite subset $b\subseteq\partial T_{n}$. Note that $s\leq_{\partial T_{n}}r$ abbreviates ${s<_{\partial T_{n}}r}\lor{s=r}$, where the second disjunct refers to the equality of terms. We can now state the definition of the desired order relation:

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

For each $n$ we define a binary relation $<_{\partial T_{n}}$ on $\partial T_{n}$. Invoking recursion on $L^{\partial T}_{n}(s)+L^{\partial T}_{n}(t)$, we stipulate that $s<_{\partial T_{n}}t$ holds if, and only if, one of the following is satisfied:

1. (i)

We have $s=\mu_{m}$ and

• •

either $t=\mu_{k}$ and $m<k$,

• •

or $t=\xi\langle b,\tau\rangle$ and $s\leq^{\operatorname{fin}}_{\partial T_{n}}b$. 2. (ii)

We have $s=\xi\langle a,\sigma\rangle$ and

• •

either $t=\mu_{k}$ and $a<^{\operatorname{fin}}_{\partial T_{n}}t$,

• •

or we have $t=\xi\langle b,\tau\rangle$, the restriction of $<_{\partial T_{n}}$ to $a\cup b$ is linear, and we have $T_{|\iota_{a}^{a\cup b}|}(\sigma)<_{T_{|a\cup b|}}T_{|\iota_{b}^{a\cup b}|}(\tau)$.

To show that $<_{\partial T_{n}}$ is a linear order we will need the following auxiliary result:

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

If $T$ is a normal prae-dilator, then we have

[TABLE]

for any number $k$ and arbitrary elements $\sigma,\tau\in T_{k}$.

Proof.

If the conclusion of the implication is false, then we have $\operatorname{supp}^{T}_{k}(\tau)<^{\operatorname{fin}}m$ for some $m\in\operatorname{supp}^{T}_{k}(\sigma)$. Note that $\operatorname{supp}^{T}_{k}(\sigma)<^{\operatorname{fin}}m$ must fail. In view of Definition 2.10 we obtain $\tau<_{T_{k}}\mu^{T}_{k}(m)\leq_{T_{k}}\sigma$, so that the premise of our implication is false. ∎

We can now establish the expected fact:

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

Given a normal prae-dilator $T$ and any number $n$, the relation $<_{\partial T_{n}}$ is a linear order on the term system $\partial T_{n}$.

Proof.

It is straightforward to see that $s<_{\partial T_{n}}s$ must fail for every $s$, based on the fact that the linear order $<_{T_{k}}$ is antisymmetric for any number $k$. We now show

[TABLE]

by simultaneous induction on $L^{\partial T}_{n}(s)+L^{\partial T}_{n}(t)$ resp. $L^{\partial T}_{n}(r)+L^{\partial T}_{n}(s)+L^{\partial T}_{n}(t)$. Trichotomy is immediate if we have $s=\mu_{m}$ and $t=\mu_{k}$ with $m,k<n$. If we have $s=\mu_{m}$ and $t=\xi\langle b,\tau\rangle$, then the induction hypothesis yields $s\leq^{\operatorname{fin}}_{\partial T_{n}}b$ or $b<^{\operatorname{fin}}_{\partial T_{n}}s$. In the first case we get $s<_{\partial T_{n}}t$ while the second leads to $t<_{\partial T_{n}}s$. Now assume that we have $s=\xi\langle a,\sigma\rangle$ and $t=\xi\langle b,\tau\rangle$. The simultaneous induction hypothesis ensures that $<_{\partial T_{n}}$ is linear on $a\cup b$ (note that $s^{\prime}<_{\partial T_{n}}t^{\prime}\land t^{\prime}<_{\partial T_{n}}s^{\prime}\rightarrow s^{\prime}<_{\partial T_{n}}s^{\prime}$ is covered, due to the factor $2$ in the definition of $L^{\partial T}_{n}$). It is easy to conclude unless we have $T_{|\iota_{a}^{a\cup b}|}(\sigma)=T_{|\iota_{b}^{a\cup b}|}(\tau)$. In this case the naturality of $\operatorname{supp}^{T}$ yields

[TABLE]

Composing both sides with $[\operatorname{en}_{a\cup b}]^{<\omega}$ we get $a=b$. Then $|\iota_{a}^{a\cup b}|$ and $|\iota_{b}^{a\cup b}|$ must be the identity on $|a|=|a\cup b|=|b|$. As $T$ is functorial we get $\sigma=\tau$ and hence $s=t$. To establish transitivity one needs to distinguish several cases according to the form of the terms $r,s$ and $t$. In the first interesting case we have $r=\mu_{m}$, $s=\xi\langle a,\sigma\rangle$ and $t=\xi\langle b,\tau\rangle$. Invoking the previous lemma we see that $s<_{\partial T_{n}}t$ implies

[TABLE]

Again we compose both sides with $[\operatorname{en}_{a\cup b}]^{<\omega}$, to get $a\leq^{\operatorname{fin}}_{\partial T_{n}}b$. In view of $r<_{\partial T_{n}}s$ we have $\mu_{m}\leq^{\operatorname{fin}}_{\partial T_{n}}a$. Using the induction hypothesis we can infer $\mu_{m}\leq^{\operatorname{fin}}_{\partial T_{n}}b$ and thus $r<_{\partial T_{n}}t$. Let us now consider $r=\xi\langle a,\sigma\rangle$, $s=\mu_{m}$ and $t=\xi\langle b,\tau\rangle$. In this situation $r<_{\partial T_{n}}s<_{\partial T_{n}}t$ amounts to $a<^{\operatorname{fin}}_{\partial T_{n}}s\leq^{\operatorname{fin}}_{\partial T_{n}}b$, which implies that $b\leq^{\operatorname{fin}}_{\partial T_{n}}a$ must fail. Similarly to the previous case we can conclude

[TABLE]

Note that we can refer to $|\iota_{a}^{a\cup b}|$ and $|\iota_{b}^{a\cup b}|$, since the simultaneous induction hypothesis ensures that $<_{\partial T_{n}}$ is linear on $a\cup b$. Using the previous lemma and trichotomy for $<_{T_{|a\cup b|}}$ we obtain $T_{|\iota_{a}^{a\cup b}|}(\sigma)<_{T_{|a\cup b|}}T_{|\iota_{b}^{a\cup b}|}(\tau)$ and hence $r<_{\partial T_{n}}t$. To establish transitivity for $r=\xi\langle a,\sigma\rangle$, $s=\xi\langle b,\tau\rangle$ and $t=\xi\langle c,\rho\rangle$ it suffices to considers the inclusions into $a\cup b\cup c$ and to use transitivity for $<_{T_{|a\cup b\cup c|}}$. ∎

We will see that the following turns $n\mapsto\partial T_{n}$ into a functor:

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

Given a strictly increasing function $f:n\rightarrow l$, we define a function $\partial T_{f}:\partial T_{n}\rightarrow\partial T_{l}$ by recursion over the build-up of terms, setting

[TABLE]

The fact that $\partial T_{f}$ has values in $\partial T_{l}$ is established as part of the following proof:

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

If $f:n\rightarrow l$ is strictly increasing, then $\partial T_{f}:\partial T_{n}\rightarrow\partial T_{l}$ is an order embedding.

Proof.

By simultaneous induction on $L^{\partial T}_{n}(r)$ resp. $L^{\partial T}_{n}(s)+L^{\partial T}_{n}(t)$ one can verify

[TABLE]

Let us consider the first claim for $r=\xi\langle a,\sigma\rangle$: The simultaneous induction hypothesis implies that $\partial T_{f}$ is order preserving and hence injective on $a$. In particular we have $|[\partial T_{f}]^{<\omega}(a)|=|a|$. Furthermore, it is easy to see that $[\partial T_{f}]^{<\omega}(a)=\{\mu_{k}\}$ implies $a=\{\mu_{m}\}$ with $k=f(m)$. Invoking Definition 4.1 we can now conclude that $r\in\partial T_{n}$ implies $\partial T_{f}(r)=\xi\langle[\partial T_{f}]^{<\omega}(a),\sigma\rangle\in\partial T_{l}$. To verify that $\partial T_{f}$ is order preserving we distinguish cases according to the form of $s$ and $t$. In the first interesting case we have $s=\mu_{m}<_{\partial T_{n}}\xi\langle b,\tau\rangle=t$ because of $s\leq^{\operatorname{fin}}_{\partial T_{n}}b$. By the induction hypothesis we obtain $\partial T_{f}(s)\leq^{\operatorname{fin}}_{\partial T_{k}}[\partial T_{f}]^{<\omega}(b)$ and hence

[TABLE]

Let us also consider the case where $s=\xi\langle a,\sigma\rangle<_{\partial T_{k}}\xi\langle b,\tau\rangle=t$ holds because we have $T_{|\iota_{a}^{a\cup b}|}(\sigma)<_{T_{|a\cup b|}}T_{|\iota_{b}^{a\cup b}|}(\tau)$. To infer $\partial T_{f}(s)<_{\partial T_{k}}\partial T_{f}(t)$ it suffices to show

[TABLE]

By the definition of the functor $|\cdot|$ (cf. the paragraph after Summary 2.1), the first of these equations reduces to

[TABLE]

The induction hypothesis tells us that $\partial T_{f}$ is order preserving on $a\cup b$. Since the increasing enumeration of a finite order is uniquely determined this yields

[TABLE]

Together with $\operatorname{en}_{a\cup b}\circ|\iota_{a}^{a\cup b}|=\iota_{a}^{a\cup b}\circ\operatorname{en}_{a}$ we indeed get

[TABLE]

The equation with $b$ at the place of $a$ is established in the same way. ∎

To get a normal prae-dilator (cf. Definitions 2.2 and 2.10) we need the following:

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

For each $n$ we define a function $\operatorname{supp}^{\partial T}_{n}:\partial T_{n}\rightarrow[n]^{<\omega}$ by induction on the build-up of terms, setting

[TABLE]

To define a family of functions $\mu^{\partial T}_{n}:n\rightarrow\partial T_{n}$ we put

[TABLE]

for all numbers $m<n$.

Let us verify that $\partial T=(\partial T,\operatorname{supp}^{\partial T},\mu^{\partial T})$ has the expected property:

Proposition 4.9** ($\mathbf{RCA}_{0}$).**

If $T$ is a normal prae-dilator, then so is $\partial T$.

Proof.

From Lemma 4.5 we know that $\partial T_{n}$ is a linear order for any number $n$. Lemma 4.7 tells us that $f\mapsto\partial T_{f}$ maps morphisms to morphisms. A straightforward induction over the build-up of terms establishes the functoriality of $\partial T$ and the naturality of $\operatorname{supp}^{\partial T}$. By another induction one can prove the implication

[TABLE]

where $\iota_{a}:a\hookrightarrow n$ denotes the inclusion of a given $a\subseteq n$. For $a=\operatorname{supp}^{\partial T}_{n}(s)$ this amounts to the support condition from clause (ii) of Definition 2.2. We have thus established that $\partial T$ is a coded prae-dilator. The functions $\mu^{\partial T}_{n}:n\rightarrow\partial T_{n}$ clearly form a natural family of embeddings. In view of Definitions 4.3 and 4.8 a straightforward induction on the build-up of $s$ shows

[TABLE]

According to Definition 2.10 this means that $\partial T$ is normal. ∎

Our next goal is to turn $\partial T$ into an upper derivative of $T$. According to Definition 2.22 we need to construct a morphism $\xi^{T}:T\circ\partial T\Rightarrow T$ of normal prae-dilators. Concerning the notion of composition, Definitions 2.15 and 2.4 tell us that any element of $(T\circ\partial T)_{n}=D^{T}(\partial T_{n})$ has the form $\langle a,\sigma\rangle$, where $a\subseteq\partial T_{n}$ is finite and $\sigma\in T_{|a|}$ satisfies $\operatorname{supp}^{T}_{|a|}(\sigma)=|a|$. In view of Definition 4.1 this justifies the following construction:

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

For each $n$ we define a function $\xi^{T}_{n}:(T\circ\partial T)_{n}\rightarrow\partial T_{n}$ by setting

[TABLE]

The following result is important as it implies the implication (1)$\Rightarrow$(2) from the introduction of this paper.

Proposition 4.11** ($\mathbf{RCA}_{0}$).**

If $T$ is a normal prae-dilator, then $(\partial T,\xi^{T})$ is an upper derivative of $T$.

Proof.

In view of Definition 2.22 we must establish that $\xi^{T}:T\circ\partial T\Rightarrow\partial T$ is a morphism of normal prae-dilators, as characterized by Definition 2.20. Let us first show that each function $\xi^{T}_{n}:(T\circ\partial T)_{n}\rightarrow\partial T_{n}$ is an embedding. To make the results from Section 2 applicable we observe that Definition 2.12 yields

[TABLE]

To see that $s<_{D^{T}(\partial T_{n})}t$ implies $\xi^{T}_{n}(s)<_{\partial T_{n}}\xi^{T}_{n}(t)$ we now distinguish cases according to the form of $s$ and $t$. First assume that we have

[TABLE]

From Proposition 2.13 we know that $D^{\mu^{T}}_{\partial T_{n}}$ is an embedding. Thus we indeed get

[TABLE]

Now consider the case

[TABLE]

where $\langle a,\sigma\rangle$ is not of the form $\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$. By Proposition 2.13 we get $a<^{\operatorname{fin}}_{\partial T_{n}}\mu_{k}$. Invoking Definition 4.3 we can conclude

[TABLE]

The case where we have $s=\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$ and $t=\langle b,\tau\rangle$ is of a different form is treated analogously (infer $\mu_{m}\leq^{\operatorname{fin}}_{\partial T_{n}}b$ from the fact that $b<^{\operatorname{fin}}_{\partial T_{n}}\mu_{m}$ must fail). Finally we consider the case where we have

[TABLE]

and neither $s$ nor $t$ is of the form $\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$ with $m<n$. By Definition 2.4 we get $T_{|\iota_{a}^{a\cup b}|}(\sigma)<_{T_{|a\cup b|}}T_{|\iota_{b}^{a\cup b}|}(\tau)$. In view of Definition 4.3 this yields

[TABLE]

Let us now show that $\xi^{T}$ is natural: Given a strictly increasing function $f:n\rightarrow k$, we invoke Definitions 2.15 and 2.4 to obtain

[TABLE]

First assume $\langle a,\sigma\rangle=\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$. Using Definition 4.6 we compute

[TABLE]

Now assume that $\langle a,\sigma\rangle$ does not have the form $\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$. Then $\langle[\partial T_{f}]^{<\omega}(a),\sigma\rangle$ does not have this form either. Again by Definition 4.6 we get

[TABLE]

To conclude that $\xi^{T}:T\circ\partial T\Rightarrow T$ is a morphism of normal prae-dilators we must show $\xi^{T}\circ\mu^{T\circ\partial T}=\mu^{\partial T}$ (cf. Definition 2.20). By Definition 2.17 we indeed get

[TABLE]

for all numbers $m<n$. ∎

In the construction of $\partial T$ we have only added terms that were needed as values of $\xi:T\circ\partial T\Rightarrow\partial T$. The resulting minimality of $\partial T$ leads to the following:

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

Assume that $T$ is a normal prae-dilator. Then $(\partial T,\xi^{T})$ is a derivative of $T$.

Proof.

The previous proposition tells us that $(\partial T,\xi^{T})$ is an upper derivative. In view of Definition 2.28 we assume that $S$ and $\xi^{\prime}:T\circ S\Rightarrow S$ form an upper derivative of $T$ as well. We must show that there is a unique morphism $\nu:\partial T\Rightarrow S$ of upper derivatives. Let us begin with existence: Note that the normality of $S$ is witnessed by a natural family of embeddings $\mu^{S}_{n}:n\rightarrow S_{n}$. Also recall that $(T\circ S)_{n}=D^{T}(S_{n})$ consists of pairs $\langle b,\sigma\rangle$, where $b\subseteq S_{n}$ is finite and $\sigma\in T_{|b|}$ satisfies $\operatorname{supp}^{T}_{|b|}(\sigma)=|b|$. For each $n$ we define $\nu_{n}:\partial T_{n}\rightarrow S_{n}$ by recursion over the build-up of terms, setting

[TABLE]

It is not immediately clear that the second clause produces values in $S_{n}$: To see that $\xi\langle a,\sigma\rangle$ implies $\langle[\nu_{n}]^{<\omega}(a),\sigma\rangle\in D^{T}(S_{n})$ we need $|[\nu_{n}]^{<\omega}(a)|=|a|$, which relies on the fact that $\nu_{n}$ is order preserving and hence injective. This suggests to verify

[TABLE]

by simultaneous induction on $L^{\partial T}_{n}(r)$ resp. $L^{\partial T}_{n}(s)+L^{\partial T}_{n}(t)$. To establish that $\nu_{n}$ is order preserving one needs to consider different possibilities for the form of $s$ and $t$. The first interesting case is

[TABLE]

According to Definition 4.3 we have $a<^{\operatorname{fin}}_{\partial T_{n}}\mu_{m}$, so that the induction hypothesis yields $[\nu_{n}]^{<\omega}(a)<^{\operatorname{fin}}_{S_{n}}\mu^{S}_{n}(m)$. By Definition 2.10 we get $\operatorname{supp}^{S}_{n}(\nu_{n}(r))<^{\operatorname{fin}}m$ for all $r\in a$. Using Lemma 2.19 and Definition 2.15 we obtain

[TABLE]

By the other direction of Definition 2.10 this implies

[TABLE]

as desired. Let us next consider the case where

[TABLE]

holds because of $\mu_{m}\leq^{\operatorname{fin}}_{\partial T_{n}}b$. Similarly to the above one can deduce that the statements $\operatorname{supp}^{S}_{n}(\nu_{n}(t))<^{\operatorname{fin}}m$ and $\nu_{n}(t)<_{S_{n}}\mu^{S}_{n}(m)=\nu_{n}(s)$ must fail. In order to conclude $\nu_{n}(s)<_{S_{n}}\nu_{n}(t)$ we shall now establish $\nu_{n}(s)\neq\nu_{n}(t)$. According to Definition 2.17 the normality of $T\circ S$ is witnessed by the functions

[TABLE]

Since $\xi^{\prime}$ is a morphism of normal prae-dilators we get

[TABLE]

Invoking the injectivity of the embedding $\xi^{\prime}_{n}$ we learn that $\nu_{n}(s)=\nu_{n}(t)$ would imply $\langle\{\nu_{n}(\mu_{m})\},\mu^{T}_{1}(0)\rangle=\langle[\nu_{n}]^{<\omega}(b),\tau\rangle$. By induction hypothesis $\nu_{n}$ is injective on $b\cup\{\mu_{m}\}$. Hence $\nu_{n}(s)=\nu_{n}(t)$ would even yield $t=\xi\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$. This possibility, however, has been excluded in Definition 4.1. Finally we assume that

[TABLE]

holds because of $T_{|\iota_{a}^{a\cup b}|}(\sigma)<_{T_{|a\cup b|}}T_{|\iota_{b}^{a\cup b}|}(\tau)$. The induction hypothesis ensures that $\nu_{n}$ is order preserving on $a\cup b$. As in the proof of Lemma 4.7 one can show

[TABLE]

Invoking Definition 2.4 one then obtains $\langle[\nu_{n}]^{<\omega}(a),\sigma\rangle<_{D^{T}(S_{n})}\langle[\nu_{n}]^{<\omega}(b),\tau\rangle$. Since $\xi^{\prime}_{n}$ is an embedding of $(T\circ S)_{n}=D^{T}(S_{n})$ into $S_{n}$ this implies

[TABLE]

So far we have established that each function $\nu_{n}$ is an embedding of $\partial T_{n}$ into $S_{n}$. To conclude that these embeddings form a morphism of prae-dilators we must show that they are natural: Given a strictly increasing function $f:n\rightarrow k$, we establish $\nu_{k}\circ\partial T_{f}(s)=S_{f}\circ\nu_{n}(s)$ by induction on the build-up of $s$. In the case of $s=\mu_{m}$ we invoke the naturality of $\mu^{S}$ to get

[TABLE]

Let us now establish the induction step for $s=\xi\langle a,\sigma\rangle$. In view of Definitions 2.15 and 2.4 the induction hypothesis yields

[TABLE]

Together with the naturality of $\xi^{\prime}:T\circ S\Rightarrow S$ we get

[TABLE]

as required. Next we observe

[TABLE]

which shows that $\nu$ is a morphism of normal prae-dilators. To conclude that we have a morphism of upper derivatives we need to establish $\nu\circ\xi^{T}=\xi^{\prime}\circ T(\nu)$. First observe that Definitions 2.25 and 2.4 yield

[TABLE]

If $\langle a,\sigma\rangle\in(T\circ\partial T)_{n}$ is not of the form $\langle\{\mu_{m}\},\mu^{T}_{1}(0)\rangle$, then we obtain

[TABLE]

In the remaining case Definition 4.10 yields

[TABLE]

Invoking Definition 2.17 and the fact that $\xi^{\prime}:T\circ S\Rightarrow S$ is a morphism of normal prae-dilators we also get

[TABLE]

To complete the proof we must show that $\nu$ is unique: Given an arbitrary morphism $\nu^{\prime}:\partial T\Rightarrow S$ of upper derivatives, we establish $\nu^{\prime}(s)=\nu(s)$ by induction on the build-up of $s$. In the case of $s=\mu_{m}$ we invoke Definition 4.8 and the assumption that $\nu^{\prime}$ is a morphism of normal prae-dilators to get

[TABLE]

Given a term $s=\xi\langle a,\sigma\rangle$, we observe that the induction hypothesis implies

[TABLE]

Together with the assumption that $\nu^{\prime}$ is a morphism of upper derivatives we obtain

[TABLE]

as required. ∎

We have described a construction that yields a derivative $\partial T$ of a given normal prae-dilator $T$. Since derivatives are essentially unique, the construction of $\partial T$ can be exploited to prove general properties of derivatives. The following result establishes some of the assumptions from Theorem 2.29. The remaining assumption, which states that $X\mapsto D^{S}_{X}$ preserves well-foundedness, will be considered in the next section (in view of Corollary 3.13 this will require a stronger base theory).

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

Consider a normal prae-dilator $T$. If $(S,\xi)$ is a derivative of $T$, then $\xi:T\circ S\Rightarrow S$ is a natural isomorphism. Furthermore

[TABLE]

is an equalizer diagram for every number $n$.

Proof.

The definition of derivative ensures that $\xi$ is a natural transformation. To conclude that it is a natural isomorphism we show that $\xi_{n}:(T\circ S)_{n}\rightarrow S_{n}$ is surjective for each $n$. Since both $(S,\xi)$ and $(\partial T,\xi^{T})$ are derivatives of $T$, there is an isomorphism $\nu:S\Rightarrow\partial T$ of upper derivatives (cf. the remark after Definition 2.28). In view of Definitions 2.27 and 2.25 we have

[TABLE]

Now $\nu_{n}$ is bijective, and it is straightforward to infer that the same holds for $D^{T}(\nu_{n})$. So it suffices to show that $\xi^{T}_{n}$ is surjective. Aiming at the latter, we first observe that Definitions 4.8 and 2.20 yield

[TABLE]

It remains to consider an element $\xi\langle a,\sigma\rangle\in\partial T_{n}$. In view of Definitions 4.1, 2.4 and 2.15 we have $\langle a,\sigma\rangle\in D^{T}(\partial T_{n})=(T\circ\partial T)_{n}$. Thus we get

[TABLE]

which completes the proof that $\xi$ is a natural isomorphism. After the statement of Theorem 2.29 above we have observed that the given equalizer diagram is automatically commutative. To establish that $\mu^{S}_{n}$ is an equalizer of $\xi_{n}\circ D^{\mu^{T}}_{S_{n}}$ and the identity we must show that

[TABLE]

holds for any element $s\in S_{n}$. To reduce the claim to the special case with $(\partial T,\xi^{T})$ at the place of $(S,\xi)$ we apply $\nu_{n}$ to both sides of the antecedent. Using the naturality of $D^{\mu^{T}}$, which is provided by Lemma 2.13, this yields

[TABLE]

Assuming the special case of the desired implication, we obtain $\nu_{n}(s)\in\operatorname{rng}(\mu^{\partial T}_{n})$, say $\nu_{n}(s)=\mu^{\partial T}_{n}(m)$. Since $\nu$ is a morphism of normal prae-dilators, this implies

[TABLE]

Invoking the injectivity of $\nu_{n}$ we see $s=\mu^{S}_{n}(m)\in\operatorname{rng}(\mu^{S}_{n})$, which is the conclusion of the general case. It remains to establish the special case for $\partial T$. Aiming at the contrapositive of the desired implication, let us assume that $s\in\partial T_{n}$ is not of the form $\mu^{S}_{n}(m)=\mu_{m}$. Then Definitions 2.12 and 4.10 yield

[TABLE]

The term on the right cannot be equal to $s$, which it contains as a proper subterm (one can also appeal to the fact that $s$ is shorter in the sense of Definition 4.2). ∎

To conclude this section we show that the conditions from the previous theorem do not suffice to characterize derivatives on the categorical level:

Example 4.14**.**

Define a normal dilator $T$ by setting $T_{n}=\{0,\dots,n-1\}$, $T_{f}=f$, $\operatorname{supp}^{T}_{n}(m)=\{m\}$ and $\mu^{T}_{n}(m)=m$. Furthermore, consider the sets

[TABLE]

with the expected ordering (i. e. such that $\hat{p}<_{S_{n}}\hat{q}<_{S_{n}}m<_{S_{n}}k$ holds for all $p<q$ from $\mathbb{Z}$ and all $m<k$ from $\{0,\dots,n-1\}$). To turn $S$ into a prae-dilator we set

[TABLE]

Let us point out that $S$ is not a dilator, since $D^{S}_{n}\cong S_{n}$ is ill-founded (cf. Lemma 2.6). Be that as it may, we obtain a normal prae-dilator by setting

[TABLE]

Since all supports with respect to $T$ are singletons we have

[TABLE]

Thus we can define $\xi:T\circ S\Rightarrow S$ by setting

[TABLE]

One can check that $(S,\xi)$ is an upper derivative of $T$. It is easy to see that $\xi$ is an isomorphism, as $p\mapsto p+1$ is an automorphism of $\mathbb{Z}$. Furthermore, the diagram from Theorem 4.13 defines an equalizer: Assume that we have

[TABLE]

In view of $p\neq p+1$ we cannot have $\sigma=\hat{p}$ with $p\in\mathbb{Z}$. Thus we must have $\sigma=m$ for some number $m\in\{0,\dots,n-1\}$. It follows that

[TABLE]

lies in the range of $\mu^{S}_{n}$, as required for the equalizer condition. Thus $S$ and $\xi$ satisfy the conclusion of the previous theorem. Nevertheless they do not form a derivative of $T$. Otherwise we would get a morphism $S\Rightarrow\partial T$ of upper derivatives. This is impossible since $S_{n}=\mathbb{Z}+n$ is infinite while $\partial T_{n}$ is finite: In view of $T_{1}=\{\mu^{T}_{1}(0)\}$ Definition 4.1 yields $\partial T_{n}=\{\mu_{m}\,|\,0\leq m<n\}$.

5. From $\Pi^{1}_{1}$-bar induction to preservation of well-foundedness

In this section we use $\Pi^{1}_{1}$-bar induction to prove the following: If $T$ is a normal dilator, then $X\mapsto D^{\partial T}_{X}$ preserves well-foundedness, so that $\partial T$ is a normal dilator as well. This establishes the implication (3)$\Rightarrow$(1) from the introduction. Together with the results of the previous sections we learn that (1), (2) and (3) are equivalent over $\mathbf{ACA}_{0}$. Invoking Theorems 2.29 and 4.13 we will also be able to conclude the following: If $(S,\xi)$ is a derivative of a normal dilator $T$, then $\alpha\mapsto\operatorname{otp}(D^{S}_{\alpha})$ is the derivative (in the usual sense) of the normal function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$.

The construction from the previous section yields a derivative $\partial T$ of a given normal prae-dilator $T$. To assess whether $\partial T$ is a dilator we must consider the orders $D^{\partial T}_{X}$ (cf. Definitions 2.4 and 2.7). These will be approximated as follows:

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

Consider a normal prae-dilator $T$, as well as a linear order $X=(X,<_{X})$. We set

[TABLE]

for any element $x\in X$.

To distinguish the expressions $\partial T_{X}^{x}$ and $\partial T_{n}$ (cf. Definition 4.1) it suffices to observe that the latter has no superscript (note that we have $\partial T_{n}^{m}\subseteq D^{\partial T}_{n}$ rather than $\partial T_{n}^{m}\subseteq\partial T_{n}$ in case $X=n=\{0,\dots,n-1\}$). We will argue by induction on $x$ to show that the suborders $\partial T^{x}_{X}\subseteq D^{\partial T}_{X}$ are well-founded. Assuming that $X$ is non-empty and has no maximal element, we clearly have

[TABLE]

In general, the union (or direct limit) of compatible well-orders does not need to be well-founded itself. On the other hand it is straightforward to see that an order is well-founded if it is the union of well-founded initial segments. In the present situation we can combine Propositions 4.9 and 2.13 to get the following:

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

Consider a normal prae-dilator $T$ and a linear order $X$. For any $x\in X$ we have

[TABLE]

In particular $\partial T^{x}_{X}$ is an initial segment of $D^{\partial T}_{X}$.

The assumption that $T$ and hence $\partial T$ is normal is crucial for the previous lemma and for many of the following results (cf. the remarks before Lemma 2.8, as well as the discussion of Aczel’s construction at the beginning of Section 4). Assuming that $\partial T^{y}_{X}$ is well-founded for every $y<_{X}x$, the lemma allows us to conclude that $\bigcup_{y<_{X}x}\partial T_{X}^{y}$ is well-founded. To complete the induction step one needs to deduce the well-foundedness of $\partial T^{x}_{X}$. For this purpose we approximate $\partial T^{x}_{X}$ by distinguishing terms of different height (cf. Definition 4.1):

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

Let $T$ be a normal prae-dilator. We define a family of functions $\operatorname{ht}^{\partial T}_{n}:\partial T_{n}\rightarrow\mathbb{N}$ by induction over the build-up of terms, setting

[TABLE]

Given an order $X$ and an element $x\in X$, we put

[TABLE]

for every number $k$.

According to Definition 4.6 and Lemma 4.7, any strictly increasing function $f:n\rightarrow k$ yields an embedding $\partial T_{f}:\partial T_{n}\rightarrow\partial T_{k}$. We will need to know that these embeddings respect our height functions:

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

Consider a normal prae-dilator $T$ and a strictly increasing function $f:n\rightarrow k$. We have

[TABLE]

for any element $s\in\partial T_{n}$.

Proof.

The claim can be verified by a straightforward induction on the build-up of $s$. Concerning the case $s=\xi\langle a,\sigma\rangle$, we point out that $\partial T_{f}(s^{\prime})$ is $<_{\partial T_{k}}$-maximal in $[\partial T_{f}]^{<\omega}(a)$ if $s^{\prime}$ is $<_{\partial T_{n}}$-maximal in $a$. ∎

Yet again, it will be crucial that Definition 5.3 provides an approximation by initial segments. To show that this is the case we need a partial converse to Lemma 4.4:

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

If $T$ is a normal prae-dilator, then we have

[TABLE]

for any number $n$ and arbitrary elements $s,t\in\partial T_{n}$.

Proof.

We establish the claim by induction on $L^{\partial T}_{n}(s)+L^{\partial T}_{n}(t)$, relying on the length function from Definition 4.2. To prove the induction step we distinguish cases according to the form of $s$ and $t$. In any case we assume $\operatorname{supp}^{\partial T}_{n}(s)\leq^{\operatorname{fin}}\operatorname{supp}^{\partial T}_{n}(t)$ and $\operatorname{ht}^{\partial T}_{n}(s)<\operatorname{ht}^{\partial T}_{n}(t)$. Let us first consider terms $s=\mu_{m}$ and $t=\xi\langle b,\tau\rangle$. In this case we need neither the induction hypothesis nor the assumption about heights: In view of Definition 4.8 we have $\{m\}\leq^{\operatorname{fin}}\operatorname{supp}^{\partial T}_{n}(t)$, so that $\operatorname{supp}^{\partial T}_{n}(t)<^{\operatorname{fin}}m$ must fail. Invoking Definition 2.10 in conjunction with Proposition 4.9 we obtain

[TABLE]

Since $s$ and $t$ are different terms we can conclude $s<_{\partial T_{n}}t$. Now consider $s=\xi\langle a,\sigma\rangle$ and $t=\mu_{k}$. Definition 4.3 tells us that $s<_{\partial T_{n}}t$ is equivalent to $a<^{\operatorname{fin}}_{\partial T_{n}}t$. The latter is trivial if $a$ is empty. Otherwise we consider the maximal element $s^{\prime}\in a$. In view of Definition 4.8 we get $\operatorname{supp}^{\partial T}_{n}(s^{\prime})\leq^{\operatorname{fin}}\operatorname{supp}^{\partial T}_{n}(t)$. Clearly we also have $\operatorname{ht}^{\partial T}_{n}(s^{\prime})<\operatorname{ht}^{\partial T}_{n}(t)$ and $L^{\partial T}_{n}(s^{\prime})<L^{\partial T}_{n}(s)$. Thus we obtain $s^{\prime}<_{\partial T_{n}}t$ by induction hypothesis. Since $s^{\prime}\in a$ is maximal this establishes $a<^{\operatorname{fin}}_{\partial T_{n}}t$, as needed. Finally we consider $s=\xi\langle a,\sigma\rangle$ and $t=\xi\langle b,\tau\rangle$. In the proof of Lemma 4.5 we have seen that $s<_{\partial T_{n}}t$ holds if $b\leq^{\operatorname{fin}}_{\partial T_{n}}a$ fails. In order to refute $b\leq^{\operatorname{fin}}_{\partial T_{n}}a$ we observe that $\operatorname{ht}^{\partial T}_{n}(s)<\operatorname{ht}^{\partial T}_{n}(t)$ implies $b\neq\emptyset$. Let $t^{\prime}\in b$ be maximal with respect to $<_{\partial T_{n}}$. To complete the proof it suffices to establish $a<^{\operatorname{fin}}_{\partial T_{n}}t^{\prime}$. Yet again this is trivial if $a$ is empty. Otherwise the claim reduces to $s^{\prime}<_{\partial T_{n}}t^{\prime}$, where $s^{\prime}\in a$ is maximal. The maximality of $t^{\prime}$ and Lemma 4.4 ensure that $\operatorname{supp}^{\partial T}_{n}(r)\leq^{\operatorname{fin}}\operatorname{supp}^{\partial T}_{n}(t^{\prime})$ holds for all $r\in b$. In view of Definition 4.8 this yields

[TABLE]

As we also have $\operatorname{ht}^{\partial T}_{n}(s^{\prime})<\operatorname{ht}^{\partial T}_{n}(t^{\prime})$, the induction hypothesis yields $s^{\prime}<_{\partial T_{n}}t^{\prime}$. ∎

For our approximations of $\partial T^{x}_{X}$ we get the following:

Proposition 5.6** ($\mathbf{RCA}_{0}$).**

Consider a normal prae-dilator $T$, an order $X$ and an element $x\in X$. For any number $k$ the order $\partial T^{x,k}_{X}$ is an initial segment of $\partial T^{x}_{X}$.

Proof.

Given $\langle a,s\rangle\in\partial T^{x,k}_{X}$ and $\langle b,t\rangle\in\partial T^{x}_{X}$, we must show that $\langle b,t\rangle\leq_{D^{\partial T}_{X}}\langle a,s\rangle$ implies $\langle b,t\rangle\in\partial T^{x,k}_{X}$. If we have $\langle a,s\rangle\in\partial T^{y}_{X}$ for some $y<_{X}x$, then we can conclude by Lemma 5.2. So we may assume $\operatorname{ht}^{\partial T}_{|a|}(s)\leq k$. Aiming at the contrapositive of the desired implication, let us assume that $\langle b,t\rangle\in\partial T^{x,k}_{X}$ fails. Then we have $\operatorname{ht}^{\partial T}_{|b|}(t)>k$, and $b<^{\operatorname{fin}}_{X}y$ must fail for all $y<_{X}x$. In view of $a<^{\operatorname{fin}}_{X}x$ we get

[TABLE]

To complete the proof of the contrapositive we must show $\langle a,s\rangle<_{D^{\partial T}_{X}}\langle b,t\rangle$. In view of Definition 2.4 this amounts to

[TABLE]

In order to show this inequality it suffices to establish the assumptions of Lemma 5.5, which we shall do in the rest of the proof. Recall that $\operatorname{supp}^{\partial T}$ is natural, that we have $\operatorname{en}_{a\cup b}\circ|\iota_{a}^{a\cup b}|=\iota_{a}^{a\cup b}\circ\operatorname{en}_{a}$ (see the beginning of Section 2), and that $\langle a,s\rangle\in D^{\partial T}_{X}$ requires $\operatorname{supp}^{\partial T}_{|a|}(s)=|a|$ (see Definition 2.4). Combining these facts we obtain

[TABLE]

In the same way one can establish

[TABLE]

Above we have shown $a\leq^{\operatorname{fin}}_{X}b$. Since $\operatorname{en}_{a\cup b}$ is order preserving we can now conclude

[TABLE]

which is the first of the assumptions needed for Lemma 5.5. Above we have also seen $\operatorname{ht}^{\partial T}_{|a|}(s)<\operatorname{ht}^{\partial T}_{|b|}(t)$. Together with Lemma 5.4 we now get

[TABLE]

This establishes the second assumption of Lemma 5.5 and completes the proof. ∎

The crucial induction step relies on the assumption that $T$ is a dilator:

Proposition 5.7** ($\mathbf{RCA}_{0}$).**

Consider a normal dilator $T$, a linear order $X$, an element $x\in X$, and a number $k$. If $\partial T^{x,k}_{X}$ is well-founded, then so is $\partial T^{x,k+1}_{X}$.

Proof.

Assume that $\partial T^{x,k}_{X}$ is a well-order. As $T$ is a dilator it follows that $D^{T}(\partial T^{x,k}_{X})$ is a well-order as well. In order to conclude that $\partial T^{x,k+1}_{X}$ is well-founded it suffices to show that this order can be embedded into $D^{T}(\partial T^{x,k}_{X})$. First observe that

[TABLE]

is a suborder of $D^{T}(D^{\partial T}_{X})$ (apply Lemma 2.8 to the inclusion map $\partial T^{x,k}_{X}\hookrightarrow D^{\partial T}_{X}$). Also recall that $\partial T$ comes with a natural transformation $\xi^{T}:T\circ\partial T\Rightarrow\partial T$, which is an isomorphism by the proof of Theorem 4.13. In view of Definition 2.20 and Proposition 2.16 we obtain an isomorphism

[TABLE]

It suffices to show that $\partial T^{x,k+1}_{X}$ is contained in the image of $D^{T}(\partial T^{x,k}_{X})$ under this isomorphism, which is equivalent to the assertion that

[TABLE]

holds for any element $\sigma\in D^{T}(D^{\partial T}_{X})$. To establish this fact we write

[TABLE]

such that the pairs $\langle a_{j},s_{j}\rangle$ are displayed in increasing order. If we have $n=0$, then $\sigma\in D^{T}(\partial T^{x,k}_{X})$ is immediate. Thus we assume $n>0$ for the rest of the proof. Under this assumption, Proposition 5.6 and Lemma 5.2 imply that $\sigma\in D^{T}(\partial T^{x,k}_{X})$ is equivalent to $\langle a_{n},s_{n}\rangle\in\partial T^{x,k}_{X}$. By Proposition 2.16 and Definition 2.20 we have

[TABLE]

where $\iota_{j}:a_{j}\hookrightarrow a_{1}\cup\dots\cup a_{n}=:c$ are the inclusions. In view of $a_{n}\subseteq c$ we learn that $D^{\xi^{T}}_{X}\circ\zeta^{T,\partial T}_{X}(\sigma)\in\partial T^{y}_{X}$ implies $\langle a_{n},s_{n}\rangle\in\partial T^{y}_{X}$, for any $y\in X$. To complete the proof it suffices to establish the implication

[TABLE]

In view of Definition 4.10 we distinguish two cases: First assume that we have

[TABLE]

Invoking Definition 2.4 we see that the map $\langle a_{j},s_{j}\rangle\mapsto\partial T_{|\iota_{j}|}(s_{j})$ is order preserving. Thus the values $\partial T_{|\iota_{j}|}(s_{j})$ are displayed in increasing order as well. By Lemma 5.4 and our definition of heights we get

[TABLE]

which yields the desired implication. Now assume that we have

[TABLE]

for some $m<|c|$. This can only happen if we have $\partial T_{|\iota_{n}|}(s_{n})=\mu_{m}$. We then get

[TABLE]

which is the conclusion of the desired implication. ∎

To deduce the main result of this section we extend the base theory by the principle of bar induction for $\Pi^{1}_{1}$-formulas (abbreviated $\mathbf{\Pi^{1}_{1}}\textbf{-BI}$).

Theorem 5.8** ($\mathbf{RCA}_{0}+\mathbf{\Pi^{1}_{1}}\textbf{-BI}$).**

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

Proof.

From Proposition 4.9 we know that $\partial T$ is a normal prae-dilator. In view of Definition 2.7 it remains to establish that $D^{\partial T}_{X}$ is well-founded for any well-order $X$. It suffices to consider the case where $X$ is a limit order, i. e. a non-empty order without a maximal element: If $X$ itself does not have this property, then we replace it by the order $X+\omega$, in which the initial segment $X$ is followed by a copy of the natural numbers. By Proposition 2.5 the inclusion $X\hookrightarrow X+\omega$ yields an embedding of $D^{\partial T}_{X}$ into $D^{\partial T}_{X+\omega}$, so that the former order is well-founded if the latter is. For the rest of this proof we assume that $X$ is a well-founded limit order. In view of Definition 5.1 we then have

[TABLE]

Let us argue that $D^{\partial T}_{X}$ is well-founded if $\partial T_{X}^{x}$ is well-founded for every $x\in X$: To find a minimal element of a non-empty set $Y\subseteq D^{\partial T}_{X}$, pick an element $x\in X$ such that $Y\cap\partial T_{X}^{x}$ is non-empty. The well-foundedness of $\partial T_{X}^{x}$ provides a minimal element $\sigma\in Y\cap\partial T_{X}^{x}$. From Lemma 5.2 we know that $\partial T_{X}^{x}$ is an initial segment of $D^{\partial T}_{X}$. It follows that $\sigma$ is minimal in the entire set $Y$, as required. Invoking the principle of $\Pi^{1}_{1}$-bar induction, we shall now establish the well-foundedness of $\partial T_{X}^{x}$ by induction on $x\in X$. In the induction step we argue that Definition 5.3 and Proposition 5.6 allow us to write

[TABLE]

as a union of initial segments. Once again it follows that $\partial T^{x}_{X}$ is well-founded if $\partial T^{x,k}_{X}$ is well-founded for every number $k$. We argue by side induction on $k$ to show that the latter is the case. Note that induction over the natural numbers is available as a particular instance of bar induction (alternatively one could combine the main and side induction into a single induction over $X\times\omega$). The side induction step is provided by Proposition 5.7. To complete the proof it is thus enough to establish the base of the side induction. As a preparation we consider an element $\langle a,s\rangle\in\partial T_{X}^{x}$ with $\operatorname{ht}^{\partial T}_{|a|}(s)=0$. In view of Definition 5.3 we must have $s=\mu_{m}$ for some number $m<|a|$. Together with Definitions 2.4 and 4.8 we obtain

[TABLE]

This forces $m=0$ and $|a|=1$, say $a=\{z\}$ with $z\in X$. Altogether we get

[TABLE]

where $\langle a,s\rangle\in\partial T_{X}^{x}$ ensures $z<_{X}x$. Let us now distinguish two cases: First assume that $x\in X$ is a limit or zero (i. e. for every $z<_{X}x$ there is a $y<_{X}x$ with $z<_{X}y$). Then Definition 5.3 yields

[TABLE]

By Lemma 5.2 this is a union of initial segments. The main induction hypothesis ensures that $\partial T^{y}_{X}$ is well-founded for every $y<_{X}x$. It follows that $\partial T^{x,0}_{X}$ is well-founded, as required. Now assume that $x$ is the successor of an element $z\in X$, so that $y<_{X}x$ is equivalent to $y\leq_{X}z$. In view of the above we obtain

[TABLE]

Once again the main induction hypothesis tells us that $\partial T^{z}_{X}$ is well-founded. Since $\partial T^{x,0}_{X}$ is a finite extension of this order, it must be well-founded itself. We have thus established the base of the side induction, which completes the proof. ∎

To shed further light on the previous proof we point out that we have

[TABLE]

due to Definitions 2.12 and 4.8 as well as Lemma 5.2. Together with the conclusions of the previous sections we obtain the main result of this paper:

Theorem 5.9** ($\mathbf{ACA}_{0}$).**

The following are equivalent:

1. (1)

If $T$ is a normal dilator, then $D^{\partial T}_{X}$ is well-founded for any well-order $X$. 2. (2)

Any normal dilator $T$ has an upper derivative $(S,\xi)$ such that $X\mapsto D^{S}_{X}$ preserves well-foundedness (which means that $S$ is again a normal dilator). 3. (3)

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

Note that statements (1) and (2) are each expressed by a single formula, relying on the formalization of dilators in Section 2. To express (3) by a single formula one uses a truth definition for $\Pi^{1}_{1}$-sentences.

Proof.

The implication (1)$\Rightarrow$(2) follows from Proposition 4.11, which asserts that $(\partial T,\xi^{T})$ is an upper derivative of $T$ (in fact we have a derivative, by Theorem 4.12). By Corollary 3.13 we get (2)$\Rightarrow$(3) (note that the proof uses arithmetical comprehension, via the Kleene normal form theorem and the characteristic property of the Kleene-Brouwer order). The implication (3)$\Rightarrow$(1) holds by Theorem 5.8. ∎

As in the previous section, results about $\partial T$ transfer to arbitrary derivatives:

Corollary 5.10** ($\mathbf{RCA}_{0}+\mathbf{\Pi^{1}_{1}}\textbf{-BI}$).**

Consider a normal dilator $T$. If $(S,\xi)$ is a derivative of $T$, then $X\mapsto D^{S}_{X}$ preserves well-foundedness.

Proof.

By Definition 2.28 and Proposition 4.11 there is a morphism $\nu:S\Rightarrow\partial T$ of upper derivatives. According to Lemma 2.21 we get an embedding

[TABLE]

for each linear order $X$. Together with Theorem 5.8 it follows that $D^{S}_{X}$ is well-founded whenever $X$ is a well-order. ∎

Working in a sufficiently strong set theory, one can deduce the following unconditional version of Theorem 2.29. This result provides further justification for our categorical definition of derivatives:

Corollary 5.11**.**

Let $T$ be a normal dilator. If $(S,\xi)$ is a derivative of $T$, then the function $\alpha\mapsto\operatorname{otp}(D^{S}_{\alpha})$ is the derivative of the normal function $\alpha\mapsto\operatorname{otp}(D^{T}_{\alpha})$.

Proof.

According to Theorem 4.13 and Corollary 5.10 the assumptions of Theorem 2.29 are satisfied whenever $(S,\xi)$ is a derivative of $T$. ∎