Predicative collapsing principles

TL;DR

This paper explores the equivalence between arithmetical transfinite recursion and a formal collapsing principle involving ordinal arithmetic, providing new characterizations of these foundational logical systems.

Contribution

It introduces a novel formal collapsing principle that characterizes arithmetical transfinite recursion and comprehension within ordinal arithmetic frameworks.

Findings

Equivalence of arithmetical transfinite recursion with a formal collapsing principle.

Characterization of arithmetical comprehension via a similar ordinal collapse.

Description of principles ensuring sets are in countable models of these systems.

Abstract

We show that arithmetical transfinite recursion is equivalent to a suitable formalization of the following: For every ordinal $\alpha$ there exists an ordinal $\beta$ such that $1+\beta\cdot(\beta+\alpha)$ (ordinal arithmetic) admits an almost order preserving collapse into $\beta$. Arithmetical comprehension is equivalent to a statement of the same form, with $\beta\cdot\alpha$ at the place of $\beta\cdot(\beta+\alpha)$. We will also characterize the principles that any set is contained in a countable coded $\omega$-model of arithmetical transfinite recursion resp. arithmetical comprehension.

Tables

arithmetical comprehension	$X\mapsto {\omega }^X$	[12, 13]
the $\omega$-jump of every set exists	$X\mapsto {\epsilon }_X$	[14, 3]
arithmetical transfinite recursion	$X\mapsto \phi \left(1+X\right)0$	[18]
every set lies in an $\omega$-model of $\mathrm{𝐀𝐓𝐑}$	$X\mapsto {\Gamma }_X$	[15]

${\omega }^{{\omega }^X}$	$Y\mapsto T_X^{\omega }\left(Y\right):=1+\left(1+X\right)\times Y$	Theorem 2.2
${\epsilon }_X$	$Y\mapsto T_X^{\epsilon }\left(Y\right):=1+Y^2+X$	Theorem 2.6
$\phi \left(1+X\right)0$	$Y\mapsto T_X^{\phi }\left(Y\right):=1+\left(Y+X\right)\times Y$	Theorem 1.4
${\Gamma }_X$	$Y\mapsto T_X^{\Gamma }\left(Y\right):=1+2\times Y^2+X$	Theorem 3.5

Equations

$$Y\mapsto T_X^{\phi }(Y):=1+(Y+X)\times Y,$$

$$X+Y=\{⟨0,x⟩|x\in X\}\cup \{⟨1,y⟩|y\in Y\}.$$

$$X\times Y=\{⟨x,y⟩|x\in X\text{ and }y\in Y\},$$

$$\vartheta :T_X^{\phi }(Y)\to Y.$$

$${\mathrm{supp}}_Y^T(\sigma )=\bigcap \{Y_0\subseteq Y|\sigma \in T(Y_0)\}.$$

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

$$({\omega }^{x_0}+\cdots +{\omega }^{x_n})+({\omega }^{y_0}+\cdots +{\omega }^{y_m})={\omega }^{x_0}+\cdots +{\omega }^{x_i}+{\omega }^{y_0}+\cdots +{\omega }^{y_m},$$

$${\omega }^{\alpha }\cdot ({\omega }^{{\beta }_0}+\cdots +{\omega }^{{\beta }_{n-1}})={\omega }^{\alpha +{\beta }_0}+\cdots +{\omega }^{\alpha +{\beta }_{n-1}},$$

$$l_X^{\omega }({\omega }^{x_0}+\cdots +{\omega }^{x_{n-1}})$$

$$L_X^{\omega }({\omega }^{{\alpha }_0}+\cdots +{\omega }^{{\alpha }_{n-1}})$$

$${\omega }^{{\beta }_0}+\cdots +{\omega }^{{\beta }_n}\in {\omega }_2(X).$$

$${\beta }_n={\omega }^x+{\gamma }_n>{\gamma }_n.$$

$${\beta }_i={\omega }^x+{\gamma }_i$$

$$\eta :={\omega }^{{\gamma }_0}+\cdots +{\omega }^{{\gamma }_n}\in {\omega }_2(X).$$

$${\omega }_2(x)\cdot \eta ={\omega }^{{\omega }^x+{\gamma }_0}+\cdots +{\omega }^{{\omega }^x+{\gamma }_n}={\omega }^{{\beta }_0}+\cdots +{\omega }^{{\beta }_n}.$$

$$0{<}_{{\omega }_2(X)}\eta {<}_{{\omega }_2(X)}{\omega }^{{\beta }_0}+\cdots +{\omega }^{{\beta }_n}={\omega }_2(x)\cdot \eta .$$

$$L_X^{\omega }(\eta )=l_X^{\omega }({\gamma }_0)+\cdots +l_X^{\omega }({\gamma }_n)+n+1<l_X^{\omega }({\beta }_0)+\cdots +l_X^{\omega }({\beta }_n)+n+1=L_X^{\omega }({\omega }_2(x)\cdot \eta ).$$

$$\eta {<}_{{\omega }_2(X)}{\omega }_2(x)\cdot \eta ={\omega }_2(y)\cdot \xi {>}_{{\omega }_2(X)}\xi$$

$${\omega }_2(x)\cdot \eta ={\omega }_2(y)\cdot \xi ={\omega }_2(x)\cdot {\omega }_2(y)\cdot \xi ={\omega }_2(x)\cdot {\omega }_2(x)\cdot \eta ,$$

$$Y\mapsto T_X^{\omega }(Y)=1+(1+X)\times Y.$$

$${\mathrm{supp}}_Y^{\omega }(\perp )=\varnothing \text{and}{\mathrm{supp}}_Y^{\omega }(⟨x,y⟩)=\{y\}.$$

$$\vartheta :1+(1+X)\times {\omega }_2(X)\to {\omega }_2(X).$$

$$\vartheta (\perp )$$

$$\vartheta (⟨\perp ,\eta ⟩)$$

$$\vartheta (⟨1+x,\eta ⟩)$$

$$\eta {<}_{{\omega }_2(X)}\eta +1{\le }_{{\omega }_2(X)}{\omega }_2(x)\cdot (\eta +1).$$

$$⟨\perp ,\eta ⟩{<}_{(1+X)\times Y}⟨1+x,{\eta }^{\prime }⟩.$$

$$\eta {<}_{{\omega }_2(X)}\vartheta (⟨1+x,{\eta }^{\prime }⟩)={\omega }_2(x)\cdot ({\eta }^{\prime }+1).$$

$$\vartheta (⟨\perp ,\eta ⟩)=\eta +1{<}_{{\omega }_2(X)}\vartheta (⟨1+x,{\eta }^{\prime }⟩),$$

$$⟨1+x,\eta ⟩{<}_{(1+X)\times Y}⟨1+x^{\prime },{\eta }^{\prime }⟩$$

$$\vartheta (⟨1+x,\eta ⟩)={\omega }_2(x)\cdot (\eta +1){<}_{{\omega }_2(X)}{\omega }_2(x)\cdot {\omega }_2(x^{\prime })\cdot ({\eta }^{\prime }+1)$$

$$={\omega }_2(x^{\prime })\cdot ({\eta }^{\prime }+1)$$

Full text

††footnotetext: © 2020 Association for Symbolic Logic. This is the accepted version of a paper published in The Journal of Symbolic Logic 85(1) 2020, pp. 511-530, doi:10.1016/j.aim.2019.106767.

1. Introduction

Well-ordering principles (of type one) are statements which assert that “$T(X)$ is well-founded for any well-order $X$”, for some transformation $T$ of linear orders. We will consider such statements from the viewpoint of reverse mathematics (see [20] for a comprehensive introduction). In this setting $X$ ranges over ordered subsets of $\mathbb{N}$. The fact that $T$ is a transformation of linear orders can usually be proved in $\mathbf{RCA}_{0}$, so that the entire strength of the well-ordering principle lies in the preservation of well-foundedness.

The literature contains many results that characterize important $\Pi^{1}_{2}$-statements in terms of well-ordering principles. In order to explain our approach we focus on the following equivalence (but further results will be covered below):

Theorem 1.1** (H. Friedman [unpublished]; M. Rathjen and A. Weiermann [18]).**

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

1. (i)

arithmetical transfinite recursion (i. e. the principal axiom of $\mathbf{ATR}_{0}$), 2. (ii)

the statement that $\varphi(1+X)0$ is well-founded for any well-order $X$.

The transformation in (ii) is related to the Veblen function, which iterates derivatives of normal functions into the transfinite (cf. [19, 14]). In the context of reverse mathematics, the relevant values of this function can be represented by relativized ordinal notation systems $\varphi(1+X)0$ (see [18, Definition 2.2] for details; our summand $1$ corresponds to the minimal element $0_{Q}$ in the cited definition).

