\section{Introduction}
A \emph{fast growing hierarchy} is a collection of functions $B_\alpha:\mathbb{N}\to\mathbb{N}$, where $\alpha$ ranges over some set of ordinal numbers, and each $B_\alpha$ eventually dominates $B_\beta$, for all $\beta<\alpha$. 
One is mainly interested in fast-growing hierarchies obtained through a given recursive construction which usually generalizes the process that produces multiplication as iterated addition, exponentiation as iterated multiplication, etc.

Fast-growing hierarchies can be defined in various ways, though all reasonable definitions that are known yield sequences of functions that agree at ordinals $\alpha$ which are sufficiently closed. 
Examples of these are the \emph{Hardy hierarchy} (named after G. H. Hardy), the \emph{iterative fast growing hierarchy}, and the \emph{binary fast growing hierarchy}. Let us focus on the latter one, for the sake of definiteness. 
It is defined by transfinite induction according to the following construction:
\begin{align*}
B_0(n) &= n+1&\\
B_{\alpha+1}(n) &= B_\alpha\circ B_\alpha(n)&\\
B_\lambda(n) &= B_{\lambda[n]}(n), &\text{ at limit stages,}
\end{align*}
where for each limit ordinal $\lambda$, $\{\lambda[n]:n\in\mathbb{N}\}$ is a sequence which converges to $\lambda$, fixed in advance. 
The precise functions defined depend on the sequences chosen, but for natural choices of sequences, the functions behave very regularly. The ordinal $\varepsilon_0$ is defined by:
\[\varepsilon_0 = \sup\{\omega,\omega^\omega,\omega^{\omega^\omega},\hdots\},\]
$B_{\varepsilon_0}$ is a total recursive function whose totality cannot be proved in Peano Arithmetic (or, equivalently, Arithmetical Comprehension, $\aca$).
The foundational significance of fast-growing functions was observed by Ackermann and, later, by Kreisel \cite{Kr52}.
\begin{theorem}[Kreisel 1952, essentially]\label{KreiselsTheorem}
There is a canonical wellordering $W$ of $\mathbb{N}$ of length $\varepsilon_0$ such that the following theories prove the same $\Pi^0_2$ theorems:
\begin{enumerate}
\item Arithmetical Comprehension;
\item Primitive Recursive Arithmetic + $\{B_\alpha$ is total  $:\alpha\in W\}$.
\end{enumerate}
\end{theorem}
Kreisel's theorem is a computational analysis of arithmetic, in the sense that it gives an explicit characterization of the recursive functions which are provably total.


Kreisel's result is of great foundational significance and has led to a great deal of metamathematical and combinatorial results in the context of arithmetic, as well as generalizations to stronger systems. For instance, one can prove a version of Kreisel's theorem for the subsystem $\Pi^1_1$-$\ca$ of analysis where $B_{\varepsilon_0}$ is replaced by $B_{\psi_0(\aleph_\omega)}$ (see Buchholz \cite{Bu87}).
Here, $\psi_0(\aleph_\omega)$ is the \emph{Takeuti ordinal}, a recursive ordinal that is most easily described by \emph{ordinal collapsing functions} for the uncountable cardinals $\aleph_n$, where $n\in\mathbb{N}$. 
$\Pi^1_1$-$\ca$ is a historically and mathematically important theory, and  is the strongest of the ``big five'' subsystems of Second-Order Arithmetic commonly studied in Reverse Mathematics. Ordinal collapsing functions were introduced by Bachmann \cite{Ba50} and are a powerful method in proof theory involved in the description of large recursive ordinals, such as the \emph{Bachmann-Howard} ordinal $\psi(\varepsilon_{\Omega+1})$, the Takeuti ordinal, and other larger numbers such as the proof-theoretic ordinals of $\kpi$ and $\kp$ + $\Pi_3$-reflection. These ordinals involve collapsing functions for inaccessible and weakly compact cardinals, respectively; see Rathjen \cite{Ra99} for an overview.


The first observation we make is that fast-growing hierarchies can be regarded as functors on the category of natural numbers with strictly increasing functions as morphisms. This fact was perhaps underpinning the main result of \cite{AFRW}. Let us say more about this observation.

For our purposes, it will be convenient to shift our focus to the norm-based presentation of fast-growing hierarchies.
This presentation goes back to \cite{BCW94} and, for our purposes, is described as follows: suppose that we are given a denotation system $D$ for ordinals.
The definition of ``denotation system'' is recalled in the next section, where these are defined as  a particular kind of \emph{dilator.} The reader unfamiliar with denotation systems might temporarily  think of $D$ as a system for representing ordinals in some way using natural numbers as parameters. For example, we may think of representing ordinals ${<}\omega^\omega$ as sums of powers of $\omega$; e.g.,
\[\omega^7 + \omega^3+ 21.\]
The \emph{norm} $N\alpha$ of an ordinal $\alpha$ is the strict supremum of the natural number parameters which occur in the denotation.
We define
\[B_\alpha(n) = \sup\{B_\beta\circ B_\beta(n): \beta<\alpha\wedge N\beta \leq n\} \cup \{n+1\}.\]

Natural numbers can be represented by repeated applications of functions in the hierarchy:
\begin{equation} \label{eqIntroNormalForm}
m = B_{\alpha_k} B_{\alpha_{k-1}}\dots B_{\alpha_1} (n).
\end{equation}
If $n$ is fixed and some constraints are imposed on the values $n_1, \hdots, n_k$, then the resulting representation is unique. 
We define
\[B_D(n) = B_{D(\omega)}(n) = \sup\{B_\beta\circ B_\beta(n): N\beta \leq n\} \cup \{n+1\}.\]
Making use of the representation of natural numbers in terms of iterations of the fast-growing hierarchy, we can regard $B_D$ as a functor on the category of natural numbers with strictly increasing functions as morphisms. This is proved in \S \ref{SectFunctor}.

 From the fact that $B_D$ is a functor on the category of natural numbers, it follows that $B_D$ can be uniquely extended to a finitary functor on the category of linear orders. In particular, expressions of the form \eqref{eqIntroNormalForm} can be given transfinite parameters and construed as denotations for elements of some linear order. The main insight in \S \ref{SectCollapse} is that (up to isomorphism) these denotations are obtained from ordinal collapsing functions. Thus, we have an object $B_D$ which can be simultaneously viewed from the point of view of two fundamental concepts in Proof Theory: fast-growing functions and ordinal collapses.

In \S \ref{SectTheorem}, we prove the main theorem. We first show that the ordinal collapses given by $B_D$ are wellfoundedness-preserving, so that if $A$ is a wellorder, then so too is $B_D(A)$. In fact, $B_D$ is a functor on the category of ordinal numbers, and indeed a \emph{dilator}. The proof of this fact requires the use of $\Pi^1_1$-$\ca$, and this is unavoidable: the fact that $B_D$ is wellfoundedness-preserving in turn implies $\Pi^1_1$-$\ca$. This way we obtain a restatement of $\Pi^1_1$-$\ca$ in terms of fast-growing hierarchies and abstract ordinal collapses. We state the theorem; for all undefined terms, we refer the reader to the following section.

\begin{theorem}\label{MainIntro}
The following are equivalent over $\aca$:
\begin{enumerate}
\item  $\Pi^1_1$-$\ca$;
\item for every weakly finite dilator $D$, $B_D$ is a weakly finite dilator;
\item  for every dilator $D$, $B_D$ is a dilator.
\end{enumerate}
\end{theorem}

Theorem \ref{MainIntro} fits within the family of results known as \emph{wellordering principles}. Most commonly, these are principles of the form ``if $X$ is a wellorder, then $f(X)$ is a wellorder,'' where $f$ is some transformation. 
These principles have been extensively studied in Reverse Mathematics and have led to reformulations of several subsystems of analysis. Some examples are the works of Girard \cite{Gi87},  Friedman (unpublished), Hirst \cite{Hi94}, Afshari-Rathjen \cite{AfRa09}
, Marcone-Montalb\'an \cite{MaMo11}, Rathjen-Valencia Vizca\'ino \cite{RaVV15}, Thomson-Rathjen \cite{ThRa20}, and \cite{RaWe11}. Higher-type wellordering principles were used by Girard \cite{GiInf} and Freund \cite{Fr19} to characterize $\Pi^1_1$-$\ca$. Freund's theorem is an ingredient of our proof of Theorem \ref{MainIntro}. Freund's principle maps dilators to wellorderings, while ours and Girard's map dilators to dilators. Girard's characterization of  $\Pi^1_1$-$\ca$ asserts the totality of the functor $\Lambda$, which itself is reminiscent of fundamental-sequence--based fast-growing hierarchies. Wellordering principles for theories such as $\Pi^1_1$-$\ca$ which are not $\Pi^1_2$-axiomatizable require the use of higher-type objects such as dilators. 

Although throughout this article we focus on the binary fast-growing hierarchy $B_D$, we mention that the statement of Theorem \ref{MainIntro} applies to many of the other usual fast-growing hierarchies as well. The use of $B_D$ is merely for convenience and to simplify the computations involved.

\subsection*{Acknowledgements}
J.P.A. was partially supported by FWF grants I4513N and ESP-3N and FWO grant 0E3017319; F.P. was supported by FWO grant G0F8421N; A.W. was partially supported by FWO grants G0E2121N and G030620N.
 

\section{Preliminaries}
We deal with the category $\LO$. The objects of $\LO$ are linear orders whose domains are subsets of $\mathbb{N}$. The morphisms are strictly increasing maps between this orders. 
We shall work within the subsystem $\aca$ of second-order arithmetic. This is the system in the language of second-order arithmetic (which contains sorts for natural numbers and sets of natural numbers) whose principal axioms are the induction axiom and the schema asserting that every arithmetically definable set exists.
When it leads to no confusion, we shall leave the precise formalization of statements to the reader and work informally. 

In the language of second-order arithmetic one cannot generally speak of functors from $\LO$ to $\LO$; thus, we shall restrict to dealing with \emph{finitary} functors, i.e., functors preserving co-limits of upward directed diagrams (direct limits in the model-theoretic sense). These can be coded by sets of natural numbers: 

We consider $\Nat$, the full subcategory of $\LO$ where objects are natural numbers $n$, which we identify with the  orders $([0,n),<)$. 
Since both $\mathsf{Ob}_\Nat$ and $\mathsf{Mor}_\Nat$ are countable, each functor from $\Nat$ to $\LO$ can be coded by a set of natural numbers. 
Each functor $D\colon \Nat\to \LO$ can be uniquely extended to a finitary functor $D\colon \LO\to \LO$ as follows: 