The present paper shows that complicated well-ordering principles can, in a certain sense, be reduced to much simpler ones. In particular we will reduce the well-ordering principle $X\mapsto\varphi(1+X)0$ to the family of order transformations

[TABLE]

indexed by the order $X$ (unless stated otherwise, “order” will always mean “linear order”). Here $1$ denotes the order with a single element. Also recall that the sum of two orders $X=(X,<_{X})$ and $Y=(Y,<_{Y})$ has underlying set

[TABLE]

For $x<_{X}x^{\prime}$ and $y<_{Y}y^{\prime}$ we have $\langle 0,x\rangle<_{X+Y}\langle 0,x^{\prime}\rangle$ resp. $\langle 1,y\rangle<_{X+Y}\langle 1,y^{\prime}\rangle$, and $\langle 0,x\rangle<_{X+Y}\langle 1,y\rangle$ holds for any $x\in X$ and $y\in Y$. The product is given by

[TABLE]

where $\langle x,y\rangle<_{X\times Y}\langle x^{\prime},y^{\prime}\rangle$ holds if we have $x<_{X}x^{\prime}$, or $x=x^{\prime}$ and $y<_{Y}y^{\prime}$. Clearly the definition of sum and product is much simpler than the construction of $\varphi(1+X)0$ in [18, Definition 2.2]. The fact that sums and products of well-orders are themselves well-ordered can be proved in $\mathbf{RCA}_{0}$, in contrast to Theorem 1.1.

So how can $X\mapsto\varphi(1+X)0$ be reduced to the transformations $T^{\varphi}_{X}$? The idea is to consider fixed points of a certain type. Let us first observe that $T^{\varphi}_{X}(Y)\cong Y$ cannot hold for any well-orders $X$ and $Y$: If the latter have order types $\alpha$ resp. $\beta$, then $T^{\varphi}_{X}(Y)$ has order type $1+\beta\cdot(\beta+\alpha)>\beta$. The best we can hope for is an “almost” order preserving function

[TABLE]

To make this precise we need some terminology: A transformation $Y\mapsto T(Y)$ of linear orders is called inclusive if $T(Y_{0})$ is a suborder of $T(Y)$ whenever $Y_{0}$ is a suborder of $Y$. This property allows us to introduce the following notion:

Definition 1.2**.**

Let $Y\mapsto T(Y)$ be an inclusive transformation of orders. Given any order $Y$, we define the support $\operatorname{supp}^{T}_{Y}(\sigma)\subseteq Y$ of an element $\sigma\in T(Y)$ by

[TABLE]

For the above transformations $T^{\varphi}_{X}$, the supports have a concrete description: The element of the summand $1$ has empty support. The support of an element $\langle\langle 0,y\rangle,y^{\prime}\rangle$ resp. $\langle\langle 1,x\rangle,y^{\prime}\rangle$ in the other summand is equal to $\{y,y^{\prime}\}$ resp. $\{y^{\prime}\}$. We can now say what we mean by an “almost” order preserving function:

Definition 1.3**.**

Consider an inclusive transformation $Y\mapsto T(Y)$ of linear orders. A function $\vartheta:T(Y)\rightarrow Y$ is called a Bachmann-Howard collapse if the following holds for all $\sigma,\tau\in T(Y)$:

1. (i)

$\sigma<_{T(Y)}\tau$ implies $\vartheta(\sigma)<_{Y}\vartheta(\tau)$, under the side condition that $y<_{Y}\vartheta(\tau)$ holds for all $y\in\operatorname{supp}^{T}_{Y}(\sigma)$, 2. (ii)

we have $y<_{Y}\vartheta(\sigma)$ for all $y\in\operatorname{supp}^{T}_{Y}(\sigma)$.

An order $Y$ that admits such a function is called a Bachmann-Howard fixed point of $T$. If $Y$ can be embedded into any other Bachmann-Howard fixed point of $T$, then it is called a minimal Bachmann-Howard fixed point.

In Remark 2.4 we will discuss a stronger notion of minimality, which may be more appealing from a categorical standpoint. We can now state our characterization of the transformation $X\mapsto\varphi(1+X)0$, which will be proved in Section 3.

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

The order $\varphi(1+X)0$ is a minimal Bachmann-Howard fixed point of the transformation $Y\mapsto 1+(Y+X)\times Y$, for any linear order $X$.

Due to minimality, a descending sequence in $\varphi(1+X)0$ propagates to any Bachmann-Howard fixed point of $T^{\varphi}_{X}$. Hence $\varphi(1+X)0$ is well-founded if, and only if, the transformation $T^{\varphi}_{X}$ has a well-founded Bachmann-Howard fixed point. Together with Theorem 1.1 we obtain the following:

Corollary 1.5**.**

The following principles are equivalent over $\mathbf{RCA}_{0}$:

1. (i)

arithmetical transfinite recursion, 2. (ii)

for every well-order $X$ the transformation $Y\mapsto 1+(Y+X)\times Y$ has a well-founded Bachmann-Howard fixed point.

As mentioned above, the literature contains several results that have the same form as Theorem 1.1. In each line of the following table, the principle in the left column is equivalent to the assertion that the transformation in the middle column preserves well-foundedness (so the third line is Theorem 1.1). Precise definitions and proofs can be found in the references that are given in the right column.

Note that the existence of $\omega$-jumps is equivalent to the statement that every set lies in a (countable coded) $\omega$-model of $\mathbf{ACA}$, over the base theory $\mathbf{ACA}_{0}$ (see [3, Lemma 3.4]; $\omega$-models are explained in [20, Section 7.2]). We will characterize all transformations from the previous table in terms of collapsing principles. In each line of the next table, the order in the left column is a minimal Bachmann-Howard fixed point of the transformation in the middle column, for any linear order $X$. The right column refers to the corresponding theorem of the present paper.

As in Corollary 1.5, we obtain new characterizations of the (broadly) predicative principles from above: arithmetical comprehension (Corollary 2.3), the existence of $\omega$-jumps (Corollary 2.7), and the existence of $\omega$-models of $\mathbf{ATR}$ (Corollary 3.6).

In the rest of this introduction we explain the wider context of our results: Let us first recall that J.-Y. Girard [11] has singled out a class of particularly uniform well-ordering principles, which are known as dilators. More precisely, a dilator is an endofunctor on the category of well-orders that preserves direct limits and pullbacks. In the inclusive case, these requirements correspond to the following properties of the supports from Definition 1.2 (cf. [5, Remark 2.2.2]):

• •

each support $\operatorname{supp}^{T}_{Y}(\sigma)\subseteq Y$ is finite,

• •

we have $\sigma\in T(\operatorname{supp}^{T}_{Y}(\sigma))$ for any $\sigma\in T(Y)$.

Girard has shown that dilators are determined by their restrictions to the category of natural numbers (up to natural equivalence). This crucial property makes it possible to represent dilators in second order arithmetic. For the purpose of the present paper we do not need this general representation, since our families of order transformations come with an explicit parametrization.

The notion of Bachmann-Howard fixed point has been introduced in [5, 6], for arbitrary (i. e. not necessarily inclusive) dilators. In the cited papers it was shown that $\Pi^{1}_{1}$-comprehension is equivalent to the statement that every dilator has a well-founded Bachmann-Howard fixed point. Furthermore, a minimal Bachmann-Howard fixed point of a given dilator can already be constructed in $\mathbf{RCA}_{0}$, as shown in [7, 8]. Due to its minimality, that fixed point must be well-founded, but $\mathbf{RCA}_{0}$ cannot prove this fact. Applied to Corollary 1.5, this confirms that the strength of statement (ii) does not lie in the existence of a Bachmann-Howard fixed point as such, but rather in its well-foundedness.

The name “Bachmann-Howard fixed point” refers to the fact that our definitions are inspired by the Bachmann-Howard ordinal, in particular by the notation system from [17, Section 1]. It is well-known that values of the Veblen function also arise in the construction of the Bachmann-Howard ordinal (see e. g. [4]). For this reason a result such as Theorem 1.4 may not be entirely unexpected. Nevertheless, it seems that the connection on the level of predicative well-ordering principles has not been made before. The literature does contain an impredicative well-ordering principle that is related to the Bachmann-Howard ordinal: As shown by M. Rathjen and P. Valencia Vizcaíno [16], the statement that every set lies in an $\omega$-model of bar induction is equivalent to the principle that a relativized notation system $\vartheta_{X}$ is well-founded for any well-order $X$. In contrast to our approach, the notation system $\vartheta_{X}$ incorporates the collapsing function into the term structure.

In the present paper we are concerned with “almost” order preserving collapsing functions of transformations that do not have well-founded fixed points in the usual sense. A class of transformations that correspond to normal functions has been singled out by P. Aczel [1, 2]: these transformations have well-founded fixed points of arbitrarily large order type. In [10, 9] it was shown that an appropriate formalization of the statement that “every normal function has a derivative (resp. at least one fixed point)” is equivalent to $\Pi^{1}_{1}$-induction along arbitrary well-orders (resp. along $\mathbb{N}$). These induction principles are considerably weaker than the principle of $\Pi^{1}_{1}$-comprehension, which is equivalent to the existence of well-founded Bachmann-Howard fixed points. The present paper appears to show that the great strength of Bachmann-Howard fixed points translates into particularly simple characterizations of weaker principles.

2. Collapsing and ordinal exponentiation

In the present section we show how the orders $\omega^{\omega^{X}}$ and $\varepsilon_{X}$ can be constructed as Bachmann-Howard fixed points. As mentioned in the introduction, this yields characterizations of arithmetical comprehension and the principle that the $\omega$-jump of every set exists.

Let us recall some definitions: Given an order $X=(X,\leq_{X})$, the underlying set

[TABLE]

of the order $\omega^{X}=(\omega^{X},\leq_{\omega^{X}})$ consists of the finite decreasing sequences with entries from $X$. The relation $\leq_{\omega^{X}}$ is defined as the lexicographic order on this set (cf. [13, Definition 2.2]). Intuitively, the elements of $\omega^{X}$ correspond to Cantor normal forms. To convey this intuition we will write $\omega^{x_{0}}+\dots+\omega^{x_{n-1}}$ rather than $\langle x_{0},\dots,x_{n-1}\rangle$, and in particular [math] rather than $\langle\rangle\in\omega^{X}$. If $X$ is a well-order of type $\alpha$, then $\omega^{X}$ has order type $\omega^{\alpha}$, in the usual sense of ordinal arithmetic.

Addition on $\omega^{X}$ can be defined in terms of Cantor normal forms: We agree that [math] is neutral and that we have

[TABLE]

where $i$ is maximal with $y_{0}\leq_{X}x_{i}$ (note $i=-1$ if $x_{0}<_{X}y_{0}$). It is well-known that basic properties of ordinal addition can be proved in $\mathbf{RCA}_{0}$ (cf. e. g. [19, 21]).

In order to define multiplication we must consider $\omega^{\omega^{X}}$ rather than $\omega^{X}$ (note that an ordinal of the form $\omega^{\alpha}$ does not need to be multiplicatively principal). The general definition of multiplication in terms of Cantor normal forms is somewhat cumbersome, since ordinal arithmetic does not validate right distributivity. Luckily, we will only need to multiply terms of a particular form: Given elements $\alpha\in\omega^{X}$ and $\beta_{n-1}\leq_{\omega^{X}}\dots\leq_{\omega^{X}}\beta_{0}$, we can set

[TABLE]

where the exponents are added in $\omega^{X}$. Since $\omega^{X}$ contains a minimal element $0=\langle\rangle$, the order $\omega^{\omega^{X}}$ contains a minimal non-zero element $1=\omega^{0}$. This allows us to distinguish between successor and limit elements. Again, basic properties of these notions can be proved in $\mathbf{RCA}_{0}$. To avoid iterated superscripts we will abbreviate $\omega_{2}(X):=\omega^{\omega^{X}}$, as well as $\omega_{2}(x)=:\omega^{\omega^{x}}\in\omega_{2}(X)$ for $x\in X$.

On an intuitive level one would like to prove certain statements by induction along the order $\leq_{\omega_{2}(X)}$, but this induction principle is not available in our setting. Instead we argue by induction over the length of terms. For this purpose we define functions $l^{\omega}_{X}:\omega^{X}\rightarrow\mathbb{N}$ and $L^{\omega}_{X}:\omega_{2}(X)\rightarrow\mathbb{N}$ by setting

[TABLE]

The following observation will be crucial for our analysis of the order $\omega_{2}(X)$.

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

Let $X$ be a linear order. Any limit element of $\omega_{2}(X)$ can be uniquely written as $\omega_{2}(x)\cdot\eta$ with $0<_{\omega_{2}(X)}\eta<_{\omega_{2}(X)}\omega_{2}(x)\cdot\eta$. Furthermore we have $L^{\omega}_{X}(\eta)<L^{\omega}_{X}(\omega_{2}(x)\cdot\eta)$ for any such decomposition.

Proof.

To establish existence we consider an arbitrary limit element

[TABLE]

Since we are concerned with a limit, the last exponent is different from $0\in\omega^{X}$. Hence there are elements $x\in X$ and $\gamma_{n}\in\omega^{X}$ with

[TABLE]

Let us also record $l^{\omega}_{X}(\gamma_{n})<l^{\omega}_{X}(\beta_{n})$. Left subtraction is readily defined on the level of Cantor normal forms. In view of $\omega^{x}\leq_{\omega^{X}}\beta_{n}\leq_{\omega^{X}}\dots\leq_{\omega^{X}}\beta_{0}$ we can thus write

[TABLE]

for all $i<n$. One readily checks $\gamma_{i}\leq_{\omega^{X}}\beta_{i}$ and $l^{\omega}_{X}(\gamma_{i})\leq l^{\omega}_{X}(\beta_{i})$ (note that the inequalities may not be strict for $i<n$). Due to the monotonicity of addition we must also have $\gamma_{n}\leq_{\omega^{X}}\dots\leq_{\omega^{X}}\gamma_{0}$. We can thus define

[TABLE]

By construction we have

[TABLE]

The above inequalities between $\beta_{i}$ and $\gamma_{i}$ imply

[TABLE]

In view of $l^{\omega}_{X}(\gamma_{n})<l^{\omega}_{X}(\beta_{n})$ we also get

[TABLE]

It remains to establish uniqueness. Due to the monotonicity of multiplication it suffices to show that

[TABLE]

implies $x=y$. Aiming at a contradiction, let us assume that we have $x<_{X}y$. Then we get $\omega^{x}+\omega^{y}=\omega^{y}$ and hence $\omega_{2}(x)\cdot\omega_{2}(y)=\omega_{2}(y)$. We can deduce

[TABLE]

which is incompatible with the assumption $\eta<_{\omega_{2}(X)}\omega_{2}(x)\cdot\eta$. ∎

Our goal is to characterize $\omega_{2}(X)$ as a minimal Bachmann-Howard fixed point of the order transformation

[TABLE]

Let us write $\bot$ for the unique element of $1$. The elements of $T^{\omega}_{X}(Y)$ will be written as $\bot$, $\langle\bot,y\rangle$ and $\langle 1+x,y\rangle$, rather than $\langle 0,\bot\rangle$, $\langle 1,\langle\langle 0,\bot\rangle,y\rangle\rangle$ and $\langle 1,\langle\langle 1,x\rangle,y\rangle\rangle$, respectively. Sometimes we also use $x$ to denote an arbitrary element of $1+X$. The supports from Definition 1.2 take the forms

[TABLE]

In view of Definition 1.3, this means that a function $\vartheta:T^{\omega}_{X}(Y)\rightarrow Y$ is a Bachmann-Howard collapse if, and only if, the following conditions are satisfied:

1. (i)

we have $\vartheta(\bot)<_{Y}\vartheta(\langle x,y\rangle)$ for any $\langle x,y\rangle\in(1+X)\times Y$, 2. (i*′*)

$\langle x,y\rangle<_{(1+X)\times Y}\langle x^{\prime},y^{\prime}\rangle$ implies $\vartheta(\langle x,y\rangle)<_{Y}\vartheta(\langle x^{\prime},y^{\prime}\rangle)$, under the side condition that we have $y<_{Y}\vartheta(\langle x^{\prime},y^{\prime}\rangle)$, 3. (ii)

we have $y<_{Y}\vartheta(\langle x,y\rangle)$ for any $x\in 1+X$ and $y\in Y$.

We can now establish the promised characterization, improving [8, Proposition 3.3]:

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

The order $\omega^{\omega^{X}}$ is a minimal Bachmann-Howard fixed point of the transformation $T^{\omega}_{X}$, for any order $X$.

Proof.

In order to show that $\omega_{2}(X)=\omega^{\omega^{X}}$ is a Bachmann-Howard fixed point of $T^{\omega}_{X}$ we must define a collapsing function

[TABLE]

Using the successor operation and multiplication in $\omega_{2}(X)$, we set