Below, we write $A'\subseteq_{\mathsf{fin}} A$ if $A'$ is a finite subset (or substructure) of $A$.
Given a linear order $A$, we consider an upward directed diagram  $H_A$ consisting of all finite suborders $A'\subseteq_{\mathsf{fin}}A$ and all morphisms $\id_{A'\to A''}$, for $A'\subseteq_{\mathsf{fin}}A''\subseteq_{\mathsf{fin}}A$. 
Let $H'$ be the naturally isomorphic diagram in which all objects are orders in $\mathsf{Ob}_\Nat$. 
Applying $D$ to all morphisms and objects in $H'_A$, we obtain a diagram $D[H'_A]$ and define 
\[D(A) = \varinjlim D[H'],\]
where 
$\injlim D[H']$ denotes the co-limit of the diagram.
The value $D(f)$, for an $\LO$-morphism $f\colon A\to C$, is recovered in the natural way.

A coded finitary functor $D$ on $\LO$ is called a pre-dilator if it preserves pullbacks. Clearly, $D$ preserves pullbacks if and only if its restriction to $\Nat$ preserves pullbacks.


It will be convenient for our purposes to work with inclusion-preserving (or \emph{$\subseteq$-preserving}) functors. These are the functors $D$ such that for any order $A$ and any suborder $B$ of $A$,
\begin{enumerate}
\item $D(B)$ is a suborder of $D(A)$, and furthermore \item $D(\id_{B\to A})=\mathsf{id}_{D(B)\to D(A)}$, where $\id_{B\to A}\colon B\to A$, denotes the inclusion map given by $\id_{B\to A}(x)=x$.
\end{enumerate} 
Finitary $\subseteq$-preserving functors were called $\omega$-local functors by S.~Feferman \cite{Fe72}.\footnote{Feferman \cite{Fe72} is an early reference for functorial ordinal notation systems.}
For $\subseteq$-preserving functors there are convenient reformulations of the conditions of being a finitary functor and a pre-dilator. Namely, a $\subseteq$-preserving functor $D$ is finitary if and only if for any order $A$, we have 
\[D(A)=\bigcup\limits_{A'\subseteq_{\mathsf{fin}}A}D(A').\] 
An  $\subseteq$-preserving finitary functor $D$ is a pre-dilator iff for any orer $A$ and its suborders $B,C\subseteq A$ we have $D(B\cap C)=D(B)\cap D(C)$.

Working in $\aca$, we code $\subseteq$-preserving finitary functors as follows. 
We consider the full subcategory $\FO$ of $\LO$, where objects are finite linear orders. 
As in the case of $\Nat$, both  $\mathsf{Ob}_\FO$ and $\mathsf{Mor}_\FO$ are countable, so $\subseteq$-preserving functors $D$ from $\FO$ to $\LO$ can be naturally each by a set of natural numbers. 
We extend any such $D$ to a functor with domain $\LO$ by putting 
$$D(A)=\bigcup\limits_{A'\subseteq_{\mathsf{fin}}A}D(A')\;\;\;\text{ and }\;\;\;D(f)=\bigcup\limits_{A'\subseteq_{\mathsf{fin}}A}D(f\upharpoonright A').$$ 
Here for $f\colon A\to C$ and $A'\subseteq A$, $f\upharpoonright A'\colon A'\to C$ is the  restriction of $f$.

A pre-dilator is called a dilator if it maps well-orders to well-orders. Dilators were introduced by Girard \cite{Gi81}, to whom we refer the reader for further background. The fundamental theorem of dilators states that every pre-dilator $D$ is naturally isomorphic to a \emph{denotation system}, a special kind of $\subseteq$-preserving predilators.

Each denotation system $D$ consists of a set of terms $t(x_1, \hdots, x_n)$ and comparison rules establishing, for each pair of terms $t(\vec x)$ and $s(\vec y)$, which one is greater, depending on the relative ordering of the constants $\vec x$ and $\vec y$. Note that we do not allow $t(\vec x) = s(\vec y)$ unless $t(\vec x)$ and $s(\vec y)$ are syntactically the same term.
This allows us to define a binary relation $D(A)$ for each linear order $A$ as follows: the domain of $D(A)$ is the set of all expressions $t(a_1,\ldots,a_n)$, where $a_1>\ldots>a_n$ and $t(x_1,\ldots,x_n)$ is a $D$-term. The relative ordering of elements of the domain of $D(A)$ is determined by the comparison rules for each pair of terms.

Given a strictly increasing map $f\colon A\to C$ between finite orderings $A$ and $C$, we define 
\begin{align*}
D(f)\colon D(A) &\to D(C)\\
D(f)\colon t(a_1,\ldots,a_n)&\mapsto t(f(a_1),\ldots,f(a_n))
\end{align*}

We shall sometimes identify the values of terms $t(x_1, \hdots, x_n)$ with the ordinals they denote.
If $\alpha =t(x_1, \hdots, x_n)$, we call the set $\{x_1, \hdots, x_n\}$ the \emph{support} of $\alpha$ and denote it by $\supp(\alpha)$. Given ordinals $\alpha,\beta$, we write
\[\supp(\alpha) < \beta \text{ if $x_i<\beta$ for all $x_i \in \supp(\alpha)$}.\]




\subsection{Conventions} Whenever we deal with a linear order $L$, we will write $<_L$ to indicate the ordering. If no confusion arises, we may occasionally omit reference to $L$ and simply write $<$.

When dealing with functions $f(x)$, we will sometimes omit brackets and simply write $fx$. The purpose of this is to avoid cluttering when dealing with nested application of functions.

\section{The functoriality of fast-growing hierarchies}
\label{SectFunctor}
In this section, we  fix a dilator $D$ and investigate the functorial structure of $B_D$. All the constructions in this section are formalizable in $\aca$. Note that the norms $N\alpha$ -- and hence $B$-hierarchy on $D(\omega)$ -- are unaffected if we replace $D$ by a naturally isomorphic denotation system. Hence, in order to simplify notation, we will assume that $D$ is a denotation system (in fact we will only use that it is $\subseteq$-preserving). 
If so, $N \alpha= \min \{n\mid \alpha \in D(n)\}$.

\iffalse
The idea is to note that, given $n\in\mathbb{N}$, every  natural number $m$ can be canonically represented as the value of an expression
\[B_{\alpha_k}\dots B_{\alpha_1}(n),\]
and, if we require some regularity conditions on the ordinals $\alpha_i$, the representation is unique and called the \emph{$n$-normal form}.
Given a finite strictly increasing function $f$ on the natural numbers, we can define $B_D(f)$ to be the function mapping $m$ to the value of the term above, with the ordinals replaced by their ``shifts'' according to $D(f)$. Below, we make this definition more precise and show that behaves properly, i.e., maps normal forms to normal forms.

\begin{lemma}
For any $\alpha\in D(\omega)$ the function $B_\alpha$ is strictly increasing.
\end{lemma}
\proof
This is proved by induction on $\alpha$. Assuming $x<y$, there are two cases. If $B_\alpha(y) = y+1$, then 
we have $B_\beta(B_\beta(y)) \leq y+1$ whenever $\beta<\alpha$ and $N\beta\leq y$, in which case we have $B_\beta(B_\beta(y)) \leq y+1$ whenever $\beta<\alpha$ and $N\beta\leq x$. For such $\beta$ by induction we thus have 
\[B_\beta(B_\beta(x)) < B_\beta(B_\beta(y)) \leq y+1,\]
so that $B_\beta(B_\beta(x)) < y + 1$ whenever $\beta<\alpha$ and $N\beta$ is at most $y$ (and hence also when $N\beta$ is at most $x$). Thus, $B_\alpha(x) < B_\alpha(y)$ in this case.

Otherwise, $B_\alpha(y)$ is of the form $B_\beta(B_\beta(y))$ for some $\beta<\alpha$, then we have 
\[x+1 < y+1 \leq B_\beta(B_\beta(y)),\]
so that either $B_\alpha(x) = x+1 < B_\alpha(y)$, or else
\begin{align*}
B_\alpha(x) 
&= B_\gamma(B_\gamma(x)) &\text{ for some $\gamma<\alpha$ with $N\gamma\leq x$}\\
&< B_\gamma(B_\gamma(y)) &\text{  by induction hypothesis}\\
&\leq B_\beta(B_\beta(y)) &\text{ since $N\gamma\leq y$}\\
&= B_\alpha(y),
\end{align*}
as desired.
\endproof
\fi

\begin{definition}
Let $n$ be a natural number and $\alpha\in D(\omega)\cup \{D(\omega)\}$. An \emph{$(n,\alpha)$-normal form term} is an expression of one of the following forms:
\begin{enumerate}
\item $m$, where $m<n$ is a natural number; or
\item $B_{\alpha_k}\dots B_{\alpha_1}(n)$, where 
\begin{enumerate}
\item $\alpha_k <_{D(\omega)} \dots <_{D(\omega)} \alpha_1<\alpha$; and
\item $N\alpha_{i+1} \leq B_{\alpha_i}\dots B_{\alpha_1}(n)$ for all $i$ with $0\leq i<k$.
\end{enumerate}
\end{enumerate}
\end{definition}

Normal form terms denote natural numbers, obtained simply by evaluating the functions. If $m = B_{\alpha_k}\dots B_{\alpha_1}(n)$ is as above, we may omit reference to $\alpha$ and call this expression the \emph{$n$-normal form} of $m$; if so, we may write 
\[m \stackrel{NF}{=} B_{\alpha_{k}}\dots B_{\alpha_1}(n).\]

For finite sequences of ordinals $(\alpha_1,\ldots,\alpha_k)\in (D(\omega))^{<\omega}$ the lexicographical comparision $<_{\mathsf{lex}}$ is defined in the usual manner: by putting 
\[(\alpha_1,\ldots,\alpha_k)<_{\mathsf{lex}} (\beta_1,\ldots,\beta_l)\] 
if there exists $0\le n\le \max(k,l)$ such that $\alpha_i=\beta_i$, for $1\le i\le n$ and either $n=k<l$ or $n<\max(k,l)$ and $\alpha_{n+1}<_{D(\omega)}\beta_{n+1}$.


\begin{lemma}[$\aca$]\label{normal_forms} 
Suppose $\alpha\in D(\omega)\cup \{D(\omega)\}$ and $n\in\mathbb{N}$. Then, 
\begin{enumerate}
\item each number smaller than $B_{\alpha}(n)$ is the value of a unique $(n,\alpha)$-normal form; and
\item  for any two $(n,\alpha)$-normal forms $B_{\alpha_1}\ldots B_{\alpha_k} (n)$ and $B_{\beta_l}\ldots B_{\beta_1} (n)$, we have
  $$B_{\alpha_1}\ldots B_{\alpha_k} (n)< B_{\beta_l}\ldots B_{\beta_1} (n)\iff (\alpha_1,\ldots,\alpha_k)<_{\mathsf{lex}}(\beta_1,\ldots,\beta_l).$$
\end{enumerate}
\end{lemma}
\begin{proof}
  We prove the lemma by transfinite induction on $\alpha$. If there are no $\alpha'<_{D(\omega)}\alpha$ with $N\alpha'\le n$, then $B_\alpha(n)=n+1$ and the only $(n,\alpha)$-normal forms are constants $\le n$ and hence the lemma holds.

Otherwise, choose $\alpha'<_{D(\omega)}\alpha$ such that $N\alpha'\leq n$ and $B_\alpha(n)=B_{\alpha'}(B_{\alpha'}(n))$. Let $s=B_{\alpha'}(n)$. By induction hypothesis,
  \begin{enumerate}
  \item any number $<B_{\alpha'}(n)$ is the value of a unique $(s,\alpha')$-normal form;
  \item any number $<s$ is the value of a unique $(n,\alpha')$-normal form.
  \end{enumerate}
Combining these two facts we observe that each number $<B_{\alpha}(n)$ is the value of the unique term of one of the following three forms:
  \begin{enumerate}
  \item $m$, for $m<n$;
  \item \label{nf_2} $B_{\alpha_k}\dots B_{\alpha_1}(n)$, where $\alpha_k <_{D(\omega)} \dots <_{D(\omega)} \alpha_1<_{D(\omega)}\alpha'$ and $N\alpha_{i+1} \leq B_{\alpha_i}\dots B_{\alpha_1}(n)$ for all $i$ with $0\leq i<k$;
    \item \label{nf_3} $B_{\alpha_k}\dots B_{\alpha_1}(B_{\alpha'}(n))$, where  $\alpha_k <_{D(\omega)} \dots <_{D(\omega)} \alpha_1<_{D(\omega)}\alpha'$ and $N\alpha_{i+1} \leq B_{\alpha_i}\dots B_{\alpha_1}(B_{\alpha'}(n))$ for all $i$ with $0\leq i<k$.
    \end{enumerate}
Since $\alpha'<_{D(\omega)}\alpha$ and $N\alpha' \leq n$, it follows that any number $<B_\alpha(n)$ is indeed the value of an $(n,\alpha)$-normal form. To prove that $(n,\alpha)$-normal forms are compared as prescribed, we simply need to consider the cases of the forms \eqref{nf_2} and \eqref{nf_3}. 
If both normal forms are of the same form, then we get the comparison property directly by induction hypothesis.
The fact that the comparison property holds for terms of different forms follows from the fact that any term of the form \eqref{nf_2} has smaller value than any term of  the form \eqref{nf_3}. This is because, by construction, every term of the form \eqref{nf_2} has value $<s$ and every term of the form \eqref{nf_3} has value $\ge s$.\end{proof}





\iffalse

In the remainder of this subsection, we prove properties of $n$-normal form terms. 

\begin{lemma}\label{LemmaLexicographic}
The values of $n$-normal form terms are compared lexicographically.
That is, suppose $B_{\alpha_k}\dots B_{\alpha_1}(n)$ and $B_{\beta_l}\dots B_{\beta_1}(n)$ are $n$-normal form terms. Then, the following are equivalent:
\begin{enumerate}
\item $B_{\alpha_k}\dots B_{\alpha_1}(n) < B_{\beta_l}\dots B_{\beta_1}(n)$,
\item $(\alpha_1, \hdots, \alpha_k) <_{lex} (\beta_1, \hdots, \beta_l)$.
\end{enumerate}
\end{lemma}
\proof
We first consider a simple case.
Suppose that $B_\alpha(n)$ and
\[m = B_{\beta_l}\dots B_{\beta_1}(n)\]
are two $n$-normal form terms and that $\beta_1 < \alpha$. Let us show that  $m < B_\alpha(n)$.
Since $B_{\beta_1}(n)$ is an $n$-normal form term, we have $N\beta_1 \leq n$, so that
\[B_{\beta_1}B_{\beta_1}(n) \leq B_\alpha(n),\]
simply by the definition of $B_\alpha$ and the fact that $\beta_1 < \alpha$. Now, $B_{\beta_2}B_{\beta_1}(n)$ is also an $n$-normal form, which implies that $\beta_2 < \beta_1$ and that $N\beta_2 \leq B_{\beta_1}(n)$. By the definition of $B_{\beta_1}$, we have 
\[B_{\beta_2}B_{\beta_2}B_{\beta_1}(n) \leq B_{\beta_1}B_{\beta_1}(n) \leq B_\alpha(n).\]
By repeating this argument, one shows that
\begin{align*}
m = B_{\beta_l}\dots B_{\beta_1}(n) 
&<B_{\beta_l} B_{\beta_l}\dots B_{\beta_1}(n) \\
&\leq B_{\beta_{l-1}} B_{\beta_{l-1}}\dots B_{\beta_1}(n)\\ &\leq \dots \\
& \leq B_{\beta_1}B_{\beta_1}(n) \\
&\leq B_\alpha(n).
\end{align*}

Since $n$ was arbitrary, the conclusion of the lemma follows immediately from this.
\endproof

\begin{lemma}
Every $m < B_D(n)$ is the value of a unique $n$-normal form term, up to equality of ordinal notations, i.e., if
\[m = B_{\alpha_k}\dots B_{\alpha_1}(n) = B_{\beta_l}\dots B_{\beta_1}(n),\]
then $k = l$ and for each $1\leq i\leq k$, $\alpha_i =_D \beta_i$.
\end{lemma}
\proof
Uniqueness is immediate from Lemma \ref{LemmaLexicographic}, so we only need to show that every natural number $m$ is the value of some $n$-normal form term. This is clear for $m< n$, so let us suppose that $n\leq m$.

By induction on $i$, and starting with $i = 0$, we define $\alpha_{i+1}$ to be the greatest ordinal such that 
\[B_{\alpha_{i+1}}\dots B_{\alpha_1}(n) \leq m.\]
We stop the process when $B_{\alpha_{i+1}}\dots B_{\alpha_1}(n)\geq m$. First, we observe that $\alpha_{i+1}$ is well defined, in the sense that 
\[\max\{\alpha: B_{\alpha}\dots B_{\alpha_1}(n) \leq m\}\]
always exists provided that the set is nonempty. This is immediate from the definition of $B_\alpha(x)$. Second, we observe that there is a maximum $k$ such that $\alpha_k$ is defined. This is because each function $B_\alpha$ is strictly increasing.
Let $\alpha_1, \hdots, \alpha_k$ be the sequence thus produced. Our third observation is that 
$$B_{\alpha_{k}}\dots B_{\alpha_1}(n) = m.$$
This is because if the expression on the left-hand side were strictly smaller than $m$, we would be able to further extend it by applying some $B_{\alpha_{k+1}}$ (for instance, we could apply $B_0$, which is the function $x\mapsto x+1$).
\begin{claim} 
Let $u\geq n$ and let $\alpha$ be greatest such that $B_\alpha(u) \leq m$. Then, $N\alpha \leq u$.
\end{claim} 
\proof
Suppose otherwise that $u < N\alpha$. Observe that there is an ordinal $\alpha'$ such that $\alpha < \alpha'$ and $N\alpha'\leq u$.
Otherwise letting
\[\beta_0 = \arg\max_\beta\{B_\beta B_\beta(u) : N\beta\leq u\},\]
we have ${\beta_0} < \alpha$, so that if $\alpha' > \alpha$ is arbitrary, then
\[B_{\alpha'}(u) = B_D(u) = B_\alpha(u) \leq m,\]
contradicting the choice of $\alpha$. We conclude that there is an ordinal $\alpha'$ such that $\alpha < \alpha'$ and $N\alpha'\leq u$.

Let $\alpha'$ be the least such ordinal, so that  whenever $\alpha\leq \gamma <\alpha'$, we have $u < N\gamma$. Hence, we have
\begin{align*}
B_\alpha(u)
&=\max\{B_\beta(B_\beta(u)) : \beta < \alpha\wedge N\beta\leq u\} \cup \{u+1\}\\
&=\max\{B_\beta(B_\beta(u)) : \beta < \alpha'\wedge N\beta\leq u\} \cup \{u+1\}\\
& = B_{\alpha'}(u),
\end{align*}
contradicting the maximality of $\alpha$. This proves the claim.
\endproof
\noindent Now, for each $i < k$,
\[B_{\alpha_{i+1}}\dots B_{\alpha_1}(n) \leq m\]
and $\alpha_{i+1}$ was chosen maximal. Applying the claim shows that
\[N\alpha_{i+1} \leq B_{\alpha_{i}}\dots B_{\alpha_1}(n),\]
so that the expression 
\[B_{\alpha_{k}}\dots B_{\alpha_1}(n)\]
is indeed an $n$-normal form term for $m$, as desired. This proves the lemma.
\endproof


\subsection{Action of $B_D$ on finite embeddings} \label{SectFGHf}
\fi

\begin{definition}\label{DefinitionBDf}
Let $f:n \to n'$ be a strictly increasing function. We define the function $B_D(f):B_D(n) \to B_D(n')$ to be the unique strictly increasing function such that
\begin{enumerate}
\item\label{funct_def_1} if $m<n$, then $B_D(f)(m) = f(m)$;
\item\label{funct_def_2} if $n\le m<B_D(n)$ and $m \stackrel{NF}{=} B_{\alpha_{k}}\dots B_{\alpha_1}(n)$, then
\[B_D(f)(m)=B_{\alpha'_{k}}\dots B_{\alpha'_1}(n'),\]
where $\alpha'_i=D(B_D(f))(\alpha_i)$ for each $i$.
\end{enumerate}
\end{definition}

\begin{lemma}[$\aca$]
Let $f:n \to n'$ be a strictly increasing function. Then, there is a unique strictly increasing function satisfying Definition \ref{DefinitionBDf}.
\end{lemma}
\proof 
By induction on $s\leq B_D(n)$,  we define a sequence of strictly increasing maps
\[g_s: s \to B_D(n')\]
such that $g_{s+1}$ extends $g_s$ for each $s$. 
The map $g_0\colon 0 \to B_D(n')$ is simply the empty map.

Assume that we already have defined maps $g_0,\ldots,g_s$ and established that they are an increasing family of strictly increasing functions. We define the map \[g_{s+1}\colon (s+1)\to B_D(n')\] 
as follows:
\begin{enumerate}
\item if $m<n$, then we put $g_{m+1}(m)=m$;
\item \label{funct_adef_2} if $n \leq m \stackrel{NF}{=} B_{\alpha_{k}}\dots B_{\alpha_1}(n)$, then we put $g_{s+1}(m)=B_{\alpha'_{k}}\dots B_{\alpha'_1}(n')$, where  $\alpha'_{i}=D(g_s)(\alpha_{i})$ for each $i$.
\end{enumerate}
Note that in the second clause the values $D(g_s)(\alpha_i)$ are well-defined. This is because, by the condition on $n$-normal forms, we have 
\begin{equation}\label{eqNalphai<s}
N\alpha_i\le B_{\alpha_{i-1}}\dots B_{\alpha_1}(n')<m\le s,
\end{equation}
and hence $\alpha_i\in D(s)$. 

Let us check that the expression $g_{s+1}(m)$ in \eqref{funct_adef_2} is an $n$-normal form. The fact that $\alpha'_k<_{D(\omega)}\ldots<_{D(\omega)}\alpha'_1$ simply follows from the functoriality of $D$. We show that $N \alpha_i'\le B_{\alpha'_{i-1}}\dots B_{\alpha'_1}(n')$. By definition,
$\alpha'_i=D(g_s)(\alpha_i)$.
Thus, $\alpha'_i$ is the value a $D$-term where all the constants result from shifting constants ${\leq}N\alpha_i$ according to $g_s$. Hence, $\alpha'_i$ is the value of a $D$-term with constants $\leq{g_s(N\alpha_i)}$. In other words,
 $D(g_s)(\alpha_i) \in D(g_s(N\alpha_i))$. By the definition of $N$, it follows that
$$N\alpha'_i\le g_s(N\alpha_i)\le g_s(B_{\alpha_{i-1}}\dots B_{\alpha_1}(n))=B_{\alpha'_{i-1}}\dots B_{\alpha'_1}(n'),$$
as desired.
Hence all the values produced in \eqref{funct_adef_2} are indeed normal forms. 

Now, the comparision algorithm for $n$-normal forms provided by Lemma \ref{normal_forms} implies that $g_{s+1}$ is strictly increasing. If $s=0$, then $g_{s+1}$ extends $g_{s}$ simply because $g_0$ is the empty map. If $s>0$ then we immediately obtain that $g_{s+1}$ extends $g_s$ from their definitions and the fact that $g_{s}$ extends $g_{s-1}$.

Consider 
\[g\colon B_D(n)\to B_D(n')\]
given by
\[g=\bigcup\limits_{m\le B_D(n)}g_m.\]
From the definition, it is clear that $g$ satisfies properties \eqref{funct_def_1} and \eqref{funct_def_2} of the definition of $B_D(f)$. By a straightforward induction on $m$ we show that if 
\[g'\colon B_D(n)\to B_D(n')\] 
is any other function satisfying properties \eqref{funct_def_1} and \eqref{funct_def_2} of the definition of $B_D(f)$, then $g(m)=g'(m)$. Therefore, the definition of $B_D(f)$ indeed defines a unique strictly increasing function.
\endproof

\iffalse

Formally, $\alpha_1$ is an ordinal term of norm ${\leq}n$ in the sense of $D$, so it is an expression of the form 
\[t(x_1, \hdots, x_{k_1}),\]
where each $x_i$ is a parameter ${<}n$ for each $i$. Since $D$ is a functor, $D(f)$ is a function which maps ordinal terms of norm ${\leq} n$ to ordinal terms of norm ${\leq} n'$. Thus, we can set $\alpha'_1 = D(f)(\alpha_1)$. The ordinal $\alpha_{i+1}'$ is described by induction on $i$. Formally, $\alpha_{i+1}$ is an ordinal term of norm ${\leq} B_{\alpha_i}\dots B_{\alpha_1}(n)$, so it is an expression of the form 
\[t(x_1, \hdots, x_{k_i}),\]
where $x_j$ is a parameter ${<} B_{\alpha_i}\dots B_{\alpha_1}(n)$ for each $j$. By induction, $B_D(f)(x_j)$ has been defined, and we define $\alpha'_{i+1}$ to be the term
\[t(B_D(f)(x_1), \hdots, B_D(f)(x_{k_i})).\]
This completes the definition of $B_D(f)(m)$. Let use abuse notation by denoting the mapping 
\[\alpha\mapsto \alpha'\]
just described by $D(f)$ (formally, it is a proper extension of $D(f)$). 

\begin{lemma} \label{LemmaStrictlyIncreasing}
The extended mapping $D(f)$ just defined is strictly increasing on ordinals.
\end{lemma}
\proof
Another way of describing this extension of $D(f)$ is as follows: given a term
\[t(x_1, \hdots, x_{k}),\]
for an ordinal $\alpha$,
first represent each $x_i$ as the value of a term
\[t_i(x^i_1, \hdots, x^i_{k_i}).\]
Then, represent each $x^i_j$ as the value of a term depending on numbers $x^{i,j}_p$, and so on. The definition of an $n$-normal form (in particular, the restriction on the possible norms of ordinals appearing in them) guarantees that 
if the initial term $t(x_1, \hdots, x_{k})$ appeared as part of an $n$-normal form, then this procedure terminates after finitely many stages and produces a deep term
\[\hat t(y_1, \hdots, y_l)\]
depending only on numbers $y_p < n$. The action of $D(f)$ on $\alpha$ is just the result of replacing each $y_p$ by $f(y_p)$. From this description and the fact that $D$ is a functor it is easily seen by induction on the depth of $\hat t$ that $D(f)$ is strictly increasing.
\endproof

\begin{lemma}
Let $f$, $m$, and $B_D(f)(m)$ be as above. Then, the expression 
\[B_D(f)(m) = B_{\alpha'_{k}}\dots B_{\alpha'_1}(n')\]
is an $n'$-normal form term.
\end{lemma}
\proof
This is immediate from the fact that $D$ is a functor.
\endproof

\begin{lemma} \label{LemmaFDFunctorNatural}
$B_D$ is a functor on the category $\mathsf{Nat}$.
\end{lemma}
\proof
The only part of the lemma which requires an argument is showing that $B_D(f)$ is strictly increasing. 
Suppose we are given $m, m' < B_D(n)$ and two $n$-normal form terms
\[m = B_{\alpha_k}\dots B_{\alpha_1}(n)\] and
\[m' = B_{\beta_l}\dots B_{\beta_1}(n).\]
By the previous lemma, $B_D(f)(m)$ and $B_D(f)(m')$ are given by $n'$-normal forms, say 
\[B_{\alpha'_{k}}\dots B_{\alpha'_1}(n') \text{ and } B_{\beta'_{l}}\dots B_{\beta'_1}(n').\] 
By Lemma \ref{LemmaLexicographic}, the ordering between these two $n'$-normal form terms is given by the lexicographic comparison of the ordinals.  By Lemma \ref{LemmaStrictlyIncreasing}, this depends only on the relative ordering of the ordinals $\alpha_1, \hdots, \alpha_k$, $\beta_1, \hdots, \beta_l$. Again by Lemma \ref{LemmaLexicographic}, this completely determines the ordering between $m$ and $m'$, as needed.
\endproof
\fi

\begin{corollary} \label{CorollaryFDFunctorNatural}
$B_D$ is a functor on the category $\mathsf{Nat}$.
\end{corollary}



Commenting on an earlier draft of this article, Wainer has brought to our attention an earlier result of his \cite{Wa99} in which he establishes functoriality for a version of the binary fast-growing hierarchy in the context of tree-ordinals.

\section{Fast-growing hierarchies as ordinal collapses}\label{SectCollapse}
In this section, we give an alternate definition of $B_D$ in terms of formal ``ordinal collapses'' which will directly result in a $\subseteq$-preserving dilator. 
We will show that the new construction, as a functor, is naturally isomorphic to the one constructed in the previous section. 
It will be clear from the construction that this definition coincides with the previous one when $A$ is a natural number with the usual ordering. 
As a consequence of this and Corollary \ref{CorollaryFDFunctorNatural}, it follows that the new definition coincides with the previous one for arbitrary linear orderings $A$. Again, all the constructions will be formalizable in $\mathsf{ACA}_0$.

Recall that for a linear order $A$, $2^A$ is the linear order consisting of formal base-$2$ Cantor normal forms \[2^{a_1}+\ldots+2^{a_n}\] 
with $a_1>_A\ldots>_Aa_n$. These formal sums are compared in the natural way, i.e., 
$2^{a_1}+\ldots+2^{a_n}<_{2^A}2^{b_1}+\ldots+2^{b_m}$ if $(a_1,\ldots,a_n)<_{\mathsf{lex}}(b_1,\ldots,b_m)$. Here, the empty sum is allowed and identified with the term $0$.
This construction naturally extends to a dilator: given a strictly increasing  function $f\colon A\to B$, we define
\begin{align*}
2^f\colon 2^A &\to 2^B\\
2^f\colon 2^{a_1}+\ldots+2^{a_n}&\mapsto 2^{f(a_1)}+\ldots+2^{f(a_n)}.
\end{align*}

Below, if $A$ is a linear ordering and $a \in A$, we denote by $A\upharpoonright a$ the initial segment $\{x\in A: x<a\}$, viewed as a linear order.
\begin{definition}
Let $A$ be a linear ordering. $B_D(A)$ is defined to be the \mbox{(inclusion-)least} linear ordering $C$ such that the following hold:
\begin{enumerate}
\item $C$ contains the term $a^\star$, for any $a\in A$.
\item $C$ contains the term $\psi(0)$.
\item Suppose that:
\begin{enumerate}
\item $\alpha_1,\ldots,\alpha_k,\alpha_{k+1}\in D(C)$,
\item $\psi(2^{\alpha_1}+\ldots+2^{\alpha_k})\in C$,
\item $\alpha_{k+1}<_{D(C)}\alpha_k$, and 
\item $\alpha_{k+1}\in D(C\upharpoonright\psi(2^{\alpha_1}+\ldots+2^{\alpha_k}))$;
\end{enumerate}
 then   $\psi(2^{\alpha_1}+\ldots+2^{\alpha_k}+2^{\alpha_{k+1}})\in C$.
\item if $a<_Ab$, then $a^{\star}<_Cb^\star$.
\item $a^\star<_C\psi(t)$, for any  $a^\star,\psi(t)\in C$.
\item if $\psi(t), \psi(u)\in C$, $t,u\in 2^{D(C)}$, and $t<_{2^{D(C)}}u$, then  $\psi(t)<_C\psi(u)$.
\end{enumerate}
\end{definition}

\begin{lemma}[$\aca$]
Suppose $D$ is a dilator and $A$ is a linear ordering. Then, $B_D(A)$ exists.
\end{lemma}
\proof
The idea is to construct $B_D(A)$ as the limit of an inductive definition of length $\omega$.
We construct linear orders 
\[B_{D,0}(A)\subseteq B_{D,1}(A)\subseteq \ldots \subseteq B_{D,n}(A)\subseteq\ldots\]
Recursively,we denote by $B_{D,<n}(A)$ the already defined linear order $\bigcup\limits_{m<n}B_{D,m}(A)$ and define $B_{D,n}(A)$ to contain the following terms:
\begin{enumerate}  
\item $a^\star$, for $a\in A$;
\item $\psi(0)$;
\item $\psi(2^{\alpha_1}+\ldots+2^{\alpha_k}+2^{\alpha_{k+1}})$, whenever $\alpha_1,\ldots,\alpha_k,\alpha_{k+1}\in D(B_{D,<n}(A))$ are such that:
\begin{enumerate}
\item $\psi(2^{\alpha_1}+\ldots+2^{\alpha_k})\in B_{D,<n}(A)$, 
\item $\alpha_{k+1}<_{D(B_{D,<n}(A))}\alpha_k$, and 
\item $\alpha_{k+1}\in D( B_{D,<n}(A){\upharpoonright} \psi(2^{\alpha_1}+\ldots+2^{\alpha_k}))$.
\end{enumerate}
\end{enumerate}
The order on these terms is defined in the same way as above, i.e., $a^\star<_{B_{D,<n}(A)}b^\star$ if and only if $a<_Ab$; we always have $a^\star<_{B_{D,<n}(A)}\psi(t)$; and $\psi(t)<_{B_{D,n}(A)}\psi(u)$ if and only if $t<_{2^{D(B)}}u$. It is straightforward to check that, provably in $\mathsf{ACA}_0$, the order $B_D(A)$ constructed as the union of the chain $\{B_{D, <n}(A):n\in\mathbb{N}\}$ satisfies the definition of $B_D(A)$, for any linear ordering $A$.
\endproof

\begin{definition}
Let $A$ and $A'$ be linear orders and $f: A\to A'$ be a morphism. We define
\[B_D(f): B_D(A)\to B_D(A')\] 
to be the unique map $g\colon B_D(A)\to B_D(B)$ such that:
\begin{enumerate}
\item $g(a^{\star}) = (f(a))^{\star}$, and
\item $g(\psi(t))=\psi(2^{D(g)}(t))$.
\end{enumerate}
\end{definition}

\begin{lemma}[$\aca$]
Suppose that $A$ and $A'$ are linear orders and $f:A \to A'$ is a morphism. Then, $B_D(f)$ exists.
\end{lemma}
\proof
This is similar to the previous proof. By induction, we define a sequence of embeddings 
$B_{D,n}(f)\colon B_{D,n}(A)\to B_{D,n}(B)$. Letting
\[B_{D,<n}(f)=\bigcup_{m<n} B_{D,m}(f)\colon B_{D,<n}(A)\to B_{D,<n}(B),\] 
we put:
\begin{enumerate}
\item $B_{D,n}(f)(a^{\star}) = (f(a))^{\star}$, and
\item $B_{D,n}(f)(\psi(t))=\psi(2^{D(B_{D,<n}(f))}(t))$.
\end{enumerate}
Clearly, $B_{D,<\omega}(f)$ satisfies the definition of $B_D(f)$. By induction on $n$, one shows that for  any $g\colon B_D(A)\to B_D(B)$ satisfying the definition of $B_D(f)$ we have 
\[g{\upharpoonright} B_{D,n}(A)=B_{D,n}(f).\] 
Thus indeed there is a unique mapping satisfying the definition of $B_D(f)$.
\endproof




\begin{lemma}[$\mathsf{ACA}_0$]\label{LemmaPullbacks}
Suppose $D$ is a $\subseteq$-preserving pre-dilator. Then, so too is $B_D$. 
\end{lemma}
\proof
The functoriality and $\subseteq$-preservation of $B_D$ are immediate from the definition. In order to check that $B_D$ is finitary it is enough to show that for any $A$ we have 
\[B_D(A)=\bigcup\limits_{A'\subseteq_{\mathsf{fin}}A}B_D(A').\] 
This is done by showing, via a straightforward induction on $n$, that
\[B_{D,n}(A)=\bigcup\limits_{A'\subseteq_{\mathsf{fin}}A}B_{D,n}(A').\] 
By a straightforward induction on $n$ we also show that for any order $A$ and any suborders $A',A''$ of $A$, we have 
\[B_{D,n}(A')\cap B_{D,n}(A'')=B_{D,n}(A'\cap A'').\] 
This implies that for any order $A$ and its suborders $A',A''$ we have 
\[B_{D}(A')\cap B_{D}(A'')=B_{D}(A'\cap A''),\]
i.e., that $B_D$ preserves pullbacks. This concludes the proof that $B_D$  is a $\subseteq$-preserving pre-dilator.
\endproof


For an arbitrary pre-dilator $D$,  we may define the pre-dilator $B_D$ to be $B_{D'}$, where $D'$ is some fixed $\subseteq$-preserving pre-dilator naturally isomorphic to $D$. 

\begin{lemma}[$\mathsf{ACA}_0$]\label{EquivalenceOfDefinitions} 
Suppose $D$ is a weakly finite dilator. Let $B_D$ be the functor defined in this section and $\hat B_D$ be the functor defined in Section \ref{SectFunctor}. Then, $B_D$ and $\hat B_D$ are naturally isomorphic.
\end{lemma}
\proof
Let $\theta\colon D\to D'$ be the natural isomorphism given by the definition of $B_D$ for arbitrary pre-dilators $D$.
For each $n\in\mathbb{N}$, let 
\[\eta_n: \hat B_D(n) \to B_D(n)\] 
be the function given by:
\begin{align*}
m &\mapsto m^\star, &\text{ if $m < n$,}\\
B_{\alpha_k}\dots B_{\alpha_1}(n) &\mapsto \psi(2^{\alpha_1'} + \dots + 2^{\alpha_k'}),\text{ where }\alpha_i'=\theta_{B_D(n)}(\alpha_i), &\text{ otherwise.}
\end{align*}
It is clear that the collection of $\eta_n$ for $n\in\mathbb{N}$ forms a natural isomorphism between $\hat B_D\colon \Nat\to \LO$ to $B_D\upharpoonright \Nat$, the restriction of $B_D$ to the category $\Nat$. 
Since both $\hat B_D$ and $B_D$ are finitary, this natural transformation extends to a natural isomorphism between the extension of $\hat B_D$ to $\LO$ and $B_D$, as desired.
\endproof


\begin{remark} We note, without giving details, that in fact the operation 
\[D\longmapsto B_D\]
 could be extended to a pullback-preserving functor on the category of pre-dilators; in other words, $B$ is a \emph{preptyx} and -- as we will see in the next section -- indeed it is a \emph{ptyx}. Furthermore, if we treat the category of pre-dilators as a category of structures (denotation systems can be regarded as structures), then in fact the definition of $B$ in terms of formal ``ordinal collapses'' will be a $\subseteq$-preserving functor. 
\end{remark}


\begin{remark} The construction of $B_D(A)$ in fact works for all $\subseteq$-preserving finitary functors $D\colon \LO\to \LO$. We decided not to cover the extension to finitary functors in this paper for the following reason: The fact that any dilator is naturally isomorphic to a $\subseteq$-preserving one is a known fact following from Girard's fundamental theorem of dilators. 
There is an unpublished result by the second author that establishes an analog of Girard's theorem for finitary functors on $\LO$ that in particularly implies that any finitary functor on $\LO$ is naturally isomorphic to a $\subseteq$-preserving one. 
This result shall appear in a forthcoming article by the second and third authors. 
\end{remark}

In order to make sense of $B_D$ in the case when $D$ is not $\subseteq$-preserving, it suffices to choose a denotation system $D'$ and put $B_{D}=B_{D'}$.


\section{Proof of the theorem}\label{SectTheorem}
In this section we prove the main theorem. We restate it, for convenience.

\begin{theorem}\label{MainRestated}
The following are equivalent over $\aca$:
\begin{enumerate}
\item \label{MainRestated1} $\Pi^1_1$-$\ca$;
\item \label{MainRestated4}for every weakly finite dilator $D$, $B_D$ is a weakly finite dilator;
\item \label{MainRestated3} for every dilator $D$, $B_D$ is a dilator.
\end{enumerate}
\end{theorem}
\begin{lemma}[$\Pi^1_1$-$\ca$] \label{LemmaPi11CA}
For any dilator $D$ and any wellordering  $A$, $B_D(A)$ is wellordered.
\end{lemma}
\proof
By the definition of $B_D$, it suffices to consider the case that $D$ is $\subseteq$-preserving.

Let $\Omega$ be the largest wellordered initial segment of $B_D(A)$. This exists by \mbox{$\Pi^1_1$-$\ca$}.  By hypothesis, $D$ is a dilator, so $D(\Omega)$ is wellordered. 
By induction on ordinals 
$\alpha \in D(\Omega)$,  we show that for every $\psi(2^{\alpha_1} + \dots + 2^{\alpha_k}) \in \Omega$, if $\psi(2^{\alpha_1} + \dots + 2^{\alpha_k} + 2^\alpha) \in B_D(A)$, then 
\[a := \psi(2^{\alpha_1} + \dots + 2^{\alpha_k} + 2^\alpha) \in \Omega.\]
Suppose that $x <_{B_D(A)} a$. Then, either
\[x \leq \psi(2^{\alpha_1} + \dots + 2^{\alpha_k})\]
or else there are $l\in\mathbb{N}$ and $\beta_1, \hdots, \beta_l$ with $\beta_l <_{D(B_D(A))} \dots <_{D(B_D(A))} \beta_1 < \alpha$ such that
\[x \leq \psi(2^{\alpha_1} + \dots + 2^{\alpha_k} + 2^{\beta_1} + \dots + 2^{\beta_l}).\]
We show by induction on $i < l$ that 
\begin{enumerate}
\item $\beta_i \in D(\Omega)$,  and
\item $\psi(2^{\alpha_1} + \dots + 2^{\alpha_k} + 2^{\beta_1} + \dots + 2^{\beta_i}) \in \Omega$.
\end{enumerate}
By the definition of $B_D$,  we have
\[\beta_{i+1} \in D(B_D(A)\upharpoonright \psi(2^{\alpha_1} + \dots + 2^{\alpha_k} + 2^{\beta_1} + \dots + 2^{\beta_i})).\]
By the induction hypothesis on $i$,  $\psi(2^{\alpha_1} + \dots + 2^{\alpha_k} + 2^{\beta_1} + \dots + 2^{\beta_i}) \in \Omega$ (this is immediate by the assumption on $\alpha_1, \ldots, \alpha_k$ in the case $i =0$) and $\Omega$ is an initial segment of $B_D(A)$,  so the first claim follows.  The second follows from the induction hypothesis on $\alpha$.
We have shown that every element $x <_{B_D(A)} a$ belongs to $\Omega$ and thus
 $a \in \Omega$, as desired.

By a straightforward induction on $k$, it follows that
\[\psi(2^{\alpha_1} + \dots + 2^{\alpha_k}) \in \Omega\]
for all $\psi(2^{\alpha_1} + \dots + 2^{\alpha_k}) \in B_D(A)$, i.e., that $B_D(A) = \Omega$ and thus $B_D(A)$ is wellordered.
\endproof

\begin{lemma}[$\aca$]\label{LemmaWeaklyFinite}
Suppose that for every weakly finite dilator $D$, $B_D$ is a weakly finite dilator. Then, for every dilator $D$, $B_D$ is a dilator.
\end{lemma}
\proof
If $D$ and $D'$ are naturally isomorphic pre-dilators, then so too are $B_D$ and $B_{D'}$. Hence, it suffices to prove the theorem for denotation systems $D$. 
Let $D$ be a denotation system and enumerate all ordinal terms of $D$ by $d_0, d_1, \hdots$; write $n_i$ for the arity of $d_i$. We define a new dilator $\hat D$ consisting of terms $\hat d_i$ of arity $n_i+i$. Clearly, $\hat D$ will be weakly finite. The comparison rules for $
\hat D$ are given by
\[\hat d_i (x_1, \hdots, x_{n_i}, \hat x_1, \hdots, \hat x_i) <_{\hat D} \hat d_j (y_1, \hdots, y_{n_j}, \hat y_1, \hdots, \hat y_j)\]
if and only if one of the following holds:
\begin{enumerate}
\item $d_i(x_1,\hdots, x_{n_i}) <_{D} d_j(y_1,\hdots, y_{n_j})$; or else
\item $i = j, x_1 = y_1, \hdots, x_{n_i} = y_{n_i}$, and $(\hat x_1, \hdots, \hat x_i) <_{lex} (\hat y_1,\hdots, \hat y_j)$.
\end{enumerate}
It is easy to check that $<_{\hat D}$ is a linear order. And it is easy to see that for any $A$, we have an embedding of $\hat D (A)$ into $2^{A}\cdot D(A)$: 
$$\hat d_i(a_1,\ldots,a_{n_i}, b_1,\ldots,b_i)\longmapsto 2^A \cdot d_i(a_1,\ldots,a_{n_i}) + 2^{b_1}+\ldots+2^{b_i}.$$ Thus $\hat D$ is a dilator. Observe that for each finite order $A$, the order $\hat D(A)$ contains only terms of the form $\hat d_i(\ldots)$, where $i\le |A|$ and hence $\hat D(A)$ is finite. Therefore $\hat D$ is a weakly finite dilator. Thus $B_{\hat D}$ is a dilator.

In order to show that $B_D$ preserves wellfoundedness it is enough to find a strictly increasing map 
\[e\colon B_D(A)\to B_{\hat D}(\omega+A)\] 
for an arbitrary wellorder $A$. We fix a wellorder $A$ and define, by recursion on $n$, 
\[e_n: B_{D,n}(A) \to B_{\hat D,n}(\omega+A)\]
\begin{enumerate}
\item $e_n(a^\star)=(\omega+a)^\star$;
\item $e_n(\psi(2^{\alpha_1}+\ldots +2^{\alpha_k}))=\psi(2^{\alpha_1'}+\ldots +2^{\alpha_k'})$, where if $\alpha_i=d_j(a_{1},\ldots,a_{n_{j}})$, then $\alpha_i'=\hat d_{j}(e_{n-1}(a_{1}),\ldots,e_{n-1}(a_{n_j}), (j-1)^\star, \ldots, 0^\star)$.\end{enumerate}
By a straightforward induction on $n$ we show that $e_n$'s form a sequence of expanding strictly increasing maps. We finish the proof by defining $e=\bigcup\limits_{n<\omega} e_n$.
\endproof

In order to complete the proof, we have to show that if $B_D$ is a dilator for every dilator $D$, then $\Pi^1_1$-$\ca$ holds. This will be done by appealing to a theorem of Freund \cite{Fr19} whereby $\Pi^1_1$-$\ca$ is equivalent to a higher order fixed-point principle. 
Using the terminology of Freund \cite{Fr19}, this is the statement that every dilator $D$ has a wellfounded Bachmann-Howard fixed point (we recall this definition during the course of the forthcoming proof).

\begin{lemma}[$\aca$]\label{LemmaBachmannHoward}
Suppose that $B_D$ is a dilator for every dilator $D$. Then, every dilator has a wellfounded Bachmann-Howard fixed point.
\end{lemma}
\proof
It suffices to restrict to the case where $D$ is a denotation system and, in particular, $\subseteq$-preserving.
We need to find a wellordering $A$ and a function 
\[\theta:D(A)\to A\]
such that the following hold:
\begin{enumerate}
\item \label{PropBHF1} whenever we have $\alpha<_{D(A)}\beta$ and $\supp(\alpha)<_A \theta(\beta)$, then we have \mbox{$\theta(\alpha) <_A \theta(\beta)$}; and
\item \label{PropBHF2}  $\supp(\alpha) <_A \theta(\alpha)$ for every $\alpha \in D(A)$.
\end{enumerate}

Consider the dilator $F=(\omega+1)D +\omega$. This is defined as follows: Given a linear order $B$, the order $F(B)$ consists of terms of two types:
\begin{enumerate}
\item $(\omega+1)\alpha+a$, where $\alpha\in D(B)$ and $a\le \omega$;
\item $\Lambda+n$, where $n<\omega$.
\end{enumerate}
The terms are compared according to the following rules:
\begin{enumerate}
\item terms of the first type are always smaller than the terms of the second type;
\item $(\omega+1)\alpha+a$ is smaller than $(\omega+1)\beta+b$ if and only if either $\alpha<\beta$ or $\alpha=\beta$ and $a<b$;
\item $\Lambda+n$ is smaller than $\Lambda+m$ if and only if $n<m$.
\end{enumerate}
For a strictly increasing function $f\colon B\to C$ we put 
\begin{align*}
F(f):F(B) &\to F(C)\\ 
(\omega+1)\alpha+a &\mapsto (\omega+1)(D(f)(\alpha))+a;\\
\Lambda + n &\mapsto \Lambda + n.
\end{align*}
It is easy to see that $F$ is indeed a dilator.

We put $A=B_{F}(0)$. Note that all elements of $A$ are of the form $\psi(2^{\alpha_1}+\ldots+2^{\alpha_n})$, where $\alpha_i\in F(A)$. We define 
\[\theta\colon D(A)\to A\] 
to be the function that maps $\alpha\in D(A)$ to the least element of $A$ of the form 
\[\psi(2^{\alpha_1}+\ldots+2^{\alpha_n}+2^{(\omega+1)\alpha+\omega}).\] 
This function is well defined, i.e., for any $\alpha\in D(A)$ there is some element of $A$ as above.
Indeed, the elements of the form $\psi(2^{\Lambda+n})$ are cofinal in $A$. 
Thus, for any $\alpha\in D(A)$ one can find $n$ large enough so that $\alpha\in D(A{\upharpoonright}\psi(2^{\Lambda+n}))$  and hence 
\[\psi(2^{\Lambda+n}+2^{(\omega+1)\alpha+\omega})\in A.\]

Let us verify that $\theta$ satisfies property \eqref{PropBHF1}: we suppose $\alpha<_{D(A)}\beta$ and $\supp(\alpha)<_A \theta(\beta)$ and claim that $\theta(\alpha) <_A \theta(\beta)$. Let $\beta_1$, $\hdots$, $\beta_n$ be such that
\[\theta(\beta) = \psi(2^{\beta_1}+\ldots+2^{\beta_n}+2^{(\omega+1)\beta+\omega}).\] 
Observe that all elements of the form 
\[\psi(2^{\beta_1}+\ldots+2^{\beta_n}+2^{(\omega+1)\beta+m})\] 
are in $A$ and are cofinal below $\theta(\beta)$. It follows that, since 
\[\supp(\alpha) = \supp((\omega+1)\alpha+\omega)\]
is a finite set, we can find $m\in\mathbb{N}$ large enough so that 
\[\supp(\alpha)<_A\psi(2^{\beta_1}+\ldots+2^{\beta_n}+2^{(\omega+1)\beta+m}).\] 
For such an $m$, $\psi(2^{\beta_1}+\ldots+2^{\beta_n}+2^{(\omega+1)\beta+m}+2^{(\omega+1)\alpha+\omega})$ is in $A$. Therefore
\begin{align*}
\theta(\alpha)
&\le \psi(2^{\beta_1}+\ldots+2^{\beta_n}+2^{(\omega+1)\beta+m}+2^{(\omega+1)\alpha+\omega})\\
&<\psi(2^{\beta_1}+\ldots+2^{\beta_n}+2^{(\omega+1)\beta+\omega})\\
&=\theta(\beta).
\end{align*}

The fact that $\theta$ satisfies \eqref{PropBHF2} is immediate from the construction. Indeed, for any $\alpha\in D(A)$, the value $\theta(\alpha)$ is of the form $\psi(2^{\alpha_1}+\ldots+2^{\alpha_n}+2^{(\omega+1)\alpha+\omega})\in A$ and we have $$\supp(\alpha)=\supp((\omega+1)\alpha+\omega)<_A\psi(2^{\alpha_1}+\ldots+2^{\alpha_n})<_A\theta(\alpha),$$
as desired.
\endproof

\iffalse
Let $D$ be a dilator. We need to find a wellordering $A$ and a function 
\[\theta:D(A)\to A\]
such that the following hold:
\begin{enumerate}
\item whenever we have $\alpha<_{D(A)}\beta$ and $\supp(\alpha)<_A \theta(\beta)$, then we have $\theta(\alpha) <_A \theta(\beta)$; and
\item $\supp(\alpha) <_A \theta(\alpha)$ for every $\alpha \in D(A)$.
\end{enumerate}
This will be done by considering three cases.\\

\noindent \paragraph{\textsc{Case I}} 
$D$ contains no constant terms. Then, $D$ is continuous on $\WO$. Let 
\[A = \sum_{n\in\mathbb{N}} D^n(A)\]
so that $D(A)$ is isomorphic to $A$ and let $\theta$ be the canonical order-preserving injection. Then $\theta$ is as required.\\

\noindent \paragraph{\textsc{Case II}} Every non-constant term is dominated by a constant term.
We define the dilator $(\omega+1)D$ as follows.  Given a linear order $A$, $(\omega+1)D(A)$ consists of pairs $(\alpha, a)$ where $a\leq\omega$ and the pair is interpreted as the sum
\[(\alpha,a) = (\omega+1) \cdot\alpha + a,\]
with the obvious ordering.
Let $A = B_{(\omega+1)D}(0)$; thus, elements of $A$ are ordinals of the form 
\begin{equation}\label{eqFormA}
a = \psi(\alpha_1 + \dots + \alpha_k)
\end{equation}
where $\alpha_1$ is of the form
\begin{equation}\label{eqFormA1}
2^{(\omega+1)\cdot \gamma_1 + n_1}
\end{equation}
for some constant term $\gamma_1$ from $D$ and some $n_1\leq\omega$; $\alpha_2$ is of the form $2^{(\omega+1)\cdot \gamma_2 + n_2}$ for some $\gamma_2$ which is either a constant term, or a non-constant term with support ${<}\gamma_1$; etc.
\begin{claim}\label{ClaimNoLargestElement}
$A$ has no largest element.
\end{claim}
\proof
For $a \in A$ of the form \eqref{eqFormA}, with $\alpha_1$ of the form \eqref{eqFormA1}, if there is a constant term $\gamma$ in $D$ such that $\gamma_1<\gamma$, then
\[a < \psi(2^{(\omega+1)\cdot \gamma}).\]
Otherwise, if $\gamma_1$ is the largest constant term in $D$, then either $n_1\in\mathbb{N}$, in which case 
\[a < \psi(2^{(\omega+1)\cdot\gamma_1 + n_1+1}),\]
or else $n_1 = \omega$. If so, then $\supp(\gamma_1) = 0 < \psi(2^{(\omega+1))\cdot\gamma+\omega})$, so that
\[\psi(2^{(\omega+1)\cdot\gamma_1+\omega} + 2^{(\omega+1)\cdot\gamma_1+n}),\]
is a valid term for each $n\in\mathbb{N}$. Since any element of $A$ (in particular, $a$) of the form \eqref{eqFormA} where $\alpha_1 = 2^{(\omega+1)\cdot\gamma_1+\omega}$ must satisfy $
\alpha_2 < (\omega+1)\cdot\gamma$, we can find some $n\in\mathbb{N}$ such that
\[a < \psi(2^{(\omega+1)\cdot\gamma_1+\omega} + 2^{(\omega+1)\cdot\gamma_1+n}),\]
as desired.
\endproof
While $A$ has no largest element, $D(A)$ might have one. If so, however, it must be denoted by a constant term, by the case hypothesis.
\begin{claim}\label{ClaimEligibleTerm}
Let $\alpha \in D(A)$. Then, either $\alpha$ is the largest element of $D(A)$ and is denoted by a constant term, or else
there is $a\in A$, say,
\[a = \psi(2^{(\omega+1)\cdot\alpha_1 + n_1} + \dots + 2^{(\omega+1)\cdot\alpha_k + n_k}),\]
such that
\begin{enumerate}
\item $\supp(\alpha) <_A a$,
\item $\alpha <_{D(A)} \alpha_k$.
\end{enumerate}
\end{claim}
\proof
Suppose that $\alpha$ is not the largest element of $D(A)$.
Let $a$ be obtained by applying Claim \ref{ClaimNoLargestElement} to the largest element of $\supp(\alpha)$.
By the case hypothesis, there is a constant term in $D$ which dominates all the non-constant terms appearing in the denotation for $\alpha$, so it is clear from the construction of $a$ that the second condition of the claim is satisfied.
\endproof

\begin{claim}\label{ClaimTheta}
Suppose $\alpha\in D(A)$. Then, there is some $b \in A$ of the form
\begin{equation}\label{eqClaimTheta}
b = \psi(2^{(\omega+1)\cdot \beta_1+m_1} + \dots + 2^{(\omega+1)\cdot \beta_l + m_1} + 2^{(\omega+1)\cdot\alpha + \omega}).
\end{equation}
\end{claim}
\proof
This is immediate from Claim \ref{ClaimEligibleTerm}.
\endproof


Now, suppose $\alpha \in D(A)$. 
We define $\theta(\alpha)$ to be the $<_A$-least element of $A$ of the form
\[\psi(2^{(\omega+1)\cdot\alpha_1 + n_1} + 2^{(\omega+1)\cdot\alpha_k + n_k} + 2^{(\omega+1)\cdot\alpha + \omega}),\]
which exists by Claim \ref{ClaimTheta}.

We show that $\theta$ is as required. The condition that
\[\supp(\alpha) < \theta(\alpha)\]
is immediate, since, by construction
\[\supp(\alpha) < \psi(2^{(\omega+1)\cdot\alpha_1 + n_1} +\dots + 2^{(\omega+1)\cdot\alpha_k + n_k} ) < \theta(\alpha).\]
For the other condition, we suppose that $\alpha <_{D(A)} \beta$ and $\supp(\alpha) < \theta(\beta)$. Write 
\[\theta(\beta) = \psi(2^{(\omega+1)\cdot\beta_1 + m_1} + 2^{(\omega+1)\cdot\beta_k + m_k} + 2^{(\omega+1)\cdot\beta + \omega}).\]
The assumption that $\alpha <_{D(A)}\beta$ implies that
\[(\omega+1)\alpha+\omega <_{(\omega+1)D} (\omega+1)\beta+n\]
for every $n$. Together with the assumption that $\supp(\alpha) < \theta(\beta)$, this implies that, for every $n$, the expression
\[\psi(2^{(\omega+1)\cdot\beta_1 + m_1} + 2^{(\omega+1)\cdot\beta_k + m_k} + 2^{(\omega+1)\cdot\beta + n} + 2^{(\omega+1)\cdot\alpha+\omega})\]
is a valid term. However, $\theta(\alpha)$ was defined as the least possible value of a term of the form $\psi(\xi + 2^{(\omega+1)\cdot\alpha+\omega})$, and so it follows that
\begin{align*}
\theta(\alpha) 
& \leq \psi(2^{(\omega+1)\cdot\beta_1 + m_1} + 2^{(\omega+1)\cdot\beta_k + m_k} + 2^{(\omega+1)\cdot\beta + n} + 2^{(\omega+1)\cdot\alpha+\omega})\\
&< \psi(2^{(\omega+1)\cdot\beta_1 + m_1} + 2^{(\omega+1)\cdot\beta_k + m_k} + 2^{(\omega+1)\cdot\beta + \omega})\\
& = \theta(\beta),
\end{align*}
as required.\\


\noindent \paragraph{\textsc{Case III}}  
Otherwise; i.e., $D$ contains both constant and non-constant terms, and there are non-constant terms which dominate every constant term.
We separate $D = D_1 \oplus D_2$, where $D_2$ consists of all non-constant terms which dominate all constant terms. We define $A_1$ and 
\[\theta_1: D_1(A_1) \to A_1\]
as in \textsc{Case II} and we define
$A_2$ and 
\[\theta_2: D_2(A_2) \to A_2\]
as in \textsc{Case I}. Then,
\[\theta := \theta_1 \oplus \theta_2: D(A_1 \oplus A_2) \to A_1 \oplus A_2\]
is as required.
\endproof
\fi

Putting together the lemmata in this section, the proof of Theorem \ref{MainRestated} is now complete. 

\begin{remark}
By appealing to the main theorem of Freund \cite{Fr20} and carefully formalizing the definition of $B_D$ in Section \ref{SectCollapse}, the equivalence in Theorem \ref{MainRestated} can be proved in $\rca$.
\end{remark}



\iffalse
\section{$\subseteq$-preserving finitary functors}
In this section we prove the following result in $\mathsf{ACA}_0$.

\begin{proposition}\label{dilator_tilde} For any finitary functor $F\colon \mathsf{LO}\to\mathsf{LO}$ there is a pre-dilator $\tilde F\colon \mathsf{LO}\to \mathsf{LO}$ such that
\begin{enumerate}
\item there is a natural transformation $\eta^F\colon F \to \tilde F$;
\item if $F$ was wellorder preserving, then $\tilde F$ is a dilator.
\end{enumerate}
\end{proposition}

Befor proving Proposition \ref{dilator_tilde} lets derive from it the corollary that we actually need in the paper. Since by Girard normal form theorem any dilator is isomorphic to a $\subseteq$-preserving functor, without loss of generality we may assume that $\tilde F$ is $\subseteq$-preserving. Using this it is trivial to produce functor $F'\colon \LO\to \LO$ that is $\subseteq$-preserving and naturally isomorphic to $F$, namely for linear orders $A$ we put $F'(A)=\tilde F(A){\upharpoonright}\{\eta^B_A(a)\mid a\in F(A)\}$ and for morphisms $f$ we define $F'(A)$ as the apropriate restriction of $\tilde F(A)$. Thus we have

\begin{corollary} Any finitary functor $F$ is naturally isomorphic to a $\subseteq$-preserving functor.\end{corollary}

Now we prove Proposition \ref{dilator_tilde}
\begin{proof}
  We are going to define a pre-dilator $\tilde F$. For this we define the restriction of $\tilde F$ to $\FO\to \LO$  together with the restriction of a natural transformation $\eta^F\colon F \to \tilde F$. This will automatically extend to $\tilde F$ and $\eta^F$ given than the restriction of $\tilde F$ will be a pullback preserving functor and the restriction of $\eta^F$ will be a natural transformation from the restriction of $F$ to the restriction of $\tilde F$.
  
  Consider some finite linear order $A$. The linear order $A^n=\omega+\omega A$ consist of the following terms with the natural order between them:
  \begin{enumerate}
  \item $n$, for all natural numbers $n$;
  \item $\omega a +n$, 
  \end{enumerate}
  The order $A^e$ is the suborder of $A^n$ consisting just of the following terms:
  \begin{enumerate}
  \item $n$ for even $n$
  \item $\omega a +n$, for all $a\in A$ and even $n$.
  \end{enumerate}
  The order $A^o$ is the  suborder of $A^n$ consisting just of the following terms:
  \begin{enumerate}
  \item $n$ for odd  $n$
  \item $\omega a +n$, for all $a\in A$ and odd $n$;
  \item $\omega a +0$, for all $a\in A$.
  \end{enumerate}
  Let the morphisms $\alpha_A\colon A\to A^o$ and $\beta_A\colon A\to A^e$ simply map each $a\in A$ to $\omega a+0$. And let $\gamma_A\colon A^o\to A^n$ and $\delta_A\colon A^e\to A^n$ simply be the identity maps. Clearly we have the following pull-back diagram:
 \[\begin{tikzcd}
	{A^e} & {A^n} \\
	A & {A^o}
	\arrow["{\delta_A}", from=1-1, to=1-2]
	\arrow["{\beta_A}", from=2-1, to=1-1]
	\arrow["{\gamma_A}"', from=2-2, to=1-2]
	\arrow["{\alpha_A}"', from=2-1, to=2-2]
	\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=90}, draw=none, from=2-1, to=1-2]
   \end{tikzcd}\]
 We (uniquely) extend $(-)^n,(-)^e,(-)^o$ to $\subseteq$-preserving functors from $\mathsf{FO}$ to $\mathsf{LO}$. 
 

 Now we put $\tilde F(A)$ to be the pullback of $F(A^e)\stackrel{F(g_A^e)}{\longrightarrow}F(A^n)$ and $F(A^o)\stackrel{F(g_A^o)}{\longrightarrow}F(A^n)$. Hence we have the following commutative diagrams for all $A$, where we obtain $\eta_A$ by the universal property of the pullback:
 \[\begin{tikzcd}
	& {F(A^e)} & {F(A^n)} \\
	& {\tilde F(A)} & {F(A^o)} \\
	{F(A)}
	\arrow["{F(\delta_A)}", from=1-2, to=1-3]
	\arrow["{\zeta_A}", from=2-2, to=1-2]
	\arrow["{F(\gamma_A)}"', from=2-3, to=1-3]
	\arrow["{\varepsilon_A}"', from=2-2, to=2-3]
	\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=90}, draw=none, from=2-2, to=1-3]
	\arrow["{\eta_A^F}"', dotted, from=3-1, to=2-2]
	\arrow["{F(\beta_A)}", bend left =20, from=3-1, to=1-2]
	\arrow["{F(\alpha_A)}"', bend right =20, from=3-1, to=2-3]
\end{tikzcd}\]

This construction naturally extends to a functor $\tilde F(f)$.  Now by universal property of pullbacks for each $f\colon A\to B$ we define $\tilde(F)(f)$ to be the unique map making the following diagram commutative:
\[\begin{tikzcd}
	&& {F(B^e)} &&& {F(B^n)} \\
	{F(A^e)} &&& {F(A^n)} \\
	\\
	&& {\tilde F(B)} &&& {F(B^o)} \\
	{\tilde F(A)} &&& {F(A^o)}
	\arrow["{F(\delta_A)}", from=2-1, to=2-4]
	\arrow["{\zeta_A}", from=5-1, to=2-1]
	\arrow["{\varepsilon_A}"', from=5-1, to=5-4]
	\arrow["{F(\gamma_A)}"', from=5-4, to=2-4]
	\arrow["{F(\delta_B)}", from=1-3, to=1-6]
	\arrow["{F(\gamma_B)}"', from=4-6, to=1-6]
	\arrow["{\zeta_B}", from=4-3, to=1-3]
	\arrow["{\varepsilon_B}"', from=4-3, to=4-6]
	\arrow["{F(f^e)}"{description}, from=2-1, to=1-3]
	\arrow["{F(f^n)}"{description}, from=2-4, to=1-6]
	\arrow["{F(f^o)}"{description}, from=5-4, to=4-6]
	\arrow["{\tilde F(f)}"{description}, dotted, from=5-1, to=4-3]
\end{tikzcd}\]
Since by adjusting two commutative cubes like this we get a commutative diagram, for give $f\colon A\to B$ and $g\colon B\to C$ we see that $\tilde F(f)\circ \tilde F(g)$ makes commutative the defining diagram for $\tilde F(f\circ g)$. Thus, by uniqueness of the definition of $\tilde F(f\circ g)$ we see that $\tilde F(f)\circ \tilde F(g)=\tilde F(f\circ g)$. The fact that $\tilde F(\id_{A})=\id_{\tilde F(A)}$ is also obvious from the construction. Thus $\tilde F$ is a functor. The fact that $\eta^F$ is a natural transformation from $F$ to $\tilde F$ could be checked in a straightforward manner using the definition of $\tilde F$. 


The only thing left for us to finish the proof is to show that $\tilde F$ preserves pullback diagrams, when the initial diagram consists of finite orders.

Befor doing this we need some preparatory work. For each natural $k$ let $(-)^n_k,(-)^o_k,(-)^e_k$ be the $\subseteq$-preserving functors that are obtained from  $(-)^n,(-)^o,(-)^e$ by restriction of orders $A^n,A^o,A^e$ to the terms $n$, $\omega a +n$, where $n<k$. The natural transformations $\delta_k\colon (-)^e_k\to (-)^n_k$ and $\gamma_k\colon (-)^o_k\to (-)^n_k$ are defined as the restrictions of the natural transformations $\delta$ and $\gamma$. The crucial property of $(-)^n_k,(-)^e_k,(-)^o_k$ is that they map finite orders to finite orders. We then define functor $\tilde B_k$ and natural transformation $\eta_k^F\colon F\to \tilde B_k$ in the same manner as we have defined $\tilde F$ and $\eta^F$:
 \[\begin{tikzcd}
	& {F(A^e_k)} & {F(A^n_k)} \\
	& {\tilde B_k(A)} & {F(A^o_k)} \\
	{F(A)}
	\arrow["{F(\delta_{k,A})}", from=1-2, to=1-3]
	\arrow["{\zeta_{k,A}}", from=2-2, to=1-2]
	\arrow["{F(\gamma_{k,A})}"', from=2-3, to=1-3]
	\arrow["{\varepsilon_{k,A}}"', from=2-2, to=2-3]
	\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=90}, draw=none, from=2-2, to=1-3]
	\arrow["{\eta_{k,A}^F}"', dotted, from=3-1, to=2-2]
	\arrow["{F(\beta_{k,A})}", bend left =20, from=3-1, to=1-2]
	\arrow["{F(\alpha_{k,A})}"', bend right =20, from=3-1, to=2-3]
\end{tikzcd}\]

Let  $\theta_k\colon (-)^n_k\to (-)^n$, $\iota_k\colon (-)^o_k\to (-)^o$, $\kappa_k\colon (-)^e_k\to (-)^e$ be the natural transformations consisting of the identity maps. We define the natural transformation $\lambda_k\colon \tilde B_k\to \tilde F$ to be the family of the unique maps making the following diagrams commutative:

\[\begin{tikzcd}
	&& {F(A^e)} &&& {F(A^n)} \\
	{F(A^e_k)} &&& {F(A^n_k)} \\
	\\
	&& {\tilde F(A)} &&& {F(A^o)} \\
	{\tilde B_k(A)} &&& {F(A^o_k)}
	\arrow["{F(\delta_{k,A})}", from=2-1, to=2-4]
	\arrow["{\zeta_{k,A}}", from=5-1, to=2-1]
	\arrow["{\varepsilon_{k,A}}"', from=5-1, to=5-4]
	\arrow["{F(\gamma_{k,A})}"', from=5-4, to=2-4]
	\arrow["{F(\delta_A)}", from=1-3, to=1-6]
	\arrow["{F(\gamma_A)}"', from=4-6, to=1-6]
	\arrow["{\zeta_A}", from=4-3, to=1-3]
	\arrow["{\varepsilon_A}"', from=4-3, to=4-6]
	\arrow["{F(\kappa_k)}"{description}, from=2-1, to=1-3]
	\arrow["{F(\theta_k)}"{description}, from=2-4, to=1-6]
	\arrow["{F(\iota_k)}"{description}, from=5-4, to=4-6]
	\arrow["{\lambda_{k,A}}"{description}, dotted, from=5-1, to=4-3]
      \end{tikzcd}\]
Clearly,  due to finitarity of $F$, any element $a\in \tilde F(A)$ is an element of $\lambda_{k,A}[\tilde B_k(A)]$, for sufficiently large $k$.
    
    
We fineshed the preparatory work and consider a pullback diagram consisting of finite linear orders:
\[\begin{tikzcd}
	B & A \\
	D & C
	\arrow["f", from=1-1, to=1-2]
	\arrow["g"', from=2-2, to=1-2]
	\arrow["l"',from=2-1, to=2-2]
	\arrow["h", from=2-1, to=1-1]
	\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=90}, draw=none, from=2-1, to=1-2]
\end{tikzcd}\]
We check that the following diagram is also a pullback diagram
\[\begin{tikzcd}
	\tilde F(B) & \tilde F(A) \\
	\tilde F(D) & \tilde F(C)
	\arrow["\tilde F(f)", from=1-1, to=1-2]
	\arrow["\tilde F(g)"', from=2-2, to=1-2]
	\arrow["\tilde F(l)"',from=2-1, to=2-2]
	\arrow["\tilde F(h)", from=2-1, to=1-1]
\end{tikzcd}\]
For this it is enough to check that for each $a\in \tilde F(A)$ if there are $b\in \tilde F(B)$ and $c\in \tilde F(C)$ such that $\tilde F(f)(b)=\tilde F(f)(d)$, then there is $d\in \tilde F(D)$ such that $\tilde F(h)(d)=b$ and $\tilde F(l)(d)=c$. Indeed consider some $a,b,c$ as above. We choose sufficiently large $k$ such that $a\in \lambda_{k,A}[\tilde B_k(A)]$, $b\in \lambda_{k,B}[\tilde B_k(B)]$, and $c\in \lambda_{k,C}[\tilde B_k(C)]$. We observe    
  
\end{proof}

\fi

\bibliographystyle{abbrv}