[TABLE]

The above condition (i) is immediate. Condition (ii) is satisfied in view of

[TABLE]

To verify condition (i*′*) one needs to distinguish several cases. In the first interesting case we are concerned with an inequality

[TABLE]

Due to the side condition in (i*′*) we may assume

[TABLE]

The element on the right side is a limit (note that the last exponent in its Cantor normal form is equal to $\omega^{x}\neq 0$). Hence we obtain

[TABLE]

as required. Let us also consider the case of an inequality

[TABLE]

with $x<_{X}x^{\prime}$. Yet again, the side condition yields $\eta+1<_{\omega_{2}(X)}\omega_{2}(x^{\prime})\cdot(\eta^{\prime}+1)$. Also observe that $x<_{X}x^{\prime}$ implies $\omega_{2}(x)\cdot\omega_{2}(x^{\prime})=\omega_{2}(x^{\prime})$, as in the proof of Lemma 2.1. Using the monotonicity of multiplication we can deduce

[TABLE]

So far we have shown that $\omega_{2}(X)$ is a Bachmann-Howard fixed point of $T^{\omega}_{X}$. To establish minimality we consider an arbitrary order $Y$ that admits a Bachmann-Howard collapse

[TABLE]

We need to construct an embedding $f:\omega_{2}(X)\rightarrow Y$. In view of Lemma 2.1 we can define $f$ by recursion over the length of terms, by setting

[TABLE]

To show that $\xi<_{\omega_{2}(X)}\xi^{\prime}$ implies $f(\xi)<_{Y}f(\xi^{\prime})$ we argue by induction on the combined length $L^{\omega}_{X}(\xi)+L^{\omega}_{X}(\xi^{\prime})$ of $\xi$ and $\xi^{\prime}$ (note that this amounts to an induction over a $\Pi^{0}_{1}$-statement, which is available in $\mathbf{RCA}_{0}$). In the first interesting case we consider an inequality

[TABLE]

In view of $\bot<_{1+X}1+x$ we clearly have $\langle\bot,f(\eta)\rangle<_{(1+X)\times Y}\langle 1+x,f(\eta^{\prime})\rangle$. Invoking the induction hypothesis, we also see that $\eta<_{\omega_{2}(X)}\xi^{\prime}$ implies

[TABLE]

This is the side condition required in clause (i*′*) above. We can thus conclude

[TABLE]

Let us now consider an inequality of the form

[TABLE]

Using the induction hypothesis and clause (ii) above we get

[TABLE]

as required. To conclude the proof we consider an inequality of the form

[TABLE]

We need to distinguish three cases: First assume that we have $x<_{X}x^{\prime}$. Then we immediately get $\langle 1+x,f(\eta)\rangle<_{(1+X)\times Y}\langle 1+x^{\prime},f(\eta^{\prime})\rangle$. In view of Lemma 2.1 we have $\eta<_{\omega_{2}(X)}\xi<_{\omega_{2}(X)}\xi^{\prime}$ and $L^{\omega}_{X}(\eta)<L^{\omega}_{X}(\xi)$. Hence the induction hypothesis yields

[TABLE]

Hence the side condition from clause (i*′*) is satisfied, and we obtain

[TABLE]

Now assume $x=x^{\prime}$. In view of $\xi<_{\omega_{2}(X)}\xi^{\prime}$ we must have $\eta<_{\omega_{2}(X)}\eta^{\prime}$. Then the induction hypothesis yields $\langle 1+x,f(\eta)\rangle<_{(1+X)\times Y}\langle 1+x^{\prime},f(\eta^{\prime})\rangle$, and we can conclude as in the previous case. Finally assume $x>_{X}x^{\prime}$. In this case we observe that

[TABLE]

implies $\xi<_{\omega_{2}(X)}\eta^{\prime}$. Using the induction hypothesis and clause (ii) we obtain

[TABLE]

just as needed. ∎

The statement that $\omega^{X}$ is well-founded for every well-order $X$ is equivalent to arithmetical comprehension, as shown by J.-Y. Girard [12, Section 5.4] (cf. also the computability-theoretic proof by J. Hirst [13]). We can deduce the following:

Corollary 2.3**.**

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

1. (i)

arithmetical comprehension (which is the principal axiom of $\mathbf{ACA}_{0}$), 2. (ii)

for every well-order $X$ the transformation $Y\mapsto 1+X\times Y$ has a well-founded Bachmann-Howard fixed point.

Proof.

To deduce (ii) from (i) we consider an arbitrary well-order $X$. In view of Girard’s result, we can invoke (i) to infer that $\omega^{X}$ and $\omega_{2}(X)$ are well-founded. Theorem 2.2 yields a Bachmann-Howard collapse

[TABLE]

The restriction of $\vartheta$ to $1+X\times\omega_{2}(X)$ witnesses that $\omega_{2}(X)$ is a Bachmann-Howard fixed point of $Y\mapsto 1+X\times Y$, as one readily verifies. To show that (ii) implies (i) we again invoke Girard’s result. Hence we must establish that $\omega^{X}$ is well-founded for an arbitrary well-order $X$. Since $1+X$ is still well-founded, we can use (ii) to get a well-founded Bachmann-Howard fixed point $Y$ of the transformation

[TABLE]

From Theorem 2.2 we know that $\omega_{2}(X)$ can be embedded into $Y$. Hence $\omega_{2}(X)$ must be well-founded as well. In view of the embedding

[TABLE]

we can infer that $\omega^{X}$ is well-founded, as required. ∎

To conclude the first half of the present section we discuss a possible improvement of Theorem 2.2:

Remark 2.4**.**

The Bachmann-Howard collapse $\vartheta:T^{\omega}_{X}(\omega_{2}(X))\rightarrow\omega_{2}(X)$ that we have constructed in the proof of Theorem 2.2 does not look quite optimal: For an element $\eta\in\omega_{2}(X)$ with $\eta<_{\omega_{2}(X)}\omega_{2}(x)\cdot\eta$ it might have been more natural to define $\vartheta(\langle 1+x,\eta\rangle)$ as $\omega_{2}(x)\cdot\eta$ rather than $\omega_{2}(x)\cdot(\eta+1)$. To make this intuition precise we can observe the following: In the second half of the proof of Theorem 2.2 we have constructed an embedding $f:\omega_{2}(X)\rightarrow Y$ into an arbitrary Bachmann-Howard fixed point $Y$ of the transformation $T^{\omega}_{X}$. If we construct this embedding with respect to the given Bachmann-Howard collapse for $Y=\omega_{2}(X)$, then we get

[TABLE]

which means that $f$ cannot be the identity on $\omega_{2}(Y)$. In order to understand this phenomenon in general we recall that the notion of Bachmann-Howard fixed point was defined for dilators, i. e. for particularly uniform endofunctors on the category of linear orders. Functoriality allows us to define the following notion: Given Bachmann-Howard fixed points $X$ and $Y$ with fixed collapsing functions $\vartheta_{X}:T(X)\rightarrow X$ and $\vartheta_{Y}:T(Y)\rightarrow Y$, we say that $f:X\rightarrow Y$ is a morphism of Bachmann-Howard fixed points if we have

[TABLE]

Following the usual categorical terminology, an initial Bachmann-Howard fixed point consists of an order $X$ and a Bachmann-Howard collapse $\vartheta:T(X)\rightarrow X$ that admit a unique morphism into any Bachmann-Howard fixed point of the same dilator. The proofs of [7, Theorem 3.4] and [8, Theorem 4.5] reveal that every dilator has an initial Bachmann-Howard fixed point, which is necessarily unique up to isomorphism. Note that any initial fixed point is minimal in the sense of Definition 1.3. The notion of initial fixed point is certainly more satisfactory from a theoretical perspective. On the other hand, minimal fixed points are entirely sufficient to deduce Corollary 2.3 and similar results. We can also observe that the order type of a minimal fixed point is necessarily unique in the well-founded case. For these reasons we have decided to avoid the additional technicalities that would be necessary to determine initial fixed points, rather than just minimal ones.

In the second half of this section we are concerned with the orders $\varepsilon_{X}=(\varepsilon_{X},<_{\varepsilon_{X}})$ that have been mentioned in the introduction. In contrast to the case of $\omega^{X}$, the set $\varepsilon_{X}$ and the relation $<_{\varepsilon_{X}}$ have to be defined simultaneously. The underlying set consists of the terms that are generated by the following clauses:

• •

The set $\varepsilon_{X}$ contains a symbol [math], and a symbol $\varepsilon_{x}$ for each element $x\in X$.

• •

If $\alpha\in\varepsilon_{X}$ is not of the form $\varepsilon_{x}$, then we have a term $\omega^{\alpha}\in\varepsilon_{X}$.

• •

Given $n>1$ elements $\alpha_{n}\leq_{\varepsilon_{X}}\dots\leq_{\varepsilon_{X}}\alpha_{1}$ of $\varepsilon_{X}$, we get $\omega^{\alpha_{1}}+\dots+\omega^{\alpha_{n}}\in\varepsilon_{X}$.

The order $<_{\varepsilon_{X}}$ reflects the intuition that any term of the form $\varepsilon_{x}$ represents an $\varepsilon$-number, i. e. an ordinal $\alpha$ that satisfies $\omega^{\alpha}=\alpha$. We refer to [8, Definition 3.4] for full details of the somewhat lengthy definition.

On the set $\varepsilon_{X}$ one can define counterparts of addition, multiplication and exponentiation to the base $\omega$, taking into account that $\varepsilon$-numbers are closed under these operations (cf. [19]). In particular we have an operation

[TABLE]

which plays a similar (though somewhat less important) role as in the analysis of the order $\omega_{2}(X)$. To define a lenght function $L^{\varepsilon}_{X}:\varepsilon_{X}\rightarrow\mathbb{N}$ we recursively set

[TABLE]

We say that an element of $\varepsilon_{X}$ is decomposable if it is neither equal to [math] nor of the form $\varepsilon_{x}$. This terminology is justified in view of the following (cf. Lemma 2.1).

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

Any decomposable element of $\varepsilon_{X}$ can be uniquely written as $\omega^{\alpha}+\beta$ with $\alpha,\beta<_{\varepsilon_{X}}\omega^{\alpha}+\beta$. Furthermore we have $L^{\varepsilon}_{X}(\alpha),L^{\varepsilon}_{X}(\beta)<L^{\varepsilon}_{X}(\omega^{\alpha}+\beta)$ for any such decomposition.

Proof.

Let us first establish existence: Given a decomposable $\omega^{\alpha_{1}}+\dots+\omega^{\alpha_{n}}\in\varepsilon_{X}$, we set $\alpha:=\alpha_{1}$ and

[TABLE]

By construction (and by the definition of addition and exponentiation on $\varepsilon_{X}$) we have $\omega^{\alpha}+\beta=\omega^{\alpha_{1}}+\dots+\omega^{\alpha_{n}}$. A straightforward induction on the term $\alpha_{1}$ yields

[TABLE]

which amounts to $\alpha<_{\varepsilon_{X}}\omega^{\alpha}+\beta$. In all cases it is straightforward to verify that we have $\beta<_{\varepsilon_{X}}\omega^{\alpha}+\beta$ as well as $L^{\varepsilon}_{X}(\alpha),L^{\varepsilon}_{X}(\beta)<L^{\varepsilon}_{X}(\omega^{\alpha}+\beta)$. Due to the monotonicity of addition, uniqueness reduces to the claim that

[TABLE]

implies $\alpha=\gamma$. Aiming at a contradiction, we assume $\alpha<_{\varepsilon_{X}}\gamma$. The latter yields

[TABLE]

which is incompatible with $\beta<_{\varepsilon_{X}}\omega^{\alpha}+\beta$. ∎

We now want to characterize $\varepsilon_{X}$ as a minimal Bachmann-Howard fixed point of the order transformation

[TABLE]

Elements of the summands $1$, $Y^{2}$ and $X$ will be written as $\bot$, $\langle y_{0},y_{1}\rangle$ and $x$, respectively. The supports from Definition 1.2 amount to

[TABLE]

Together with Definition 1.3, this means that a function $\vartheta:T^{\varepsilon}_{X}(Y)\rightarrow Y$ is a Bachmann-Howard collapse if, and only if, the following conditions are satisfied:

1. (i)

we have $\vartheta(\bot)<_{Y}\vartheta(\langle y_{0},y_{1}\rangle)$ for all $y_{0},y_{1}\in Y$, and $\vartheta(\bot)<_{Y}\vartheta(x)<_{Y}\vartheta(x^{\prime})$ for all $x,x^{\prime}\in X$ with $x<_{X}x^{\prime}$, 2. (i*′*)

$\langle y_{0},y_{1}\rangle<_{Y^{2}}\langle y^{\prime}_{0},y^{\prime}_{1}\rangle$ implies $\vartheta(\langle y_{0},y_{1}\rangle)<_{Y}\vartheta(\langle y^{\prime}_{0},y^{\prime}_{1}\rangle)$, under the side condition that we have $y_{0},y_{1}<_{Y}\vartheta(\langle y^{\prime}_{0},y^{\prime}_{1}\rangle)$, 3. (i*′′*)

$\vartheta(\langle y_{0},y_{1}\rangle)<_{Y}\vartheta(x)$ holds for any $y_{0},y_{1}\in Y$ and $x\in X$ with $y_{0},y_{1}<_{Y}\vartheta(x)$, 4. (ii)

we have $y_{0},y_{1}<_{Y}\vartheta(\langle y_{0},y_{1}\rangle)$ for all $y_{0},y_{1}\in Y$.

We can now establish the desired characterization:

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

The order $\varepsilon_{X}$ is a minimal Bachmann-Howard fixed point of the transformation $T^{\varepsilon}_{X}$, for any order $X$.

Proof.

To witness that $\varepsilon_{X}$ is a Bachmann-Howard fixed point of $T^{\varepsilon}_{X}$ we need a collapsing function

[TABLE]

Relying on the ordinal arithmetic that is available in $\varepsilon_{X}$, we set

[TABLE]

It is straightforward to see that the above conditions (i) and (ii) are satisfied (note that condition (ii) could fail if we were to replace $\omega_{2}(\alpha+1)$ by $\omega_{2}(\alpha)$, as the proof of Theorem 2.2 might suggest). Condition (i*′) is verified as in the proof of Theorem 2.2. To establish condition (i′′*) we consider arbitrary $\alpha,\beta\in\varepsilon_{X}$ and $x\in X$ with

[TABLE]

Considering the order on $\varepsilon_{X}$ (cf. [8, Definition 3.4]), it is straightforward to see that the element $\varepsilon_{x}$ behaves like an $\varepsilon$-number. Hence we obtain

[TABLE]

This completes the proof that $\varepsilon_{X}$ is a Bachmann-Howard fixed point of $T^{\varepsilon}_{X}$. Let us now consider an arbitrary Bachmann-Howard collapse

[TABLE]

We need to construct an embedding $f:\varepsilon_{X}\rightarrow Y$. In view of Lemma 2.5 we can recursively define

[TABLE]

By induction on $L^{\varepsilon}_{X}(\eta)+L^{\varepsilon}_{X}(\xi)$ we can show that $\eta<_{\varepsilon_{X}}\xi$ implies $f(\eta)<_{Y}f(\xi)$. The first interesting case concerns an inequality

[TABLE]

Since $\varepsilon_{x}$ behaves like an $\varepsilon$-number we must have $\varepsilon_{x}\leq_{\varepsilon_{X}}\alpha$. Using the induction hypothesis and clause (ii) above we get

[TABLE]

Let us now consider an inequality

[TABLE]

By Lemma 2.5 we get $\alpha,\beta<_{\varepsilon_{X}}\xi$, so that the induction hypothesis yields

[TABLE]

Invoking clause (i*′′*) we can infer

[TABLE]

Finally, we consider an inequality

[TABLE]

Considering the proof of Lemma 2.5, it is straightforward to see that we must have $\alpha\leq_{\varepsilon_{X}}\gamma$. If we have $\alpha=\gamma$, then we get $\beta<_{\varepsilon_{X}}\delta$. In any case we can use the induction hypothesis to infer

[TABLE]

In view of $\alpha,\beta<_{\varepsilon_{X}}\eta<_{\varepsilon_{X}}\xi$ the induction hypothesis also yields

[TABLE]

By condition (i*′*) we now obtain

[TABLE]

as required. ∎

The statement that $\varepsilon_{X}$ is well-founded for any well-order $X$ is equivalent to the assertion that the $\omega$-jump of any set exists, as shown by A. Marcone and A. Montalbán [14] (see also the proof-theoretic argument due to B. Afshari and M. Rathen [3]). Together with Theorem 2.6 we obtain the following:

Corollary 2.7**.**

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

1. (i)

the $\omega$-jump of every set exists (which is the principal axiom of $\mathbf{ACA}_{0}^{+}$), 2. (ii)

for every well-order $X$ the transformation $Y\mapsto 1+Y^{2}+X$ has a well-founded Bachmann-Howard fixed point.

3. Collapsing and the Veblen hierarchy

In this section we show how the orders $\varphi(1+X)0$ and $\Gamma_{X}$ can be constructed as Bachmann-Howard fixed points. This will yield characterizations of arithmetical transfinite recursion and of the principle that every set lies in an $\omega$-model of $\mathbf{ATR}$.

Let us begin by recalling the Veblen hierarchy: A function $f$ from ordinals to ordinals is called a normal function if it is strictly increasing and continuous at limit stages. Equivalently, $f$ is the unique increasing enumeration of a closed and unbounded (club) class of ordinals. If $f$ is a normal function, then the class

[TABLE]

of its fixed points is itself closed and unbounded. The normal function that enumerates these fixed points is called the derivative of $f$ and is denoted by $f^{\prime}$. The Veblen hierarchy is a family of normal functions $\varphi_{\alpha}$, indexed by the ordinals. The first function in this hierarchy is usually given as

[TABLE]

Since the intersection of set-many clubs is itself a club, the function at stage $\alpha>0$ can be recursively defined by

[TABLE]

In particular we have $\varphi_{\alpha+1}={\varphi_{\alpha}}^{\prime}$ at successor stages. Since the values of $\varphi_{\alpha}$ are fixed points of all previous functions in the hierarchy, we obtain

[TABLE]

It is straightforward to deduce that we have

[TABLE]

Also note that the values of $\varphi_{\alpha}$ are additively closed; for $\alpha>0$ they are $\varepsilon$-numbers.

Relativized notation systems $\varphi(1+X)0$ for values of the Veblen function have been described in [18, Definition 2.2] (note that our summand $1$ corresponds to the minimal element $0_{Q}$ that was required in the cited reference). As in the case of $\varepsilon_{X}$, the underlying set of $\varphi(1+X)0$ needs to be defined simultaneously with the order relation. The set $\varphi(1+X)0$ and the auxiliary function $h:\varphi(1+X)0\rightarrow 1+X$ are recursively defined by the following clauses (recall that $\bot$ denotes the unique element of $1$, which coincides with the minimal element of the order $1+X$):

• •

We have an element $0\in\varphi(1+X)0$ with $h(0)=\bot$.

• •

Given elements $x\in 1+X$ and $\alpha\in\varphi(1+X)0$ with $h(\alpha)\leq_{1+X}x$, we get a term $\varphi_{x}\alpha\in\varphi(1+X)0$ with $h(\varphi_{x}\alpha)=x$.

• •

Given $n>1$ elements $\varphi_{x_{n}}\alpha_{n}\leq_{\varphi(1+X)0}\dots\leq_{\varphi(1+X)0}\varphi_{x_{1}}\alpha_{1}$ of the indicated form, we get $\alpha:=\varphi_{x_{1}}\alpha_{1}+\dots+\varphi_{x_{n}}\alpha_{n}\in\varphi(1+X)0$ with $h(\alpha)=\bot$.

The order on $\varphi(1+X)0$ (which we will usually denote by $<$ rather than $<_{\varphi(1+X)0}$) reflects equivalence ($\star$ ‣ 3), as well as the intuition that elements of the form $\varphi_{x}\alpha$ are additively closed. Full details can be found in [18, Section 2]. Note that we write $\varphi_{x}\alpha$ (without parentheses) for terms in $\varphi(1+X)0$ but $\varphi_{\gamma}(\alpha)$ (with parentheses) for values of the Veblen function on actual ordinals (an exception is made when parentheses in a term are needed to avoid ambiguity). In the sequel, we also write ($\star$ ‣ 3) for the “term version” of this equivalence in $\varphi(1+X)0$.

Similarly to the previous section, we define a length function $L^{\varphi}_{X}:\varphi(1+X)0\rightarrow\mathbb{N}$ by the recursive clauses

[TABLE]

where the second clause includes the case $n=1$. We will need the following fact:

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

We have $\alpha<\varphi_{x}\alpha$ for any element $\varphi_{x}\alpha\in\varphi(1+X)0$.

Before we prove the lemma, let us explain how it can be reconciled with the intuition that we should have $\varphi_{y}\beta=\varphi_{x}(\varphi_{y}\beta)$ in case $x<_{1+X}y$. The point is that $\varphi(1+X)0$ does not even allow to form the “superfluous” term $\varphi_{x}(\varphi_{y}\beta)$, which violates the condition $h(\varphi_{y}\beta)\leq_{1+X}x$.

Proof.

The following stronger claim can be shown by induction on $L^{\varphi}_{X}(\alpha)+L^{\varphi}_{X}(\gamma)$:

[TABLE]

Let us consider the most interesting case, in which we have $\alpha=\varphi_{x}\beta$ and $\gamma=\varphi_{y}\delta$. In view of equivalence ($\star$ ‣ 3) we need to distinguish three cases: First assume $x<_{X}y$. By induction hypothesis we get $\beta<\varphi_{y}\delta$, which does indeed imply $\varphi_{x}\beta<\varphi_{y}\delta$. Now assume that we have $x=y$. Since $\beta$ is a proper subterm of $\delta$, the induction hypothesis yields $\beta<\delta$. Once again ($\star$ ‣ 3) yields the claim. Finally, assume that we have $y<_{X}x$. In view of

[TABLE]

we see that $\varphi_{x}\beta$ cannot be equal to $\delta$; hence it must be a proper subterm. Then the induction hypothesis yields $\varphi_{x}\beta<\delta$, as needed to conclude by ($\star$ ‣ 3). ∎

Above we have used $x$ to denote an arbitrary element of $1+X$. If we want to distinguish the elements of the two summands, then we write them as $\bot$ and $1+x$. On $\varphi(1+X)0$ one readily defines an operation of addition with the usual properties. Exponentiation to the base $\omega$ can be given by

[TABLE]

This allows to develop a notion of Cantor normal form, which supports the usual definition of multiplication. Let us observe that values of the form $\varphi_{1+x}(\beta)$ do indeed behave like $\varepsilon$-numbers: In view of $\bot<_{1+X}1+x$ equivalence ($\star$ ‣ 3) reveals that $\alpha<\varphi_{1+x}\beta$ implies $\omega^{\alpha}<\varphi_{1+x}\beta$. An element of $\varphi(1+X)0$ will be called decomposable if it is not equal to [math] and not of the form $\varphi_{1+x}\alpha$ (hence $\varphi_{\bot}\alpha$ is considered as decomposable). Let us state an appropriate version of Lemma 2.5:

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

Any decomposable element of $\varphi(1+X)0$ can be uniquely written as $\omega^{\alpha}+\beta$ with $\alpha,\beta<\omega^{\alpha}+\beta$. Furthermore $L^{\varphi}_{X}(\alpha),L^{\varphi}_{X}(\beta)<L^{\varphi}_{X}(\omega^{\alpha}+\beta)$ holds for any such decomposition.

Proof.

Given a decomposable element $\varphi_{x_{1}}\alpha_{1}+\dots+\varphi_{x_{n}}\alpha_{n}\in\varphi(1+X)0$, possibly with $n=1$ and $x_{1}=\bot$, we set

[TABLE]

as well as $\beta:=\varphi_{x_{2}}\alpha_{2}+\dots+\varphi_{x_{n}}\alpha_{n}$ (in particular we have $\beta=0$ in case $n=1$). By construction we have $\omega^{\alpha}=\varphi_{x_{1}}\alpha_{1}$ and hence $\omega^{\alpha}+\beta=\varphi_{x_{1}}\alpha_{1}+\dots+\varphi_{x_{n}}\alpha_{n}$. It is straightforward to see that we have $\alpha,\beta<\omega^{\alpha}+\beta$, except when we have $x_{1}=\bot$. In that case the claim reduces to $\alpha_{1}<\varphi_{\bot}\alpha_{1}$, which requires Lemma 3.1. The condition $L^{\varphi}_{X}(\alpha),L^{\varphi}_{X}(\beta)<L^{\varphi}_{X}(\omega^{\alpha}+\beta)$ is readily verified. Uniqueness follows from basic properties of addition and exponentiation, as in Lemma 2.5. ∎

Our goal is to characterize $\varphi(1+X)0$ as a minimal Bachmann-Howard fixed point of the transformation

[TABLE]

Elements of $T^{\varphi}_{X}(Y)$ will be written as $\bot$, $\langle y_{0},y_{1}\rangle$ and $\langle x,y\rangle$, with $y_{0},y_{1},y\in Y$ and $x\in X$. The supports from Definition 1.2 can be given as

[TABLE]

Hence a function $\vartheta:T^{\varphi}_{X}(Y)\rightarrow Y$ is a Bachmann-Howard collapse if, and only if, the following conditions are satisfied:

1. (i)

we have $\vartheta(\bot)<_{Y}\vartheta(\langle y_{0},y_{1}\rangle)$ for arbitrary elements $y_{0},y_{1}\in Y$, as well as $\vartheta(\bot)<_{Y}\vartheta(\langle x,y\rangle)$ for arbitrary $y\in Y$ and $x\in X$, 2. (i*′*)

$\langle y_{0},y_{1}\rangle<_{Y^{2}}\langle y_{0}^{\prime},y_{1}^{\prime}\rangle$ implies $\vartheta(\langle y_{0},y_{1}\rangle)<_{Y}\vartheta(\langle y_{0}^{\prime},y_{1}^{\prime}\rangle)$, under the side condition that we have $y_{0},y_{1}<_{Y}\vartheta(\langle y_{0}^{\prime},y_{1}^{\prime}\rangle)$, 3. (i*′′*)

if we have $y_{0},y_{1}<_{Y}\vartheta(\langle x,y\rangle)$, then we have $\vartheta(\langle y_{0},y_{1}\rangle)<_{Y}\vartheta(\langle x,y\rangle)$, 4. (i*′′′*)

$\langle x,y\rangle<_{X\times Y}\langle x^{\prime},y^{\prime}\rangle$ implies $\vartheta(\langle x,y\rangle)<_{Y}\vartheta(\langle x^{\prime},y^{\prime}\rangle)$, under the side condition that we have $y<_{Y}\vartheta(\langle x^{\prime},y^{\prime}\rangle)$, 5. (ii)

we have $y_{0},y_{1}<_{Y}\vartheta(\langle y_{0},y_{1}\rangle)$ for arbitrary $y_{0},y_{1}\in Y$, 6. (ii*′*)

we have $y<_{Y}\vartheta(\langle x,y\rangle)$ for arbitrary $y\in Y$ and $x\in X$.

We can now prove the theorem that was stated in the introduction:

Proof of Theorem 1.4.

In the first half of the proof we show that $\varphi(1+X)0$ is a Bachmann-Howard fixed point of the transformation $T^{\varphi}_{X}$. For this purpose we must specify a Bachmann-Howard collapse

[TABLE]

Above we have discussed basic ordinal arithmetic on $\varphi(1+X)0$. As in the previous section we abbreviate $\omega_{2}(\alpha):=\omega^{\omega^{\alpha}}$, as well as $1:=\omega^{0}$. We can now set

[TABLE]

Concerning the third clause, we observe that $\varphi_{1+x}(\gamma+1)\in\varphi(1+X)0$ holds because of $h(\gamma+1)=\bot$ (note that $\gamma+1$ cannot be of the form $\varphi_{y}\delta$ with $y\neq\bot$). Terms of the form $\varphi_{\bot}\delta$ are used implicitly, via the definition of exponentiation. We need to verify the conditions stated above: Conditions (i) and (ii) are immediate, and condition (ii*′) follows from Lemma 3.1. To verify condition (i′) one argues just as in the proof of Theorem 2.2. For condition (i′′) it suffices to recall that $\varphi_{1+x}(\gamma+1)$ behaves like an $\varepsilon$-number (cf. also the proof of Theorem 2.6). In order to establish condition (i′′′*) we consider an inequality

[TABLE]

If we have $x=y$ and $\gamma<\delta$, then

[TABLE]

follows from equivalence ($\star$ ‣ 3). It remains to consider the case where we have $x<_{X}y$. Due to the side condition in (i*′′′*) we may assume

[TABLE]

which can be strengthened to $\gamma+1<\varphi_{1+y}(\delta+1)$. As we also have $1+x<_{1+X}1+y$, we can again infer $\varphi_{1+x}(\gamma+1)<\varphi_{1+y}(\delta+1)$ by equivalence ($\star$ ‣ 3). In the rest of this proof we show that the Bachmann-Howard fixed point $\varphi(1+X)0$ is minimal. For this purpose we consider an arbitrary order $Y$ with a Bachmann-Howard collapse

[TABLE]

We need to construct an order embedding $f:\varphi(1+X)0\rightarrow Y$. In view of Lemma 3.2 we can recursively define

[TABLE]

Note that elements of the form $\varphi_{\bot}\alpha=\omega^{\alpha}+0$ are covered by the second clause. To show that $\eta<\xi$ implies $f(\eta)<_{Y}f(\xi)$ we argue by induction on $L^{\varphi}_{X}(\eta)+L^{\varphi}_{X}(\xi)$. In most cases one argues just as in the proof of Theorem 2.6. The only case that is essentially new concerns an inequality

[TABLE]

In view of ($\star$ ‣ 3) we first assume that this inequality holds because we have $x<_{X}z$ and $\gamma<\xi$. Then we immediately get

[TABLE]

Due to the induction hypothesis we also obtain

[TABLE]

This is the side condition required by (i*′′′*) above. We can thus infer

[TABLE]

Now assume $x=z$ and $\gamma<\delta$. The induction hypothesis yields $f(\gamma)<_{Y}f(\delta)$, so that we obtain $\langle x,f(\gamma)\rangle<_{X\times Y}\langle z,f(\delta)\rangle$ once again. Using Lemma 3.1 we also get $\gamma<\eta<\xi$, which allows us to conclude as in the previous case. Finally, assume that we have $z<_{X}x$ and $\eta<\delta$. Using the induction hypothesis and condition (ii*′*) we obtain

[TABLE]

just as required. ∎

The statement that $\varphi(1+X)0$ is well founded for any well-order $X$ is equivalent to the principle of arithmetical transfinite recursion, as shown by H. Friedman (the first published proof seems to appear in [18], where a draft by Friedman, Montalbán and Weiermann is cited as the original reference). Now that we have proved Theorem 1.4, we immediately obtain Corollary 1.5 from the introduction.

In the rest of this section we show how the orders $\Gamma_{X}$ can be characterized in terms of minimal Bachmann-Howard fixed points. To motivate the definition of these orders we observe that the function $\alpha\mapsto\varphi_{\alpha}(0)$ is normal. We write $\gamma\mapsto\Gamma_{\gamma}$ for the derivative of this function. Its range is the club class

[TABLE]

of $\Gamma$-numbers. Note that any $\Gamma$-number is an $\varepsilon$-number.

A relativized notation system $\Gamma_{X}$ for all ordinals below the $X$-th $\Gamma$-number has been described in [15, Section 2]. As for the notation system $\varphi(1+X)0$, the underlying set $\Gamma_{X}$ and the order relation are defined by a simultaneous recursion. In the present case we must also specify a function $h:\Gamma_{X}\rightarrow\Gamma_{X}$ and a set $\mathbf{H}\subseteq\Gamma_{X}$ (here $\mathbf{H}$ refers to the German “Hauptzahlen” for (additively) principal ordinals):

• •

We have an element $0\in\Gamma_{X}\backslash\mathbf{H}$ with $h(0)=0$.

• •

For each $x\in X$ we have an element $\Gamma_{x}\in\mathbf{H}\subseteq\Gamma_{X}$ with $h(\Gamma_{x})=\Gamma_{x}$.

• •

Given elements $\alpha,\beta\in\Gamma_{X}$, we get a term $\varphi_{\alpha}\beta\in\mathbf{H}\subseteq\Gamma_{X}$ with $h(\varphi_{\alpha}\beta)=\alpha$, provided that the following conditions are satisfied:

• –

we have $h(\beta)\leq_{\Gamma_{X}}\alpha$,

• –

if $\alpha$ is of the form $\Gamma_{x}$, then we have $\beta\neq 0$.

• •

Given $n>1$ elements $\alpha_{n}\leq_{\Gamma_{X}}\dots\leq_{\Gamma_{X}}\alpha_{1}$ from $\mathbf{H}\subseteq\Gamma_{X}$, we get a term $\alpha:=\alpha_{1}+\dots+\alpha_{n}\in\Gamma_{X}\backslash\mathbf{H}$ with $h(\alpha)=0$.

The order on $\Gamma_{X}$ is determined by ($\star$ ‣ 3) and ($\dagger$ ‣ 3), where the latter are to be read as statements about terms from $\Gamma_{X}$ rather than actual ordinals. Full details of the somewhat lengthy definition can be found in [15, Section 2].

Addition, multiplication and exponentiation on $\Gamma_{X}$ can be defined as in the case of $\varphi(1+X)0$. We point out that $\varphi_{0}\alpha\in\Gamma_{X}$ assumes the role of $\varphi_{\bot}\alpha\in\varphi(1+X)0$. Elements of the form $\Gamma_{x}$ or $\varphi_{\alpha}\beta$ with $\alpha\neq 0$ behave like $\varepsilon$-numbers. To define a length function $L^{\Gamma}_{X}:\Gamma_{X}\rightarrow\mathbb{N}$ we set

[TABLE]

It will be convenient to use a somewhat different decomposition than before:

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

Any non-zero element of $\Gamma_{X}\backslash\mathbf{H}$ can be uniquely written as $\alpha+\beta$ with $\alpha,\beta<_{\Gamma_{X}}\alpha+\beta$ and $\alpha\in\mathbf{H}$. Furthermore $L^{\Gamma}_{X}(\alpha),L^{\Gamma}_{X}(\beta)<L^{\Gamma}_{X}(\alpha+\beta)$ holds for any such decomposition.

Proof.

Given an element $\alpha_{1}+\dots+\alpha_{n}$ we set $\alpha:=\alpha_{1}$ and $\beta:=\alpha_{2}+\dots+\alpha_{n}$ (in particular $\beta=\alpha_{2}$ in case $n=2$). It is straightforward to see that this satisfies the desired properties. To establish uniqueness it suffices to observe that $\gamma+\alpha=\alpha$ holds for any $\gamma<_{\Gamma_{X}}\alpha\in\mathbf{H}$ (cf. the proof of Lemma 2.5). ∎

We will also need the following variant of Lemma 3.1 (cf. the explanation after the statement of that result):

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

We have $\alpha,\beta<_{\Gamma_{X}}\varphi_{\alpha}\beta$ for any element $\varphi_{\alpha}\beta\in\Gamma_{X}$.

Proof.

Yet again, the following stronger claim can be established by induction on the joint complexity $L^{\Gamma}_{X}(\eta)+L^{\Gamma}_{X}(\xi)$ of $\eta$ and $\xi$:

[TABLE]

Let us consider the case of $\eta=\varphi_{\alpha}\beta$ and $\xi=\varphi_{\gamma}\delta$. In contrast to Lemma 3.1, we must now distinguish two possibilities: If $\eta$ is a subterm of $\delta$, then one argues just as before. Now assume that $\eta$ is a subterm of $\gamma$. Then the induction hypothesis yields both $\alpha<_{\Gamma_{X}}\gamma$ and $\beta<_{\Gamma_{X}}\varphi_{\gamma}\delta$. We can conclude $\varphi_{\alpha}\beta<_{\Gamma_{X}}\varphi_{\gamma}\delta$ by ($\star$ ‣ 3). ∎

Our aim is to characterize $\Gamma_{X}$ in terms of the order transformation

[TABLE]

Elements of $T^{\Gamma}_{X}(Y)$ will be written as $\bot$, $\langle i,y_{0},y_{1}\rangle$ and $x$, with $i\in\{0,1\}$, $y_{0},y_{1}\in Y$ and $x\in X$. The supports from Definition 1.2 amount to

[TABLE]

In view of Definition 1.3 this means that a function $\vartheta:T^{\Gamma}_{X}(Y)\rightarrow Y$ is a Bachmann-Howard collapse if, and only if, the following conditions are satisfied:

1. (i)

we have $\vartheta(\bot)<_{Y}\vartheta(\langle i,y_{0},y_{1}\rangle)$ for arbitrary $i\leq 1$ and $y_{0},y_{1}\in Y$, as well as $\vartheta(\bot)<_{Y}\vartheta(x)<_{Y}\vartheta(x^{\prime})$ for any $x,x^{\prime}\in X$ with $x<_{X}x^{\prime}$, 2. (i*′*)

$\langle y_{0},y_{1}\rangle<_{Y^{2}}\langle y^{\prime}_{0},y^{\prime}_{1}\rangle$ implies $\vartheta(\langle i,y_{0},y_{1}\rangle)<_{Y}\vartheta(\langle i,y^{\prime}_{0},y^{\prime}_{1}\rangle)$ for each $i\leq 1$, under the side condition that we have $y_{0},y_{1}<_{Y}\vartheta(\langle i,y^{\prime}_{0},y^{\prime}_{1}\rangle)$, 3. (i*′′*)

$y_{0},y_{1}<_{Y}\vartheta(\langle 1,y^{\prime}_{0},y^{\prime}_{1}\rangle)$ implies $\vartheta(\langle 0,y_{0},y_{1}\rangle)<_{Y}\vartheta(\langle 1,y^{\prime}_{0},y^{\prime}_{1}\rangle)$, 4. (i*′′′*)

$y_{0},y_{1}<_{Y}\vartheta(x)$ implies $\vartheta(\langle i,y_{0},y_{1}\rangle)<_{Y}\vartheta(x)$ for each $i\leq 1$, 5. (ii)

we have $y_{0},y_{1}<_{Y}\vartheta(\langle i,y_{0},y_{1}\rangle)$ for each $i\leq 1$.

We can now establish the promised characterization:

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

The order $\Gamma_{X}$ is a minimal Bachmann-Howard fixed point of the transformation $T^{\Gamma}_{X}$, for each order $X$.

Proof.

Let us first construct a Bachmann-Howard collapse

[TABLE]

As before we abbreviate $\omega_{2}(\alpha):=\omega^{\omega^{\alpha}}$. We then set

[TABLE]

To see that we have $\varphi_{1+\alpha}(\beta+1)\in\Gamma_{X}$ it suffices to observe that we have $h(\beta+1)=0$ (as $\beta+1$ does not lie in $\mathbf{H}\backslash\{\varphi_{0}0\}$) and $\beta+1\neq 0$ (which is only relevant if $\alpha=\Gamma_{x}$). We need to show that the above conditions are satisfied. Condition (i) is immediate. To establish condition (i*′) one argues just as in the proofs of Theorems 2.2 and 1.4. Conditions (i′′) and (i′′′*) hold because $\varphi_{1+\alpha}(\beta+1)$ behaves like an $\varepsilon$-number (due to $1+\alpha\neq 0$) while $\Gamma_{x}$ behaves like a $\Gamma$-number (cf. equation ($\dagger$ ‣ 3)). Using Lemma 3.4, one readily checks that condition (ii) is satisfied. To show that $\Gamma_{X}$ is minimal we consider an arbitrary order $Y$ with a Bachmann-Howard collapse

[TABLE]

Relying on Lemma 3.3, we define $f:\Gamma_{X}\rightarrow Y$ by the recursive clauses

[TABLE]

In order to show that $\eta<_{\Gamma_{X}}\xi$ implies $f(\eta)<_{Y}f(\xi)$ one argues by induction on the number $L^{\Gamma}_{X}(\eta)+L^{\Gamma}_{X}(\xi)$. In the following we discuss the cases that are not already covered by the proofs of Theorems 2.6 and 1.4 (where Lemma 3.4 assumes the role of Lemma 3.1). Let us first consider an inequality

[TABLE]

By Lemma 3.4 we get $\alpha,\beta<_{\Gamma_{X}}\eta<_{\Gamma_{X}}\xi$, so that the induction hypothesis yields

[TABLE]

Using condition (i*′′′*) from above we can infer

[TABLE]

The case of an inequality $\alpha+\beta<_{\Gamma_{X}}\Gamma_{x}$ is treated similarly. Let us now establish the induction step for an inequality

[TABLE]

In view of equation ($\dagger$ ‣ 3) we must have $\Gamma_{x}\leq_{\Gamma_{X}}\alpha$ or $\Gamma_{x}\leq_{\Gamma_{X}}\beta$. In either case we can invoke the induction hypothesis and condition (ii) to get

[TABLE]

A similar argument covers the case of an inequality $\Gamma_{x}<_{\Gamma_{X}}\alpha+\beta$ (where we must have $\Gamma_{x}\leq_{\Gamma_{X}}\alpha$). Finally we consider an inequality

[TABLE]

Since $x\mapsto\Gamma_{x}$ represents a normal function we have $x<_{X}z$. By condition (i) we get $f(\eta)=\vartheta(x)<_{Y}\vartheta(z)=f(\xi)$, just as required. ∎

The statement that $\Gamma_{X}$ is well-founded for any well-order $X$ is equivalent to the assertion that every set lies in a countable coded $\omega$-model of arithmetical transfinite recursion, as shown by Rathjen [15]. We can conclude with the following:

Corollary 3.6**.**

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

1. (i)

every set is contained in a countable coded $\omega$-model of $\mathbf{ATR}$, 2. (ii)

for every well-order $X$ the transformation $Y\mapsto 1+2\times Y^{2}+X$ has a well-founded Bachmann-Howard fixed point.