2 Well quasi-orders in reverse mathematics

Given the crucial role played by well quasi-orders in our results, this section is dedicated to their formal introduction in reverse mathematics, particularly over the base theory ${\textsf {RCA}}_0$ , and to a first analysis of their properties which includes novel analysis regarding closure results for ${\textsf {wqo}}$ under order-preserving and order-reflecting functions. For an introduction to reverse mathematics, including the axioms of ${\textsf {RCA}}_0$ , we refer to [Reference Simpson65]; while for a recent introductory survey on wqo, including the more refined notion of better quasi-orders, see [Reference Buriola and Schuster11].

All the following definitions are given in ${\textsf {RCA}}_0$ .

In the following, $|Q|$ is simply denoted by Q, and we may denote with Q also the qo $(Q,\leqslant )$ , omitting the quasi-order relation $\leqslant $ ; moreover, we use $ \thicksim $ for the comparability relation, namely $p \! \thicksim \! q : \Leftrightarrow p \! \leqslant \! q \vee q \! \leqslant \! p$ . Observe that, provable in ${\textsf {RCA}}_0$ , if $(Q,\leqslant )$ is a quasi-order, than $(Q/\! \! \thicksim , \leqslant )$ is a partial order.

To properly work with qo, some auxiliary definitions are needed.

We move on to well quasi-orders.

Many different definitions have been proposed for well quasi-orders; in his classical historical survey [Reference Kruskal44], J. Kruskal referred to wqo as a “frequently discovered concept”. It is therefore natural to ask if all these definitions are equivalent in reverse mathematics, in particular over weak theories like ${\textsf {RCA}}_0$ or ${\textsf {WKL}}_0$ . This problem has been thoroughly treated by Cholak et al. [Reference Cholak, Marcone and Solomon16] and by Marcone [Reference Marcone and Simpson45, Reference Marcone, Schuster, Seisenberger and Weiermann46]. For a recent introductory survey on wqo and the stronger notion of better quasi-orders see [Reference Buriola and Schuster11]. We now briefly summarize their findings.

Let us consider the following definitions for wqo.

For what concerns the relations over ${\textsf {RCA}}_0$ , ${\textsf {WKL}}_0$ , and ${\textsf {ACA}}_0$ , between these definitions, the main results in [Reference Cholak, Marcone and Solomon16, Reference Marcone and Simpson45, Reference Marcone, Schuster, Seisenberger and Weiermann46] are the following.

Given their good behavior, one of the main problems in the theory of well quasi-orders concerns how to obtain new wqo’s or, equivalently, how to preserve the property of being wqo. Two standard operations on qo are product and (disjoint) union.

The word “disjoint” may be omitted; for other possible quasi-order operations, for example, the sum $P +Q$ (see [Reference Buriola and Weiermann13, Reference Marcone, Schuster, Seisenberger and Weiermann46]).

We now consider the closure of wqo under product, union, and subsets, starting with the good behavior of union.

Except for wqo(ext), a similar well behavior also holds for subsets.

The statement of the previous lemma for wqo(ext) is still open, see [Reference Marcone, Schuster, Seisenberger and Weiermann46, Question 2.15]; similarly, it is still open in the context of constructive mathematics [Reference Buriola, Schuster, Blechschmidt, Vedova, Dundua, Lempp and Manea12]. In the case of the product the situation is far more complex, as showed by the next result.

These limitations regarding the product of wqo will partially affect the proof of Theorem 4.2. For sake of completeness, let us observe that the property “ $P,Q$ wqo implies $P \times Q$ wqo” is known to be strictly between the principles CAC and ADS [Reference Towsner68, Theorem 1.16]. We consider the preservation of wqo with respect to functions, starting with the following definition.

Regarding wqo preservation with respect to such order functions, we have the following result whose provability over ${\textsf {RCA}}_0$ is, to the best of our knowledge, novel in the literature.

Proof We start with the first point, that is, $\phi $ order-preserving surjection, considering all the cases for $\mathcal {P}$ .

[P wqo] Let $(q_k)_k$ be an infinite sequence in Q, since $\phi $ is surjective we can find (also in ${\textsf {RCA}}_0$ ) an infinite sequence $(p_k)_k$ in P such that for all k, $\phi (p_k)=q_k$ ; but P is wqo, thus there exist indexes $i<j$ such that $p_i \leqslant _P p_j$ and, since $\phi $ is order-preserving, we obtain $q_i=\phi (p_i) \leqslant _Q \phi (p_j)=q_j$ .

[P wqo(set) or P wqo(anti)] The previous technique works here too.

[P wqo(ext)] In order to keep the notation readable, we only consider the case $P,Q$ partial orders, although the following strategy extends to quasi-orders. Let $\preccurlyeq _Q$ be a linear extension of $\leqslant _Q$ , we have to prove that $\preccurlyeq _Q$ is well-founded. For each element $q \! \in \! Q$ , we consider the subset $P_q= \phi ^{-1}(q) =\{ p\! \in \! P \, |\, \phi (p)=q \}$ together with the restriction $\leqslant _P \downharpoonright _{P_q}$ of $\leqslant _P$ to $P_q$ ; by Szpilrajn’s theorem, available in ${\textsf {RCA}}_0$ ([Reference Downey, Hirschfeldt, Lempp and Solomon23, Observation 6.1], see also [Reference Frittaion and Marcone31]), we can consider for each $q\! \in \! Q$ a linear extension $\trianglelefteq _q$ of $(P_q, \leqslant _P \downharpoonright _{P_q})$ . We define the following order on P:

$$\begin{align*}p_1 \preccurlyeq_P p_2 : \Leftrightarrow \phi(p_1) \prec_Q \phi(p_2) \, \vee \, (\phi(p_1)=\phi(p_2) \wedge p_1 \trianglelefteq _{\phi(p_1)} p_2). \end{align*}$$

It is straightforward to verify that $\preccurlyeq _P$ is a linear extension of $\leqslant _P$ and $p_1 \! \preccurlyeq _P \! p_2$ implies $\phi (p_1) \! \preccurlyeq _Q \! \phi (p_2)$ .

Since $\preccurlyeq _P$ is a linear order extending $\leqslant _P$ and P is wqo(ext), then $\preccurlyeq _P$ is a well-order. Let us assume, by contradiction, that $q_1 \succ _Q q_2 \succ _Q \dots $ is a strictly descending chain in $(Q, \preccurlyeq _Q)$ , since $\phi $ is surjective we can find a sequence $p_1, p_2, \dots $ such that $\phi (p_k)=q_k$ for all k; but $\preccurlyeq _P$ is a well-order, thus there exist $i \! < \! j$ such that $p_i \preccurlyeq p_j$ and then $\phi (p_i) \preccurlyeq _Q \phi (p_j)$ , contradiction.

Let us consider the second point, namely $\phi $ order-reflecting.

[Q wqo] Let $(p_k)_k$ be an infinite sequence in P, then $(\phi (p_k))_k$ is an infinite sequence in Q and thus there exist indexes $i\! < \! j$ such that $\phi (p_i) \! \leqslant _Q \! \phi (p_j)$ ; but, since $\phi $ is order-reflecting, this implies $p_i \! \leqslant _P \! p_j$ .

[P wqo(set) or P wqo(anti)] The previous strategy works here too.

As before, the case wqo(ext) is still open for an order-reflecting map $\phi $ .

We conclude this section by formally stating Higman’s lemma, recalling that $Q^* \! : = \bigcup _{n=0}^{\infty }Q^n$ is the set of finite sequences on Q.

Lemma 2.3. If $(Q,\leqslant )$ is a wqo, then $(Q^*,\leqslant ^*)$ is a wqo, where:

$$\begin{align*}p_1\dots p_n \leqslant^* q_1 \dots q_m \ \ \text{iff} \ \ \exists 1 \! \leqslant \! i_1 \! < \! \dots \! < \! i_n \! \leqslant \! m\ \forall k\! \in \! \{1,\dots,n\}\ p_k \leqslant q_{i_k}. \end{align*}$$

Higman’s lemma, together with Dickson’s lemma, will be analysed from a proof-theoretic point of view in Section 5; for now, let us recall that, provably over ${\textsf {RCA}}_0$ , Higman’s lemma is equivalent to the formal system ${\textsf {ACA}}_0$ .

Remarkably, if in Higman’s lemma finite sequences are substituted with infinite sequences (and an appropriate embedding relation), then the corresponding statement is false, as proved by Rado’s counterexample [Reference Rado55]. The fact that not all operations preserve the property of being a wqo, particularly the infinitary ones, is the main reason that motivated the introduction of better quasi-orders [Reference Carroy, Pequignot, Schuster, Seisenberger and Weiermann15, Reference Nash-Williams52].

3 Abstract algebras and trees

In this section, we introduce the two main topics of the article, Higman’s and Kruskal’s theorem, as well as the required preliminaries.

3.1 Ordered algebras and Higman’s theorem

This paragraph is devoted to formally present ordered algebras and Higman’s theorem. As before all the definitions are given in ${\textsf {RCA}}_0$ ; however, since dealing in ${\textsf {RCA}}_0$ with sets of operations, that is, sets of functions and thus sets of sets, required some care, the following definition is slightly more involved than its classical counterpart [Reference Higman40].

Definition 3.1. An n-ary (abstract) algebra $(A,M)$ is given by a set $|A| \! \subseteq \! \mathbb {N}$ together with a finite list $M=(M_i)_i$ with $1\! \leqslant \! i \! \leqslant \! n$ of sequences, possibly finite, infinite, or empty, of operations over $|A|$ ; for each i, $M_i$ is the sequence of i-ary operations from $|A|^i$ to $|A|$ .

As for qo, we tacitly write A instead of $|A|$ , omitting also the term “abstract”. Moreover, although it does not formally exist in ${\textsf {RCA}}_0$ as a set, we use M to refer to the family of all the operations of the algebra; namely $\mu \in M$ is not a well-defined formula of our syntax, but just a syntactic abbreviation of “ $\mu $ is an operation over A”.

Remark 3.1. Since each operation $\mu $ is uniquely determined by its arity r, that is, $\mu \! \in \! M_r$ for some $r\! \in \! \{1, \dots , n\}$ , and its position d in the sequence $M_r$ , we can uniquely assign a natural number $|\mu |$ to each operation, allowing us to consider also the set $|M_i|$ of the codes of elements of $M_i$ ; moreover, we can also require that codes for operations and codes for elements of A are disjoint. Given this bijection, at least in the metatheory, in the following we write $\mu $ for both an operation and the corresponding code relying on the context to make clear the exact meaning; similarly for $M_i$ and $|M_i|$ .

The following generalization can be stated.

Definition 3.2. An (abstract) algebra $(A,M)$ is given by a set $|A| \! \subseteq \! \mathbb {N}$ together with a sequence M of operations over $|A|$ , to any operation $\mu \in M$ is associated its arity $d(\mu )$ .

As before, we simply write A instead of $|A|$ , omitting the word “abstract” and, frequently, also the arity operator d. In analogy with the previous case, we can associate a unique code to each operation of M (and thus considering the code set $|M|$ ), requiring these codes to be different from the codes of elements of A. Finally, we underline how an n-ary algebra can be seen as an algebra placing $M=M_1 \cup \dots \cup M_n$ and $d(\mu )=i$ if $\mu \! \in \! M_i$ .

For algebras, there are the following auxiliary definitions.

Definition 3.3. Given an algebra $(A,M)$ :

• • $(B,M)$ is a subalgebra of $(A,M)$ if $B \subseteq A$ and B is closed with respect to M, that is, for every $\mu $ in M of arity $d(\mu )$ and every $b_1, \dots , b_{d(\mu )}$ in B, $\mu (b_1, \dots , b_{d(\mu )}) \in B$ ;

• • $C \subseteq A$ is a generating set of A, and A is generated by C, if for every subalgebra $(B,M)$ of $(A,M)$ , $C \subseteq B$ implies $B=A$ .

Quasi-orders and abstract algebras can now be linked together.

Definition 3.4. Given an algebra $(A,M)$ and a quasi-order $\leqslant $ over A:

1. 1. $(A,M,\leqslant )$ is an ordered algebra if for any function $\mu \! \in \! M$ with arity $d(\mu )$

   $$\begin{align*}\forall i\! \leqslant \! d(\mu) \ a_i \! \leqslant \! b_i \ \ \text{implies}\ \ \mu(a_1, \dots, a_{d(\mu)}) \! \leqslant \! \mu(b_1, \dots, b_{d(\mu)}); \end{align*}$$

2. 2. $\leqslant $ is a divisibility order if, in addition, for any function $\mu \! \in \! M$ with arity $d(\mu )$

   $$\begin{align*}\forall i\! \leqslant \! d(\mu) \ \, a_i \leqslant \mu(a_1, \dots, a_{d(\mu)}); \end{align*}$$

3. 3. $\leqslant $ is compatible with a qo $\trianglelefteq $ on M if for any $\mu , \lambda $ in M

   $$\begin{align*}a_1\dots a_{d(\lambda)} & \leqslant^* b_1\dots b_{d(\mu)}\ \text{and}\ \lambda \! \trianglelefteq \! \mu \ \, \text{imply}\ \, \lambda(a_1, \dots, a_{d(\lambda)}) \\& \leqslant \mu(b_1,\dots , b_{d(\mu)}), \end{align*}$$
   where $\leqslant ^{*}$ is Higman’s order (see Lemma 2.3).

This definition can be given almost untouched for an n-ary algebra too, the only concrete modification is for compatibility. In an n-ary algebra, we could have different qo’s $\trianglelefteq _r$ , one for each operation set $M_r$ ; compatibility is then stated separately for each arity, that is, if $\lambda , \mu $ belong to $M_r$ then

$$\begin{align*}\forall i\! \leqslant \! r \ a_i \! \leqslant \! b_i \ \ \text{and}\ \ \lambda \! \trianglelefteq _r \! \mu \ \ \text{imply}\ \ \lambda(a_1, \dots, a_r) \! \leqslant \! \mu( b_1, \dots, b_r). \end{align*}$$

Properties 1. and 2. of the previous definition, or their equivalents, can be found also in other contexts. A function over ordinals satisfying those conditions is commonly called, respectively, monotonic and increasing [Reference Schmidt, Schuster, Seisenberger and Weiermann59, Definition 4.5]; while, talking about natural numbers, such a function is dubbed, respectively, weakly increasing and inflationary [Reference Weiermann72, p. 178].

Remark 3.2 (cf. Remark 3.1).

Formally speaking in the third point of Definition 3.4 (compatibility), given a qo $\trianglelefteq $ over $|M|$ , we are requiring that $\leqslant $ preserves this order, namely,

$$\begin{align*}a_1\dots a_{d(\lambda)} \! \leqslant^* \! b_1\dots b_{d(\mu)}\ \text{and}\ |\lambda| \! \trianglelefteq \! |\mu| \ \text{imply}\ \lambda(a_1, \dots, a_{d(\lambda)}) \! \leqslant \! \mu(b_1,\dots , b_{d(\mu)}). \end{align*}$$

The finite and the infinite versions of Higman’s theorem can finally be stated; the former is found in the seminal paper of Higman [Reference Higman40], while the latter is presented in [Reference Pouzet and Riva54]. For each $n \! \in \! \mathbb {N}$ , we have the corresponding version of the following theorem.

Theorem 3.1 (n-finite Higman’s theorem).

Given an n-ary ordered algebra $(A,M,\leqslant )$ , if $(M_r, \trianglelefteq _r)$ is a wqo for each r, $\leqslant $ is a divisibility order compatible with the qo’s of M and $(A,M)$ is generated by a wqo set $C\subseteq A$ , then $(A,\leqslant )$ is wqo.

Using a notation similar to the one reserved for the various versions of Kruskal’s theorem (see below), each n-version of the previous theorem is denoted by HT $(n)$ , for example, HT $(3)$ corresponds to the theorem for $3$ -ary ordered algebras. Given this notation, the original theorem due to Higman [Reference Higman40] simply reads as follows.

Theorem 3.2 (Original Higman’s theorem).

$\forall n\, \text {HT}(n)$ .

Using abstract algebras, an infinite version of Higman’s theorem, denoted by HT $(\omega )$ and firstly proposed by Pouzet [Reference Pouzet and Riva54, Theorem 2.2],Footnote ² can be stated.

Theorem 3.3 (Infinite Higman’s theorem).

Given an ordered algebra $(A,M,\leqslant )$ , if $(M, \trianglelefteq )$ is a wqo, $\leqslant $ is a divisibility order compatible with $\trianglelefteq $ and $(A,M)$ is generated by a wqo set $C\subseteq A$ , then $(A,\leqslant )$ is wqo.

The crucial difference between the finite and the infinite version is the presence in the former of an arbitrarily high, but fixed, upper bound on the arity of the operations in M. The main references for abstract algebras are Higman’s original paper [Reference Higman40] and the book of Cohn [Reference Cohn18].

3.2 Labelled trees and Kruskal’s theorem

We start by recalling some definitions regarding trees, tree embedding, and branching degree; as before, all definitions are stated in ${\textsf {RCA}}_0$ .

Definition 3.5. Given a set Q, we inductively define the set $\mathbb {T}(Q)$ of (finite ordered) trees with labels in Q as follows:

1. 1. for each $q \! \in \! Q$ , $q[]$ is an element of $\mathbb {T}(Q)$ ;

2. 2. if $t_1, \dots , t_n$ , with $n \! \geqslant \! 1$ , is a finite sequence of elements of $\mathbb {T}(Q)$ and $q \! \in \! Q$ , then $t \! : = q[t_1, \dots , t_n]$ is an element of $\mathbb {T}(Q)$ .

Since all trees considered in this article are finite and ordered, we omit these specifications. Connected to labelled trees, there are the following definitions.

Definition 3.6. Let Q and $\mathbb {T}(Q)$ be as before:

• • if $t = q[t_1, \dots , t_n]$ , then $l(t) \! : = q$ is the label of the t and $t_1, \dots , t_n$ are called the (immediate) subtrees of t;

• • the set of nodes $\mathcal {N}(t)$ of $t \in \mathbb {T}(Q)$ is recursively defined as:

  1. 1. if $t=q[]$ , then $\mathcal {N}(t) \! : = \{ t\}$ ;

  2. 2. if $t=q[t_1, \dots , t_n]$ , then $\mathcal {N}(t) \! : = \{ t\} \cup \mathcal {N}(t_1) \cup \dots \cup \mathcal {N}(t_n)$ ;

• • if Q is a singleton, then $\mathbb {T} \! : = \mathbb {T}(Q)$ is the set of unlabelled trees.

Starting from a qo Q, it is possible to define an embeddability relation.

Definition 3.7. Given a qo $(Q,\leqslant _Q)$ and $t,s \! \in \! \mathbb {T}(Q)$ , we inductively define the embeddability relation $\preccurlyeq $ on $\mathbb {T}(Q)$ as follows: $t \preccurlyeq s$ holds if

1. 1. $t=p[]$ , $s=q[]$ , and $ p \leqslant _Q q$ ; or

2. 2. $s=q[s_1, \dots , s_m]$ and $t \preccurlyeq s_i$ for some $ 1 \! \leqslant \! i \! \leqslant \! m$ ; or

3. 3. $t=p[t_1, \dots , t_n]$ , $s=q[s_1, \dots , s_m]$ , $p \leqslant _Q q$ and $t_1\dots t_n \preccurlyeq ^{*} s_1 \dots s_m$ .

Here, $\preccurlyeq ^{*}$ is Higman’s order with respect to $\preccurlyeq $ (see Lemma 2.3).

Let us observe that $(\mathbb {T}(Q), \preccurlyeq )$ is a quasi-order.

Before stating Kruskal’s theorems, one last definition is required: the branching degree.

Definition 3.8. The degree, d, and the branching degree, $Deg$ , of a tree $t \! \in \! \mathbb {T}(Q)$ are recursively defined as:

1. 1. if $t=q[]$ , then $d(t)=Deg(t) \! : = 0$ ;

2. 2. if $t=q[t_1, \dots , t_n]$ , then $d(t) \! : = n$ and $Deg(t) \! : = \max \{n, Deg(t_1), \dots , Deg(t_n)\}$ .

Moreover, for every $n \! \in \! \mathbb {N}$ and every set Q:

• • $\mathbb {T}_n$ is the set of unlabelled trees with branching degree less or equal to n;

• • $\mathbb {T}_n(Q)$ is the set of trees with labels in Q and branching degree less or equal to n.

Since only finite trees are considered, d and $Deg$ are always well defined.

We now present the various versions of Kruskal’s theorem under scrutiny; each is denoted by an abbreviation, possibly accompanied by a numeric parameter.

Theorem 3.4. The following statements hold for every natural number n:

• K $\text {T}(n)$ : $(\mathbb {T}_n, \preccurlyeq )$ is a wqo;

• K $\text {T}(\omega )$ : $(\mathbb {T},\preccurlyeq )$ is a wqo;

• K $\text {T}_\ell (n)$ : if Q is a wqo, then $(\mathbb {T}_n(Q), \preccurlyeq )$ is a wqo;

• K $\text {T}_\ell (\omega )$ : if Q is a wqo, then $(\mathbb {T}(Q), \preccurlyeq )$ is a wqo.

Starting from the original paper by Kruskal [Reference Kruskal43], proofs of Kruskal’s theorem, or its variation, are ubiquitous in the literature [Reference Goubault-Larrecq, Chatterjee and Sgall38, Reference Nash-Williams51, Reference Sternagel67, Reference Veldman70]. For what concerns its strength from the reverse mathematics point of view, by a result due to Harvey Friedman [Reference Simpson, Harrington, Morley, Šcedrov and Simpson63] (see also [Reference Gallier32]), it is known that even Kruskal’s theorem for unlabelled trees (K $\text {T}(\omega )$ in our notation), as well as its finite miniaturization [Reference Simpson, Harrington, Morley, Šcedrov and Simpson63, Reference Smith, Harrington, Morley, Šcedrov and Simpson66], is not provable in ${\textsf {ATR}}_0$ . A thorough investigation of the unlabelled versions of Kruskal’s theorem has been carried out by Rathjen and Weiermann [Reference Rathjen and Weiermann57], some of their results can be summarized in the following theorem.

Theorem 3.5 (Rathjen and Weiermann).

$$ \begin{align*} \text{RCA}_0 \vdash \, \forall n\, \text{KT}(n) \, \leftrightarrow \, \text{KT}(\omega) \, \leftrightarrow \, \text{WO}\left( \vartheta (\Omega^{\omega}) \right). \end{align*} $$

In the previous statement, WO $\left (\vartheta ( \Omega ^{\omega }) \right )$ denotes the well-orderedness of the countable ordinal $\vartheta (\Omega ^{\omega })$ , where $\vartheta $ is a so-called collapsing function (see [Reference Buchholz8, Reference Van der Mereen47, Reference Rathjen and Weiermann57] for an introduction to such functions). As we will see, the situation for the labelled case is quite different.

4 Relations between Higman’s and Kruskal’s theorems

Adapting to the framework of reverse mathematics the proof by Pouzet [Reference Pouzet and Riva54] (see also [Reference Schmidt, Schuster, Seisenberger and Weiermann59]), we prove that, regarding ordered algebras and labelled trees, Higman’s and Kruskal’s theorems are two sides of the same coin. We first consider the fine case, namely HT $(n)$ and KT $_\ell (n)$ ; our goal is to prove the following equivalence.

The previous result is an immediate consequence of the following lemma that is provable in ${\textsf {RCA}}_0$ .

Proof Let us prove Lemma 4.1 by fixing n and considering each direction separately. First of all, we introduce some notation:

• • $ \leqslant $ indicates the qo over the set A, representing an n-ary algebra, whose elements are denoted by $ a,b,c \dots $ ; $\leqslant $ will be also the usual order over $\mathbb {N}$ .

• • $\trianglelefteq $ stands for the qo over $M_r$ for each r, whose elements are denoted by $\mu , \lambda , \dots $ ; for sake of readability, we use the same symbol $\trianglelefteq $ for each set $M_r$ , $1 \! \leqslant \! r \! \leqslant \! n$ .

• • $\preccurlyeq $ represents the embeddability relation between finite ordered labelled trees, which are denoted by $t,s, \dots $ ; if necessary, also the extended notation $t=q[t_1, \dots , t_n]$ is used.

“HT $(n) \Rightarrow \text {KT}_\ell (n)$ ”

Given a wqo $(Q,\leqslant )$ , we must prove that $(\mathbb {T}_n(Q), \preccurlyeq )$ is well quasi-ordered by $\preccurlyeq $ . For each $1 \leqslant r \leqslant n$ and $q \! \in \! Q$ , we define the following operation over $\mathbb {T}_n(Q)$ :

$$\begin{align*}\bigoplus_{r,q} : \mathbb{T}_n(Q)^r \rightarrow \mathbb{T}_n(Q)\ \text{with} \ \bigoplus_{r,q}(t_1, \dots, t_r) \! := q[t_1, \dots , t_r], \end{align*}$$

where $q[t_1, \dots , t_r]$ is the tree whose root is labelled by q and whose immediate subtrees are $t_1, \dots , t_r$ . We dub $\bigoplus _{N,Q}$ the family of all these operations (which is in bijection with $\{1, \dots , n\} \times Q$ ); for each of these operations we can consider a unique code (see Remark 3.1). For each $1 \leqslant r \leqslant n$ , we quasi-order the set $\bigoplus _{r,Q}=\{ \bigoplus _{r,q}\, | \, q \! \in \! Q \}$ (of codes) of r-ary operations in the following way: $\bigoplus _{r,q} \trianglelefteq _r \bigoplus _{r,p}$ iff $q \! \leqslant \! p$ ; with such quasi-orders each $(\bigoplus _{r,Q}, \trianglelefteq _r)$ is a wqo, since also $(Q, \leqslant )$ is a wqo.

Claim. $(\mathbb {T}_n(Q), \bigoplus _{N,Q}, \preccurlyeq )$ is an ordered n-ary algebra with $\preccurlyeq $ a divisibility order compatible with $\trianglelefteq $ ; moreover $C=\{q[]\, |\, q \! \in \! Q\}$ is a generating set for $\mathbb {T}_n(Q)$ .

Proof of the Claim

Since $\bigoplus _{N,Q}$ is a family of at most n-ary operations, we need to check the three properties of Definition 3.4 regarding the quasi-order $\preccurlyeq $ and the generation of $\mathbb {T}_n(Q)$ by C.

Ordered algebra: Given $1 \! \leqslant \! r \! \leqslant \! n,\ q \! \in \! Q$ , and $t_i \! \preccurlyeq \! s_i$ for all $1 \! \leqslant \! i \! \leqslant \! r$ , then $q[t_1, \dots , t_r] \preccurlyeq q[s_1, \dots , s_r]$ holds by the third condition of Definition 3.7; thus, $\bigoplus _{r,q}(t_1, \dots , t_r) \! \preccurlyeq \! \bigoplus _{r,q}(s_1, \dots , s_r)$ .

Divisibility: Given $1 \! \leqslant \! r \! \leqslant \! n$ and $q \! \in \! Q$ , $t_i \! \preccurlyeq \! q[t_1, \dots , t_r]$ holds by the second condition of Definition 3.7; therefore, $t_i \! \preccurlyeq \! \bigoplus _{r,q}(t_1, \dots , t_r)$ for all $1 \! \leqslant \! i \! \leqslant \! r$ .

Compatibility: Given $1 \! \leqslant \! r \! \leqslant \! n$ , $\bigoplus _{r,q} \! \trianglelefteq \! \bigoplus _{r,p}$ , and $t_i \! \preccurlyeq \! s_i$ for all $1 \! \leqslant \! i \! \leqslant \! r$ , then $q \! \leqslant \! p$ and $q[t_1, \dots , t_r] \! \preccurlyeq \! p[s_1, \dots , s_r]$ holds by the third case of Definition 3.7; thus $\bigoplus _{r,q}(t_1, \dots , t_r) \preccurlyeq \bigoplus _{r,p}(s_1, \dots , s_r)$ .

Generation: Obviously $C\! \subseteq \! \mathbb {T}_n(Q)$ ; we need to prove that, given a subset $B\! \subseteq \! \mathbb {T}_n(Q)$ closed with respect to $\bigoplus _{N \!,Q}$ , if $C \! \subseteq \! B$ , then $B = \mathbb {T}_n(Q)$ . Let $C \! \subseteq \! B$ and $t \! \in \! \mathbb {T}_n(Q)$ , if $t \! \in \! C$ , that is, $t=q[]$ with $q \! \in \! Q$ , then $t \! \in \! B$ ; else t is obtained by a finite number of elements of C, the leaves of t, and a finite number of applications of operations in $\bigoplus _{N,Q}$ . Since B is closed with respect to $\bigoplus _{N,Q}$ , $t \! \in \! B$ and thus $B = \mathbb {T}_n(Q)$ . Lastly, $(C, \preccurlyeq )$ is wqo since $q[] \! \preccurlyeq \! p[] \Leftrightarrow q \leqslant p$ and $(Q,\leqslant )$ is wqo by hypotheses. End of the proof of the Claim.

To conclude, since $\trianglelefteq $ is a wqo on $\bigoplus _{N,Q}$ , we can apply HT $(n)$ to obtain that $(\mathbb {T}_n(Q), \preccurlyeq )$ is a wqo.

“KT $_\ell (n) \Rightarrow \text {HT}(n)$ ”

Let $(A,M,\leqslant )$ be an n-ary ordered algebra satisfying all the hypotheses of Higman’s theorem: each set of r-ary operations $M_r$ is a wqo with respect to $\trianglelefteq $ ; $\leqslant $ is a divisibility order compatible with the wqo $\trianglelefteq $ of each $M_r$ ; there is a wqo generating set C. We must prove that $(A,\leqslant )$ is wqo.

Since M is a wqo (given by the finite disjoint union $M_1 \cup \dots \cup M_n$ of wqo’s) and C is a wqo, so is $C\! \cup \! M$ , by Lemma 2.1, and applying K $\text {T}_\ell (n)$ so is $(\mathbb {T}_n(C\! \cup \! M), \preccurlyeq )$ . Over $C\! \cup \! M$ , we consider the grade function $g\! :\! C \! \cup \! M \rightarrow \mathbb {N}$ defined as $g(x) \! : = 0$ if $x \! \in \! C$ and $g(x) \! : = r$ if $x\! \in \! M_r$ . Finally, we define, inside $\mathbb {T}_n(C\! \cup \! M)$ , the subset $\mathbb {T}_n^g(C\! \cup \! M)$ of graded trees, that is, the trees t satisfying the following grade condition:

$$\begin{align*}\forall s\! \in \! \mathcal{N}(t) \ \ d(s)=g(l(s)). \end{align*}$$

In other words, we are considering trees t such that, for each node s, the degree $d(s)$ of the node is equal to the grade g of the label $l(s)$ of the node itself. The functions $g,d$ , and $\mathbb {T}_n^g(C\! \cup \! M)$ are all definable in ${\textsf {RCA}}_0$ ; moreover, $\mathbb {T}_n^g(C\! \cup \! M)$ is well quasi-ordered by $\preccurlyeq $ .

We now construct an order-preserving function $\phi $ between $(\mathbb {T}_n^g(C\! \cup \! M), \preccurlyeq )$ and $(A,M,\leqslant )$ that is defined by recursion over the tree structure of the elements of $\mathbb {T}_n^g(C\! \cup \! M)$ :

$$\begin{align*}\phi (t) = \left\{ \begin{array}{@{}ll} q & \text{if}\ t=q[]\ \text{with}\ q\! \in \! C;\\ \mu (\phi(t_1), \dots , \phi(t_r)) & \text{if}\ t=\mu[t_1, \dots , t_r]\ \text{with}\ \mu \! \in \! M_r. \end{array} \right. \end{align*}$$

Since we are considering graded trees, the label of a leaf is always an element of C; whereas the label of a node of degree r is always (the code of) an operation of $(A,M)$ of arity r, that is, an element of $M_r$ . This, together with the fact that we are treating ordered trees (i.e., $\lambda [t_1,t_2] \not = \lambda [t_2,t_1]$ , unless $t_1=t_2$ ), ensures that $\phi $ is well defined. An instance of $\phi $ is depicted below.

We prove by induction that $\phi $ is order-preserving, that is, $t\! \preccurlyeq \! s \Rightarrow \phi (t) \!\leqslant \! \phi (s)$ , considering the three defining cases of Definition 3.7. Given $t,s \! \in \! \mathbb {T}_n^g(C\! \cup \! M)$ :

1. 1. if $t \! \preccurlyeq \! s$ with $t=q[], s=p[]$ , then $q \leqslant p$ and thus $\phi (t) \! \leqslant \! \phi (s)$ ;

2. 2. if $t \! \preccurlyeq \! s$ with $s=\mu [s_1, \dots , s_r]$ , $\mu \! \in \! M_r$ , and $t \preccurlyeq s_i$ for some $i\! \in \! \{ 1, \dots , r \}$ , then, by induction, $\phi (t) \! \leqslant \! \phi (s_i)$ and, since $\leqslant $ is a divisibility order, $\phi (t) \! \leqslant \! \mu ( \phi (s_1), \dots , \phi (s_r))$ , thus $\phi (t) \! \leqslant \! \phi (s)$ ;

3. 3. if $t \! \preccurlyeq \! s$ with $t=\mu [t_1, \dots , t_r]$ , $s=\lambda [s_1, \dots , s_k]$ , $\mu \! \in \! M_r$ , $\lambda \! \in \! M_k$ , $\mu \trianglelefteq \lambda $ and there exist $1 \! \leqslant \! i_1 \! < \! \dots \! < \! i_r \! \leqslant \! k$ such that $t_1 \! \preccurlyeq s_{i_1}, \dots , t_r \! \preccurlyeq \! s_{i_r}$ , then, by definition of $\trianglelefteq $ , $r=k$ and, by induction, $\phi (t_1) \! \leqslant \! \phi (s_1), \dots , \phi (t_r) \! \leqslant \! \phi (s_r)$ , thus, since $\leqslant $ is compatible with $\trianglelefteq $ , $\mu (\phi (t_1), \dots ,\phi (t_r)) \! \leqslant \! \lambda (\phi (s_1), \dots , \phi (s_r))$ , that is, $\phi (t) \! \leqslant \! \phi (s)$ .

In order to conclude by applying Theorem 2.1, we need to prove that $\phi $ is also surjective. Let us consider $\phi (\mathbb {T}_n^g(C\! \cup \! M)) \! \subseteq \! A$ . Obviously $C \subseteq \phi (\mathbb {T}_n^g(C \cup M))$ ; since C is a generating set it suffices to check that $\phi (\mathbb {T}_n^g(C \cup M))$ is closed under M. Given $a_1, \dots , a_r \! \in \! \phi (\mathbb {T}_n^g(C\! \cup \! M))$ and $\mu \! \in \! M_r$ , there exist $t_1, \dots , t_r \! \in \! \mathbb {T}_n^g(C\! \cup \! M)$ such that $\phi (t_1)=a_1, \dots , \phi (t_r)=a_r$ ; but now $\mu [t_1, \dots , t_r]$ , that is, the tree with the root labelled by $\mu $ and with immediate subtrees $t_1, \dots , t_r$ , is an element of $\mathbb {T}_n^g(C\! \cup \! M)$ and, by definition, $\phi (\mu [t_1, \dots , t_r])=\mu (\phi (t_1), \dots , \phi (t_r))=\mu (a_1, \dots , a_r)$ , thus $\mu (a_1, \dots , a_r) \! \in \! \phi (\mathbb {T}_n^g(C\! \cup \! M))$ . So $\phi (\mathbb {T}_n^g(C\! \cup \! M))=A$ , that is, $\phi $ is surjective, and we can apply Theorem 2.1 to conclude that $(A,\leqslant )$ is wqo.

We move to the infinite case of the previous equivalence.

Theorem 4.2. ${\textsf {RCA}}_0\, \vdash $ HT( $\omega $ ) $\longleftrightarrow $ KT $_\ell $ ( $\omega $ ).

Proof The general framework is quite similar, the main differences regarding the background are the following:

• • We are dealing with abstract algebras rather than n-ary algebras; this means that we could have operations of any finite arity. In particular, since an infinite union of wqo’s is not in general a wqo, we do not consider a wqo $\trianglelefteq _r$ for each set $M_r$ of r-ary operations as before; conversely, we have one single wqo $\trianglelefteq $ over the set M.

• • We are dealing with trees of, possibly, any finite branching degree, that is, we consider $\mathbb {T}(Q)$ and $\mathbb {T}^g(Q)$ rather than $\mathbb {T}_n(Q)$ and $\mathbb {T}_n^g(Q)$ .

For what concerns the proof, we briefly highlight the required adaptations being the general strategy essentially the same.

“HT $(\omega ) \Rightarrow \text {KT}_\ell (\omega )$ ”: the main difference involves the operations $\bigoplus _{r,q}$ which are now defined for each natural number $r\! \in \! \mathbb {N}$ . The set (of codes) $\bigoplus _{\mathbb {N}, Q}$ is well quasi-ordered by the “quotient order” over Q, that is, $\bigoplus _{n,q} \! \trianglelefteq \! \bigoplus _{m,p}$ iff $q\! \leqslant \! p$ (we can not take directly $\mathbb {N} \times Q$ since, by Theorem 2.2, RCA $_0$ does not prove in general that $\mathbb {N} \times Q$ is a wqo). We have then a corresponding version of the claim.

Claim. $(\mathbb {T}(Q), \bigoplus _{\mathbb {N},Q}, \preccurlyeq )$ is an ordered algebra with $\preccurlyeq $ a divisibility order compatible with $\trianglelefteq $ ; moreover $C=\{q[]\, |\, q \! \in \! Q\}$ is a generating set for $\mathbb {T}(Q)$ .

The proof of the claim, as well as the rest of this direction, is almost equal; a minor modification occurs for compatibility since, through $\trianglelefteq $ , we can compare operations $\bigoplus _{r,q}$ and $\bigoplus _{s,p}$ with different arities, that is, $r\not = s$ .

“KT $_\ell (\omega ) \Rightarrow \text {HT}(\omega )$ ”: in this case, M is directly a wqo and we apply K $\text {T}_\ell (\omega )$ to obtain the well quasi-orderedness of $(\mathbb {T}(C \cup M), \preccurlyeq )$ . The grade function g is now an extension of the arity function d of the abstract algebra under consideration, namely $g\! :\! C \! \cup \! M \rightarrow \mathbb {N}$ is defined as $g(x) \! : = 0$ if $x \! \in \! C$ and $g(x) \! : = d(x)$ if $x\! \in \! M$ . The remaining minor changes concern notation.

From previous equivalences, in particular the one between finite versions, the following corollary is derivable.

In [Reference Buriola and Weiermann13], the authors computed the $\Pi ^1_1$ proof-theoretic ordinalsFootnote ⁴ of $\forall n \,\text {K}\text {T}_\ell (n)$ and K $\text {T}_\ell (\omega )$ obtaining the following estimations.

Theorem 4.3.

$$\begin{align*}|{\textsf{RCA}}_0 + \forall n\, \text{KT}_{\ell}(n)|=\vartheta (\Omega^{\omega}+\omega)\ \text{and}\ |\textsf{RCA}_0 + \text{KT}_{\ell}(\omega)|=\vartheta (\Omega^{\omega+1}). \end{align*}$$

From this last theorem, the following separation result, which is in striking contrast with Theorem 3.5, derives.

Previous findings regarding Higman’s and Kruskal’s theorems can be summed up in the above proof-relation schema where all the possible implications over ${\textsf {RCA}}_0$ are depicted (Figure 1).

Figure 1

Proof-theoretic relations over ${\textsf {RCA}}_0$ between finite and infinite versions of Higman’s theorem and Kruskal’s theorem, with and without labels.

5 Relations between Higman’s and Dickson’s lemmas

Despite having been subsequently overtaken by Kruskal’s theorem, Higman’s and Dickson’s lemma remain two remarkable milestones in the history of well quasi-order theory. In this section, we collect the main proof-theoretic results regarding these two achievements, including their proof-theoretic ordinals. Recall that $Q^{*}$ denotes the set of finite sequences over Q.

Several findings present in the literature [Reference Carlucci, Mainardi and Rathjen14, Reference Clote, Ambos-Spies, Müller and Sacks17, Reference Girard35, Reference Hasegawa, Jones, Hagiya and Sato39, Reference Simpson64, Reference Simpson65] are collected in the following result regarding $\Pi ^1_1$ ordinals.

The proof of the previous estimations derives mainly from the following four lemmas, where WO $(\alpha )$ denotes the well-ordering of $\alpha $ .

Given the above results, we easily obtain.

Corollary 5.1. Over ${\textsf {RCA}}_0$ the following chain of implications is provable:

$$\begin{align*}HL \rightarrow HL(\omega) \leftrightarrow \forall n\, HL(n) & \rightarrow \dots \rightarrow HL(n+1) \ \rightarrow \ HL(n) \\ &\rightarrow \dots \rightarrow HL(2) \leftrightarrow DL. \end{align*}$$

The only proof-theoretical relation that does not derive immediately from the aforementioned results is the last one, namely ${\textsf {RCA}}_0\, \vdash \text {HL}(2) \leftrightarrow \text {DL}$ . This can be obtained indirectly through another result by Simpson [Reference Simpson65, Theorem X.3.20], that is, ${\textsf {RCA}}_0\, \vdash \text {DL} \leftrightarrow \text {WO}(\omega ^{\omega })$ ; nevertheless, we give a direct proof adapting to the framework of reverse mathematics a constructive proof originally proposed by J. Berger [Reference Berger6]. All the following definitions and results are stated or proved in ${\textsf {RCA}}_0$ .

Proof Denoted by $\mathbb {N}_{+}$ the set of positive integers and by $\{0,1\}^*_0$ the set of finite sequences of $0$ and $1$ starting with a $0$ , we actually prove the equivalence over ${\textsf {RCA}}_0$ of the two following statements:

${DL'}$ : for all n, $\mathbb {N}_{+}^n$ is a wqo;

${HL'(2)}$ : $\{ 0,1\}^*_0$ is a wqo;

whose equivalence with, respectively, “ $DL$ ” and “ $HL(2)$ ” is apparent.

We denote by $u,v,w$ the elements of $\{0,1\}_0^*$ , by i an element of $\{0,1 \}$ , by $n,m,k,l$ the elements of $\mathbb {N}$ and, with a harmless abuse of notation, by $0$ both the natural number and the string consisting only of the number $0$ . Moreover, $ui$ indicates the string obtained from u by adding as final letter i, and $|u|$ the length of u, that is, its number of letters. Over $\{0,1\}^{*}_0$ we define the quasi-order $\sqsubseteq $ given by subsequences, namely $v \! \sqsubseteq \! w$ if $v=v_1 \dots v_p,\ w=w_1\dots w_q$ and there exist $1 \! \leqslant r_1 \! < \dots <\! r_p \! \leqslant \! q$ such that $v_j \! = \! w_{r_j}$ for all $1 \! \leqslant \! j \! \leqslant \! p$ ; whereas over $\mathbb {N}^n_{+}$ let us consider the product order $\leqslant $ , that is, $(k_1, \dots k_n) \! \leqslant \! (k^{\prime }_1, \dots , k^{\prime }_n)$ if $k_j \! \leqslant k^{\prime }_j$ for all $1 \! \leqslant \! j \! \leqslant \! n$ .

We define the following function $\lambda \! : \! \{0,1\}_0^* \rightarrow \{0,1\}$ as:

$$\begin{align*}\lambda(0) \! := 0 \ \text{and} \ \lambda(ui) \! := i, \end{align*}$$

that is, $\lambda (w)$ is just the last letter of w.

Let us also define $\Phi \! : \! \{0,1\}^{*}_0 \rightarrow \mathbb {N}$ as

$$\begin{align*}\Phi(0) \! := 1 \ \ \text{and} \ \Phi(ui) \! := \left\{ \begin{array}{@{}ll} \Phi(u) & \text{if}\ \lambda(u)=i,\\ \Phi(u)+1 & \text{if}\ \lambda(u)\not=i. \end{array} \right. \end{align*}$$

$\Phi (w)$ is called the weight of w and amounts to the number of “blocks” of 0’s and 1’s in w, for example,

$$\begin{align*}\Phi(00)=1, \ \ \Phi(01100)=3, \ \ \Phi(011011100)=5. \end{align*}$$

Moreover, we inductively define $F \! :\! \{0,1\}^{*}_0 \rightarrow \bigcup _{n\! \geqslant \! 1}\mathbb {N}^n_{+}$ as

$$\begin{align*}F(0) & := 1\ \text{and, if}\ F(u)=(k_1, \dots, k_m),\ \text{then}\ \\ F(ui) & := \left\{ \begin{array}{@{}ll} (k_1, \dots, k_m+1) & \text{if}\ \lambda(u)=i,\\ (k_1, \dots, k_m, 1) & \text{if}\ \lambda(u)\not=i. \end{array} \right. \end{align*}$$

F is a bijection which converts a string of weight m into an m-tuple counting the occurrences of 0’s and 1’s, for example,

$$\begin{align*}F(00)=(2), \ \ F(01100)=(1,2,2),\ \ F(011011100)=(1,2,1,3,2). \end{align*}$$

Since we are dealing with finite sequences of natural numbers, $\lambda , \Phi $ , and F are all definable in ${\textsf {RCA}}_0$ .

Fixed $n\! \in \! \mathbb {N}_{+}$ , let $\mathcal {W}_n$ denote the elements of $\{0,1\}^*_0$ with weight n and $F_n$ the restriction of F to $\mathcal {W}_n$ ; given the previous definitions we obtain the following claim.

Claim 1. $F_n \! :\! \mathcal {W}_n \rightarrow \mathbb {N}^n_{+}$ is an order isomorphism between $(\mathcal {W}_n, \sqsubseteq )$ and $(\mathbb {N}^n_{+},\leqslant )$ .

Proof of Claim 1

It is easy to see that $F_n$ is a bijection since it converts a string of weight n into an n-tuple and the other way round. For what concerns the order, we proceed as follows. Let $u \sqsubseteq v$ with $u,v \in \mathcal {W}_n$ ; this means that $u,v$ are made by the same numbers of blocks of $0$ ’s and $1$ ’s (starting with $0$ ) and that both the lengths $|u|$ and $|v|$ are greater or equal to n. We adopt the following notation, let $B_j^{\Box }$ and $k_j^{\Box }$ (with $1 \! \leqslant \! j \! \leqslant \! n$ and $\Box \! \in \! \{u,v\}$ ) denote, respectively, the $j^{th}$ -block of $\Box $ and its length (in particular, $B_j^{\Box }$ is a non-empty finite string made entirely either by $0$ ’s or $1$ ’s); for example, $B_3^u$ is the third block of u and $k_3^u$ is the number of $0$ ’s composing it (since u starts with $0$ and thus the third block, as all the odd ones, is made of $0$ ’s). Let us observe that $F_n(u)=(k_1^u, \dots , k_n^u)$ and the same for v. Since $u \sqsubseteq v$ and $u,v \in \mathcal {W}_n$ , we obtain $B_j^{u} \sqsubseteq B_j^{v}$ , and thus $k_j^u \leqslant k_j^v$ , for all $1 \! \leqslant \! j \! \leqslant \! n$ ; namely, $F_n(u)=(k_1^u, \dots , k_n^u) \leqslant (k_i^v, \dots , k_n^v)=F_n(v)$ . For the other direction, if $k=(k_1, \dots , k_n) \leqslant (k^{\prime }_1, \dots , k^{\prime }_n)=k'$ , we can consider non-empty finite strings $B_j^k$ and $B_j^{k'}$ , with $1 \! \leqslant \! j \! \leqslant \! n$ , made, respectively, of $k_j$ and $k^{\prime }_j\, 0$ ’s (if j is odd) and $k_j$ and $k^{\prime }_j\, 1$ ’s (if j is even). Since $k_j \leqslant k^{\prime }_j$ , $B_j^k \sqsubseteq B_j^{k'}$ and, considering juxtaposition, $F_n^{-1}(k)=B_1^k\dots B_n^k \sqsubseteq B_1^{k'}\dots B_n^{k'}=F_n^{-1}(k')$ . This concludes the proof of Claim 1.

Finally, we define a length-normalizing function $G_n \! :\! \bigcup _{m\! \geqslant \! 1}\mathbb {N}^m_{+} \rightarrow \mathbb {N}^n_{+}$ as

$$\begin{align*}G_n(k_1, \dots, k_m) \! := \left\{ \begin{array}{@{}ll} (k_1, \dots, k_m, 1, \dots,1) & \text{if}\ m<n,\\ (k_1, \dots, k_n) & \text{if}\ n\! \leqslant \! m. \end{array} \right. \end{align*}$$

For $u\! \in \! \{0,1\}^*_0$ , let us set

(1) $$ \begin{align} u!_n \! := F_n^{-1}(G_n(F(u))). \end{align} $$

Proof of Claim 2

Straightforward.

Before the main result, we state and prove two other claims.

Claim 3. For all $v,w$ in $\{0,1\}^*_0$ , the following holds:

$$\begin{align*}( 2 \cdot |v| \! \leqslant \! \Phi(w) ) \ \Rightarrow \ v \sqsubseteq w.\\[-31pt] \end{align*}$$

Proof of Claim 3

Let us assume, by contradiction, that $v=v_1\dots v_n$ , $w=w_1\dots w_m$ with $\Phi (w)=k$ , $2n \! \leqslant \! k$ , but $v \! \not \sqsubseteq \! w$ . We consider the word $u=01\dots 01$ of length and weight $2n$ ; since for all $1 \! \leqslant \! j \! \leqslant \! n$ , $v_j=u_{2j-1}$ , or $v_j=u_{2j}$ , then $v \! \sqsubseteq \! u$ . Moreover, since $\Phi (u)=2n\! \leqslant \! k=\Phi (w)$ , we have that $u_j =\bar {w}_j$ where $\bar {w}_j$ is the first letter of the j-th block of w, and so $u\! \sqsubseteq \! w$ . Thus $v\! \sqsubseteq \! u \! \sqsubseteq \! w$ , contradiction. This concludes the proof of Claim 3.

Claim 4. For all $v,w$ in $\{0,1\}^*_0$ , we have

$$\begin{align*}\Phi(v) \! \leqslant \! \Phi(w) \! \leqslant \! n \, \wedge \, v!_n \! \sqsubseteq \! w!_n \ \Rightarrow \ v\! \sqsubseteq \! w.\\[-33pt] \end{align*}$$

Proof of Claim 4

Let $k=\Phi (v)$ . By $v!_n \! \sqsubseteq \! w!_n$ , we obtain $G_n(F(v)) \! \leqslant \! G_n(F(w))$ and therefore,

$$\begin{align*}F_k(v)=G_k(F(v)) \leqslant G_k(F(w))=F_k(w!_k), \end{align*}$$

thus,

$$\begin{align*}v\! \sqsubseteq \! w!_k. \end{align*}$$

Since $k\! \leqslant \! \Phi (w)$ , $w!_k \! \sqsubseteq \! w$ holds and, by transitivity, $v\! \sqsubseteq \! w$ . This concludes the proof of Claim 4.

We can now prove the main result of this section considering separately the two directions.

“ $HL'(2) \Rightarrow DL'$ ”: fix $n \! \in \! \mathbb {N}_{+}$ and an infinite sequence $f\! :\! \mathbb {N} \rightarrow \mathbb {N}^n_{+}$ . By applying $HL'(2)$ to $F_n^{-1}\circ f$ we obtain $k\! < \! l$ with

$$\begin{align*}F_n^{-1} \circ f(k) \sqsubseteq F_n^{-1} \circ f(l), \end{align*}$$

and thus, applying F, $f(k) \! \leqslant \! f(l)$ .

“ $DL' \Rightarrow HL'(2)$ ”: fix an infinite sequence $g\! :\! \mathbb {N} \rightarrow \{0,1\}^{*}_0$ and set $n=2 \cdot |g(0)|$ . Then, applying $DL'$ , we obtain $k\! < \! l$ such that

$$\begin{align*}(F_n(g(k)!_n),\Phi(g(k))) \leqslant (F_n(g(l)!_n),\Phi(g(l))). \end{align*}$$

If $n\! < \! \Phi (g(l))$ , then $g(0) \! \sqsubseteq \! g(l)$ holds by Claim 3. Otherwise, we have

$$\begin{align*}\Phi(g(k)) \leqslant \Phi(g(l)) \leqslant n \ \text{and} \ g(k)!_n \sqsubseteq g(l)!_n, \end{align*}$$

thus $g(k)\! \sqsubseteq \! g(l)$ by Claim 4.

6 Independence results

Arguably, among the greatest milestones in proof theory are Gödel’s incompleteness theorems [Reference Gödel36] regarding the unprovability, or equivalently the independence, of some statements over a mathematical theory; in the case of the second incompleteness theorem the consistency of Peano arithmetic over Peano arithmetic itself. The first concrete example of independence (i.e., a true, yet unprovable, statement with a numerical, rather than logical, content) was found in 1977 by Paris and Harrington [Reference Paris, Harrington and Barwise53]; since then, many other cases have been discovered [Reference Kirby and Paris41, Reference Simpson, Harrington, Morley, Šcedrov and Simpson63, Reference Smith, Harrington, Morley, Šcedrov and Simpson66].

Following the approach of [Reference Friedman and Weiermann30], we consider tree-like structures proving that the well quasi-orderedness of some, relatively simple, embeddability relations on these structures is not provable over relevant theories, such as Peano Arithmetic, PA, or Arithmetic Transfinite Recursion ${\textsf {ATR}}_0$ (see [Reference Simpson65] for a detailed presentation of ${\textsf {ATR}}_0$ ).

For what concerns notation let us define $2_0(l) \! : = l$ and $2_{k+1}(l) \! : = 2^{2_k(l)}$ , so that $2_k(l)$ is an iterated exponential function of height k with the number l at the highest position.

6.1 Independence results for Ackermannian terms

In this section, we treat independence results, over first- and second-order arithmetical theories, for tree-like structures built upon Ackermannian terms. First, let us consider a suitable version of the Ackermann function.

Definition 6.1. Let $a,b,k$ be integers with $k \! \geqslant \! 2$ , we define the following Ackermannian function $A_a(k,b) \! \in \! \mathbb {N}$ . Fix k and let us denote $A_a(k,b)$ by $A_ab$ with $A_a(-1) \! : = 1$ as auxiliary value, then $A_ab$ is recursively defined asFootnote ⁵ :

$$\begin{align*} A_0b & := k^b \\ A_{a+1}b & := A_{a}^k A_{a+1}(b-1) \\ A_{\omega}(k,b) & := A_bb \\ A_{\omega}(b) & := A_{\omega}(b,b). \end{align*}$$

Note that $A_0(k, 0) = 1$ regardless of k. Except for a few trivial cases, the Ackermann function increases strictly in each of its parameters. This can be confirmed by a straightforward inductive argument, which we leave to the reader.

Lemma 6.1. Let $a \leqslant a', b \leqslant b'$ , and $2 \leqslant k \leqslant k'$ be natural numbers. Then,

$$\begin{align*}\max\{a, b\} < A_a(k, b) \leqslant A_{a'}(k',b'). \end{align*}$$

If, moreover, $a + b + k < a' + b' + k'$ and $a' + b'> 0$ , then $A_a(k, b) < A_{a'}(k', b').$

Exploiting these functions, for a fixed $k \geqslant 2$ the following set $T_k$ of Ackermannian terms is definable.

Definition 6.2. Let $T_k$ be the least set of terms such that:

1. 1. $0 \in T_k$ ;

2. 2. if $\mathfrak {a},\mathfrak {b} \in T_k \setminus \{0\}$ , then $\mathfrak {a}+\mathfrak {b} \in T_k$ ;

3. 3. if $\mathfrak {a},\mathfrak {b} \in T_k$ , then $A_{\mathfrak {a}}(k,\mathfrak {b}) \in T_k$ .

Moreover, let $T \! : = \bigcup _{k}^{\infty } T_k$ be the set of all Ackermannian terms.

For $\mathfrak {a} \in T_k$ , the value of $\mathfrak {a}$ , denoted by $|\mathfrak {a}| \! \in \! \mathbb {N}$ , is inductively defined as follows: $|0| \! : = 0$ , $|\mathfrak {a}+\mathfrak {b}| \! : = |\mathfrak {a}| + |\mathfrak {b}|$ , and $|A_{\mathfrak {a}}(k,\mathfrak {b})| \! : = A_{|\mathfrak {a}|}(k,|\mathfrak {b}|)$ . Furthermore, since k is a parametric placeholder, given $k,h \geqslant 2$ a “base change” from elements of $T_k$ to elements of $T_h$ can be defined; more precisely, given $\mathfrak {a} \! \in \! T_k$ , $\mathfrak {a}[k\! : = h]$ indicates the element of $T_h$ obtained from $\mathfrak {a}$ by replacing every occurrence of k with h.

For each $k \geqslant 2$ , the elements of $T_k$ can be represented as ordered binary trees with the leaves labelled by $0$ and the inner nodes labelled by $+$ or $A_k$ . For example,

This connection allows to easily define the following relation on $T_k$ .

Definition 6.3. Let $\leqslant _k$ be the least binary relation on $T_k$ such that, for all $\mathfrak {a},\mathfrak {b},\mathfrak {c} \in T_k$ , the following properties hold:

1. 1. $ 0 \leqslant _k \mathfrak {a}$ ;

2. 2. if $\mathfrak {a} \leqslant _k \mathfrak {b}$ , then $\mathfrak {a} \leqslant _k \mathfrak {b}+\mathfrak {c}$ and $\mathfrak {a} \leqslant _k \mathfrak {c}+\mathfrak {b}$ ;

3. 3. if $\mathfrak {a} \leqslant _k \mathfrak {b}$ , then $\mathfrak {a} \leqslant _k A_{\mathfrak {b}}(k,\mathfrak {c})$ and $\mathfrak {a} \leqslant _k A_{\mathfrak {c}}(k,\mathfrak {b})$ ;

4. 4. if $\mathfrak {a} \leqslant _k \mathfrak {a}'$ and $\mathfrak {b} \leqslant _k \mathfrak {b}'$ , then $\mathfrak {a}+\mathfrak {b} \leqslant _k \mathfrak {a}' + \mathfrak {b}'$ and $A_{\mathfrak {a}}(k,\mathfrak {b}) \leqslant _k A_{\mathfrak {a}'}(k,\mathfrak {b}')$ .

Let us observe that if $\mathfrak {a} \leqslant _k \mathfrak {b}$ , then $|\mathfrak {a}| \leqslant |\mathfrak {b}|\! .$ Moreover, given the tree structure of its elements, $T_k$ is a proper subset of $\mathbb {T}(\bar {3})$ , with $\bar {3} \! : =\{0,+, A_k\}$ , and it is easy to see that $\mathfrak {a} \leqslant _k \mathfrak {b}$ if and only if $\mathfrak {a} \preccurlyeq \mathfrak {b}$ , where $\preccurlyeq $ is tree embeddability (see Definition 3.7).

The next definition introduces the first principle under scrutiny.

Definition 6.4. For a non-decreasing number-theoretic function f of two arguments, let $W(f)$ be the following assertion:

$$ \begin{align*} (\forall K)(\exists M)&(\forall \mathfrak{a}_0, \dots, \mathfrak{a}_M \in T) \big[(\forall i \leqslant M)[\mathfrak{a}_i \! \in \! T_{i+2} \wedge |\mathfrak{a}_i| \leqslant f(K,i)] \\ & \rightarrow (\exists i,j \leqslant M) \left( i < j \, \wedge \, \mathfrak{a}_i[i+2 \! := j+2] \leqslant_{j+2} \mathfrak{a}_j\right) \big]. \end{align*} $$

For what concerns the provability of $W(f)$ with respect to some specific functions f, we have the following two results.

Theorem 6.1. Let $d \geqslant 1$ be a natural number and fix $f_d(K,i) \! : = 2_{d-1}((i+2)^K)$ , then:

1. 1. $W(f_d)$ is true;

2. 2. $I\Sigma _d \, \nvdash \ W(f_d)$ .

Theorem 6.2. Let $f(K,i)\! : = A^K_{\omega }(i+2,0)$ Footnote ⁶ , then:

1. 1. $W(f)$ is true;

2. 2. ${\textsf {ATR}}_0\, \nvdash \ W(f)$ .

We consider, and prove, the following slight generalization. Denoted with $\mathbb {N}_{\geqslant 2}$ the set of integers greater than $1$ , let $t \!: \mathbb {N}_{\geqslant 2} \times \mathbb {N} \rightarrow T$ be a selection function sending $(i,n) \mapsto t_i(n) \in T_i$ with the only constraint that $|t_i(n)|=n$ . For any such selection function and any non decreasing number-theoretic function f of two arguments, let $W(t, f)$ be the following assertion:

$$ \begin{align*} &(\forall K)(\exists M)(\forall a_0, \dots, a_M \in \mathbb{N}) \big[(\forall i \leqslant M)[ a_i \leqslant f(K,i)] \\ & \quad\rightarrow (\exists i,j \leqslant M) \left( i < j \, \wedge \, t_{i+2}(a_i)[i+2 \! := j+2] \leqslant_{j+2} t_{j+2}(a_j)\right) \big]. \end{align*} $$

In particular, we consider the specific selection function that sends $(i,n)$ to the tree representation of the i-base Ackermannian normal form of n. More precisely, as detailed in [Reference Arai, Fernández-Duque, Wainer and Weiermann1] (see also [Reference Arai, Wainer and Weiermann2, Reference Fernández-Duque and Weiermann24, Reference Fernández-Duque and Weiermann25]), for a fixed $k \geqslant 2$ , every natural number n can be uniquely written in the form $A_a(k,b)+c$ , for suitable natural numbers $a,b,c \geqslant 0$ , if we impose some conditions (e.g., a is the smallest number such that $A_{a+1}(k,b)> n$ and b is the smallest one such that $A_a(k,b+1)> n$ ). Moreover, $a,b$ , and c can themselves be put into their k-base Ackermannian normal form and so on; we write $n =_k A_a(k,b)+c$ when $A_a(k,b)+c$ is the k-base Ackermannian normal form of n and $a,b,c$ are themselves in their normal form. Since the k-base Ackermannian normal form involves only addition and the function , it can be written as an element of $T_k$ ; for example, $0 \! =_2 \! 0, 1 \! =_2 \! A_00, 4 \! =_2 \! A_{A_00}0$ , and $2^{16}+1 \! =_2 \! A_{A_00}A_00 + A_00$ .

The aforementioned Ackermannian normal form and its associate selection function t enjoy the following two combinatorial properties: the former is the so-called base-change maximal property ensuring that the Ackermannian normal form maximizes the values with respect to change of base; the latter is a form of commutativity between the Ackermannian normal form and the base-change operation.

Lemma 6.2. Let t be the Ackermannian normal form selection function, then

• • $\forall k \! \geqslant \! 2 \ \forall \tau \! \in \! T_k\ \forall l \!> \! k \ \ |\tau [k:=l]| \, \leqslant \, \left |t_k(|\tau |)[k:=l]\right |$ ;

• • $\forall k \! \geqslant \! 2 \ \forall \tau \! \in \! T_k\ \forall l \!> \! k \ \ t_k(|\tau |)[k:=l] \, = \, t_l \big ( \left |t_k(|\tau |)[k:=l]\right | \big )$ .

Proof See [Reference Arai, Fernández-Duque, Wainer and Weiermann1, Reference Fernández-Duque and Weiermann25].

For such a selection function, we have the following independence results.

Theorem 6.3. Let $d \! \geqslant \! 1$ be a natural number; if $f_d(K,i) \! : = 2_{d-1}((i+2)^K)$ , then:

1. 1. $W(t,f_d)$ is true;

2. 2. $I\Sigma _d \, \nvdash \ W(t,f_d)$ .

Proof The proof is analogous to the one of the next theorem.

Theorem 6.4. Fix $f(K,i)\! : = A^K_{\omega }(i+2,0)$ , then

1. 1. $W(t,f)$ is true;

2. 2. ${\textsf {ATR}}_0\, \nvdash \ W(t,f)$ .

Proof 1 (Correctness). For a given K, choose M according to the following miniaturization of Kruskal’s theorem:

$$ \begin{align*} &(\forall K)(\exists M)(\forall t_0, \dots, t_M \in \mathbb{T}(\bar{3}))\\ &\left[(\forall i \leqslant M)[N(t_i) \leqslant 4 \cdot A^K_{\omega}(i+2,0) +1] \rightarrow (\exists i < j \leqslant M)[ t_i \preccurlyeq t_j]\right], \end{align*} $$

where, similarly as before, $\mathbb {T}(\bar {3})$ is the set of finite trees with labels in $\bar {3}=\{0,+,A_{x}\}$ and, for $t \! \in \! \mathbb {T}(\bar {3})$ , $N(t)$ is the number of nodes of t (see [Reference Friedman and Weiermann30, Reference Gallier32] for a proof of this statement). Let $a_0, \dots , a_M$ be a given sequence such that $a_i \! \leqslant \! A^K_{\omega }(i+2,0)$ , then $t_{i+2}(a_i)[i+2:=x] \! \in \! T_x \subseteq \mathbb {T}(\bar {3})$ and $N(t_{i+2}(a_i)[i+2:=x]) \leqslant 4 \cdot A^K_{\omega }(i+2,0) +1$ ; the last inequality holds since an Ackermannian term $\mathfrak {a}$ with value $|\mathfrak {a}| \leqslant \! A^K_{\omega }(i+2,0)$ , such as $t_{i+2}(a_i)$ , has less then $4 \cdot A^K_{\omega }(i+2,0) +1$ nodes when seen as a tree. This non optimal upper bound derives from the fact that writing a number n using just $1$ and $+$ required $2n-1$ symbols (i.e., nodes in a binary tree); in our case, each $1$ is written as $A_0(k,0)$ (two leaves labelled by $0$ and an inner node labelled by $A_k$ ) and thus requires in total $4n-1$ nodes. By the previous miniaturization of Kruskal’s theorem, there exist $i<j \leqslant M$ such that $t_{i+2}(a_i)[i+2:=x] \preccurlyeq t_{j+2}(a_j)[j+2:=x]$ , thus $t_{i+2}(a_i)[i+2 \! : = j+2] \leqslant _{j+2} t_{j+2}(a_j)$ . Let us observe that an easy adaptation of this strategy can readily be used to prove point 1. of Theorem 6.2.

2. (Unprovability). For $2 \! \leqslant \! h \! \leqslant \! l$ , let $a[h := l]$ be the result of replacing in the h-base Ackermannian normal form of a all occurrences of h by l; namely, if $a =_h A_r(h,p) + q$ , then $a[h := l] \! : = A_{r[h:=l]}(l, p[h:=l]) + q[h := l]$ . The unprovability result relies on the following claim.

Claim: Let $a_0 :=A^K_{\omega }(2,0)$ and $a_{i+1}:=a_i[i+2 :=i+3]-1$ , then:

1. 1. $\forall K\, \exists M'\ a_{M'}=0$ holds;

2. 2. ${\textsf {ATR}}_0\nvdash \, \forall K\, \exists M'\ a_{M'}=0$ .

Proof of the claim

See [Reference Arai, Fernández-Duque, Wainer and Weiermann1].

Let $f(K,i)\! :=A^K_{\omega }(i+2,0)$ and, for a given K, choose M according to $W(t,f)$ . Moreover, as in the claim, let $a_0=A^K_{\omega }(2,0)$ and $a_{i+1}=a_i[i+2:=i+3]-1$ ; then, $a_i \! \leqslant \! A^K_{\omega }(i+2,0)$ . Assume, by $W(t,f)$ , that there exist $i \! < \! j \! \leqslant \! M$ such that $t_{i+2}(a_i)[i+2 \! : = j+2] \leqslant _{j+2} t_{j+2}(a_j)$ ; then, $|t_{i+2}(a_i)[i+2 \! : = j+2]| \leqslant \left |t_{j+2}(a_j)\right |=a_j$ . Now we claim that, if $a_m \neq 0$ for all $0 \! \leqslant \! m \! \leqslant \! M$ , then $|t_{i+2}(a_i)[i + 2 := j + 2]| \!> \! |t_{j+2}(a_j)|$ . This contradiction shows that $W(t, f)$ implies $\forall K\, \exists M' \, a_{M'}=0$ , thus ${\textsf {ATR}}_0$ does not prove $W(t,f)$ for $f(K,i)\! :=A^K_{\omega }(i+2,0)$ . The claim is proved by induction on $k \!> \! i$ . Let $k=i+1$ , then $|t_{i+2}(a_i)[i+2:=i+3]|=|t_{i+2}(a_i)|[i+2:=i+3]=a_i[i+2:=i+3]>a_i[i+2:=i+3]-1=a_{i+1}=|t_{i+3}(a_{i+1})|$ ; the first equality derives from the choice of t, that is, $t_{i+2}(a_i)$ is the (tree representation of the) $i+2$ -base Ackermannian normal form of $a_i$ (see Lemma 6.2). The induction step, $k \rightarrow k+1$ , is proved analogously, exploiting the fact that $a_k [k+2 := k+3]> a_k [k+2 := k+3]-1 = a_{k+1} = |t_{k+3}(a_{k+1})|$ .

Lastly, we prove the equivalence between $W(f)$ and $\forall t\, W(t,f)$ ; since, by the previous theorem ${\textsf {ATR}}_0\nvdash \, \forall t\, W(t,f)$ , this implies that ${\textsf {ATR}}_0\, \nvdash W(f)$ .

Proposition 6.1 ( ${\textsf {ATR}}_0$ ).

Let f be a non-decreasing number-theoretic function of two arguments, then $W(f)$ and $\forall t\, W(t, f)$ are equivalent.

Proof $"W(f) \Rightarrow \forall t\, W(t,f)$ ” Let t be any selection function, we need to prove that

$$ \begin{align*} &(\forall K)(\exists M)(\forall a_0, \dots, a_M \in \mathbb{N}) \big[(\forall i \leqslant M)[ a_i \leqslant f(K,i)] \\& \qquad \rightarrow (\exists i,j \leqslant M) \left( i < j \, \wedge \, t_{i+2}(a_i)[i+2 \! := j+2] \leqslant_{j+2} t_{j+2}(a_j)\right) \big]. \end{align*} $$

Let $K \! \in \! \mathbb {N}$ , M be given as in $W(f)$ and consider a finite sequence $a_0, \dots , a_M\! \in \mathbb {N}$ such that, for all $i \! \leqslant \! M$ , $a_i \! \leqslant \! f(K,i)$ ; then, the finite sequence of Ackermannian terms $t_2(a_0), \dots , t_{M+2}(a_M)$ satisfies the hypotheses of $W(f)$ , that is, $t_{i+2}(a_i) \! \in \! T_{i+2} \wedge |t_{i+2}(a_i)|=a_i \leqslant f(K,i)$ for all $i \leqslant M$ . Let $i<j \leqslant M$ as given by $W(f)$ , we obtain $t_{i+2}(a_i)[i+2:=j+2] \leqslant _{j+2} t_{j+2}(a_j)$ ; thus $W(t,f)$ holds.

$"\forall t\, W(t,f) \Rightarrow W(f)$ ” We reason by contradiction assuming $\neg W(f)$ , namely,

$$ \begin{align*} &(\exists \bar{K})(\forall M)(\exists \tau_0, \dots, \tau_M \in T) \big[(\forall i \leqslant M)[\tau_i \! \in \! T_{i+2} \wedge |\tau_i| \leqslant f(\bar{K},i)] \\&\qquad\quad \wedge (\forall i <j \leqslant M) \left(\tau_i[i+2 \! := j+2] \not\leqslant_{j+2} \tau_j\right) \big]. \end{align*} $$

Thus, for every M, we can find a “bad sequence” $\tau _0, \dots , \tau _M$ such that, for all $i \leqslant M$ , $\tau _i \in T_{i+2}$ and $|\tau _i| \leqslant f(\bar {K},i)$ , but $\tau _i[i+2 \! : = j+2] \not \leqslant _{j+2} \tau _j$ for all $i<j \leqslant M$ . Since such sequences are closed under initial segments and, for every i, there are finitely many terms $\tau $ in $T_{i+2}$ such that $|\tau | \leqslant f(\bar {K},i)$ , this type of bad sequences form a finitely branching infinite tree. By König’s lemma, we can obtain an infinite sequence $\tau _0, \tau _1, \dots $ such that $\tau _i \in T_{i+2}$ and $|\tau _i| \leqslant f(\bar {K},i)$ for all i, and $\tau _i[i+2 \! : = j+2] \not \leqslant _{j+2} \tau _j$ for all $i<j$ . Given such sequence, we consider the following selection function s, where $t^{NF}$ is the Ackermannian normal form selection function

$$\begin{align*}s(i+2,n) \! := \left\{ \begin{array}{@{}ll} \tau_i & \text{if}\, n=|\tau_i|, \\t_{i+2}^{NF}(n) & \text{otherwise}. \end{array} \right. \end{align*}$$

From $W(s,f)$ , with respect to $\bar {K}$ , we obtain a value $M_{\bar {K}}$ such that

$$ \begin{align*} &(\forall a_0, \dots, a_{M_{\bar{K}}} \in \mathbb{N}) \big[(\forall i \leqslant M_{\bar{K}})[ a_i \leqslant f(\bar{K},i)] \\& \qquad\qquad \rightarrow (\exists i < j \leqslant M) \left( s_{i+2}(a_i)[i+2 \! := j+2] \leqslant_{j+2} s_{j+2}(a_j)\right) \big]. \end{align*} $$

Applying this property to the sequence $|\tau _0|, |\tau _1|, \dots , |\tau _{M_{\bar {K}}}|$ , there are indexes $i < j \leqslant M_{\bar {K}}$ such that

$$\begin{align*}\tau_i[i+2:=j+2]=s_{i+2}(|\tau_i|)[i+2:=j+2] \leqslant_{j+2} s_{j+2}(|\tau_j|) = \tau_j \end{align*}$$

which contradicts our hypothesis.

6.2 Independence results for exponential expressions

In this paragraph, we treat an independence result over Peano arithmetic regarding exponential expressions.

Definition 6.5. Let $EXP$ be the least set of terms in one variable x such that:

1. 1. $0 \in EXP$ ;

2. 2. if $\mathfrak {a},\mathfrak {b} \in EXP$ , then $x^{\mathfrak {a}} + \mathfrak {b} \in EXP$ .

For $\mathfrak {a} \in EXP$ and a positive integer k, we denote by $\mathfrak {a}(k)$ the integer value of the term $\mathfrak {a}$ when the variable x is set to k; namely, $\mathfrak {a}(k)$ is inductively defined as: $\mathfrak {a}(k)\! : = 0$ if $\mathfrak {a} \equiv 0$ , and $\mathfrak {a}(k)\! : = k^{\mathfrak {c}(k)} + \mathfrak {b}(k)$ if $\mathfrak {a} \equiv x^{\mathfrak {c}} +\mathfrak {b}$ . Moreover, $\mathfrak {a}(\omega )$ indicates the ordinal, smaller than $\varepsilon _0$ , obtained by replacing x with $\omega $ and interpreting $+$ as the natural sum between ordinals (see [Reference Bachmann4] for the definition of natural sum). Lastly, similar to how we defined the exponential iteration with base $2$ , let us define $\omega _0 \! : = 1$ and $\omega _{k+1} \! : = \omega ^{\omega _k}$ , so that $\omega _k$ is an $\omega $ -tower of height k.

Our goal is to study a slow well-ordering principle.

Definition 6.6. Let $SWO$ be the following assertion:

$$ \begin{align*} &(\forall K)(\exists M)(\forall \mathfrak{a}_0, \dots, \mathfrak{a}_M \in EXP)\\&\quad \left[(\forall i \leqslant M)[\mathfrak{a}_i(2) \leqslant 2_K(i)] \rightarrow (\exists j < M)[\mathfrak{a}_j(2_K(M)) \leqslant \mathfrak{a}_{j+1}(2_K(M))]\right]. \end{align*} $$

For what concerns the provability of $SWO$ , we obtain the next independence result.

Theorem 6.5.

1. 1. $SWO$ is true;

2. 2. $\textsf {PA} \nvdash \, SWO$ .

Proof 1 (Correctness). The truth of $SWO$ follows from the corresponding result for $\varepsilon _0$ with respect to the maximal coefficient. Namely, we consider the following statement:

(2) $$ \begin{align} &(\forall K)(\exists M)(\forall \alpha_0, \dots, \alpha_M \leqslant \varepsilon_0) \notag\\&\qquad\qquad \big[(\forall i \leqslant M)[|\alpha_i|\leqslant 2_K(i)] \rightarrow (\exists j < M)[\alpha_j \leqslant \alpha_{j+1}]\big], \end{align} $$

where, for an ordinal $\alpha < \varepsilon $ in Cantor normal form (i.e., $\alpha = \omega ^{\alpha _1} \cdot a_1 + \dots + \omega ^{\alpha _r} \cdot a_r$ with $\varepsilon _0 \!> \! \alpha _1 \! > \! \dots \! > \! \alpha _r$ and $a_1, \dots , a_r \! \in \! \mathbb {N}_{+}$ ), the maximal coefficient $|\alpha |$ is recursively defined as $|\alpha | \! : = \max \{|\alpha _1|, \dots , |\alpha _r|, a_1, \dots , a_r\}$ (see [Reference Smith, Harrington, Morley, Šcedrov and Simpson66] for the proof of (2)). Let K be given and choose M with respect to (2). If $\mathfrak {a}_0, \dots , \mathfrak {a}_M$ is a sequence in $EXP$ such that $\mathfrak {a}_i(2) \leqslant 2_K(i)$ for all $i \leqslant M$ , then $\mathfrak {a}_i(\omega )$ is a sequence of ordinals less than $\varepsilon _0$ such that the maximal coefficient of $\mathfrak {a}_i(\omega )$ is bounded by $\mathfrak {a}_i(2)$ , hence by $2_K(i)$ . The assertion for the maximal coefficient yields the existence of a natural number $j < M$ such that $\mathfrak {a}_j(\omega ) \leqslant \mathfrak {a}_{j+1}(\omega )$ . We have $\mathfrak {a}_i(2) \leqslant 2_K(i)$ for all $i \leqslant M$ , therefore the maximal coefficient of $\mathfrak {a}_j(\omega )$ is strictly smaller than $2_K(M)$ . For the last step of correctness, we rely on some properties of the slow-growing hierarchy G that, up to $\varepsilon _0$ , is inductively defined as: $G_{0}(x) \! : = 0, G_{\alpha +1}(x) \! : = G_{\alpha }(x) +1$ , and $G_{\lambda }(x) \! : = G_{\lambda [x]}(x)$ if $\lambda $ is a limit ordinal.Footnote ⁷ In our case, we find $G_{\mathfrak {a}_j(\omega )}(2_K(M)) \leqslant G_{\mathfrak {a}_{j+1}(\omega )}(2_K(M))$ and, since $G_{\mathfrak {a}_j(\omega )}(2_K(M)) = \mathfrak {a}_j(2_K(M))$ and $G_{\mathfrak {a}_{j+1}(\omega )}(2_K(M)) = \mathfrak {a}_{j+1}(2_K(M))$ , the conclusion follows. The two required properties of the slow-growing hierarchy G, namely $\alpha \! \leqslant \! \beta , |\alpha | \! \leqslant \! x \Rightarrow G_{\alpha }(x) \leqslant G_{\beta }(x)$ and $G_{\alpha }(x) = \alpha [\omega \! : = x]$ , are proved in [Reference Meskens, Weiermann, Kahle and Rathjen48, Lemma 6].

2. (Unprovability) Assume $K \geqslant 2$ . Let us define $\alpha _0 \! : = \omega _{K-2}$ and $\alpha _{i+1} \! : = \alpha _i[i]$ , and let N be the least i such that $\alpha _i = 0$ ; then PA does not prove $\forall K\, \exists N\, \alpha _N \! = \! 0$ [Reference Buchholz, Cichon and Weiermann9]. The maximal coefficient of $\alpha _i$ is smaller than i for all $0 < i \leqslant M$ and, since $\alpha _i < \alpha _0$ , we find $G_{\alpha _i}(i) < G_{\omega _K}(i) \leqslant 2_K(i)$ .

Put $\mathfrak {a}_i \! : = \alpha _i[\omega := x]$ , that is, any occurrence of $\omega $ in $\alpha _i$ is replaced by x; then $\mathfrak {a}_i \in EXP$ . Moreover, for $i \geqslant 2$ we obtain $\mathfrak {a}_i(2) \leqslant \alpha _i[\omega := 2] = G_{\alpha _i}(2) \leqslant G_{\alpha _i}(i) \leqslant G_{\omega _K}(i) \leqslant 2_K(i)$ ; while, for $i < 2$ , $\mathfrak {a}_i(2) \leqslant 2_K(i)$ can be found by direct evaluation. Let us apply $SWO$ to K in order to obtain an appropriate M, and assume, to reach a contradiction, that $\alpha _M \neq 0$ , that is, $\alpha _i \!> \! \alpha _{i+1}$ for all $i < M$ . If we consider the sequence $\mathfrak {a}_i$ , on the one hand we obtain, by $SWO$ , that there exists an $j < M$ such that $\mathfrak {a}_j(2_K(M)) \leqslant \mathfrak {a}_{j+1}(2_K(M))$ . On the other hand, we have that $\alpha _i\!>\! \alpha _{i+1}$ , and the maximal coefficient of $\alpha _i$ is strictly bounded by $2_K(M)$ which leads to $G_{\alpha _i}(2_K(M))> G_{\alpha _{i+1}}(2_K(M))$ . Hence $\mathfrak {a}_j(2_K(M))> \mathfrak {a}_{j+1}(2_K(M))$ , contradiction. This shows that $SWO$ implies $\forall K\, \exists N\, \alpha _N =0$ and thus, PA does not prove $SWO$ .

7 Related and future work

Well quasi-orders have been extensively studied in the recent decades, with fruitful applications in algebra [Reference Aschenbrenner and Pong3], graph theory [Reference Pouzet and Riva54], logic (remarkably proof theory [Reference Simpson, Harrington, Morley, Šcedrov and Simpson63]), and even theoretic computer science (e.g., for term rewriting [Reference Dershowitz20–Reference Dershowitz, Okada and Gurevich22] and program termination [Reference Blass and Gurevich7]). For a general introduction and an historical survey, we refer, respectively, to [Reference Kruskal44, Reference Milner and Rival49]; whereas for a recent collection that illuminates the multifaceted nature of wqo, we refer to [Reference Schuster, Seisenberger and Weiermann60].

For what concerns Higman’s lemma, recent investigations, particularly in reverse mathematics, are related to its extension called “generalized Higman’s lemma”. As previously said, well quasi-orders are not preserved under infinitary operations, such as infinite sequences; to overcome this obstacle better quasi-orders, bqo, have been introduced [Reference Nash-Williams52]. Involving bqo, the generalized Higman’s lemma reads as follows: “if Q is a bqo, then $Q^*$ is a bqo”. It can be proved (see, e.g., [Reference Marcone, Schuster, Seisenberger and Weiermann46, Theorem 6.21]) that the generalized Higman’s lemma is actually equivalent to the celebrated Nash-Williams’ theorem [Reference Nash-Williams52]: denoted with $\tilde {Q}$ the set of countable sequences over Q, that is, transfinite sequences of countable length, Nash-Williams’ theorem states that “if Q is a bqo, then $\tilde {Q}$ is a bqo”.

Regarding Kruskal’s theorem, the latest developments, attributed to Anton Freund, Patrick Uftring, and collaborators [Reference Freund26–Reference Freund and Uftring29, Reference Uftring69], primarily focus on the so-called “uniform Kruskal theorem”. This theorem extends the classical result for trees to encompass general recursive data types and incorporates Girard’s dilator theory [Reference Girard33, Reference Girard34], giving it a pronounced categorical character. It is worth mentioning also the rich literature related to constructive proofs of Higman’s lemma [Reference Coquand and Fridlender19, Reference Murthy, Russell and Mitchel50, Reference Richman and Stolzenberg58, Reference Seisenberger, Callaghan, Luo, McKinna and Pollack61] and Kruskal’s theorem [Reference Seisenberger, Schuster, Berger and Osswald62, Reference Veldman70]. The most recent result in this stream is a novel version of Higman’s lemma relative to bars [Reference Berardi, Buriola, Schuster, Murano and Silva5].

For what concerns independence results, the ancestors are obviously Gödel’s incompleteness theorems [Reference Gödel36]. Despite the fundamental theoretical relevance of Gödel’s achievement, the first example of a concrete mathematical statement independent from PA was only discovered in 1977 by Paris and Harrington [Reference Paris, Harrington and Barwise53]. Following their finding, many other independence results have been discovered [Reference Kirby and Paris41, Reference Simpson, Harrington, Morley, Šcedrov and Simpson63, Reference Smith, Harrington, Morley, Šcedrov and Simpson66]. In more recent years, the study of independence results exposes the so-called “phase transition” phenomenon in logic [Reference Gordeev and Weiermann37, Reference Weiermann71] where the shift from provability to unprovability is characterized by a sharp threshold.

With respect to future developments regarding Kruskal’s theorem, the proof-theoretic work of Rathjen and Weiermann [Reference Rathjen and Weiermann57] continues to serve as a guiding reference. Beyond calculating its proof ordinal, namely ${\textsf {RCA}}_0\, \vdash \text {KT}(\omega ) \leftrightarrow \text {WO}\left ( \vartheta (\Omega ^{\omega }) \right )$ , they characterized the proof-theoretic strength of Kruskal’s theorem for unlabelled trees in terms of reflection principles.

Theorem 7.1. (Rathjen and Weiermann)

$$\begin{align*}\text{RCA}_0 \vdash \, \text{KT}(\omega) \leftrightarrow \Pi^1_1\text{-}RF\!N(\Pi^1_2\text{-}BI_0), \end{align*}$$

where $\Pi ^1_1\text {-}RFN(\Pi ^1_2\text {-}BI_0)$ stands for the uniform reflection principle for $\Pi ^1_1$ formulas of the theory $\Pi ^1_2\text {-}BI_0$ , which amounts to ${\textsf {RCA}}_0$ extended with bar induction for $\Pi ^1_2$ formulas (see [Reference Rathjen and Weiermann57, Section 11] for more details).

As a result, the next step is to achieve a comparable classification for K $\text {T}_\ell (\omega )$ as well as $\forall n\,\text {K}\text {T}_\ell (n)$ . Currently, we have the following two conjectures.

Further research in this area will be needed to expand the current results to encompass other embeddability relationships between trees, such as Friedman’s gap condition [Reference Freund26, Reference Kriz42].

For what concerns independence results, if terms for the Ackermann function are added to $EXP$ , we expect to achieve an independence result for ${\textsf {ATR}}_0$ ; moreover, integrating terms for the fast-growing hierarchy $(F_{\alpha })_{\alpha <\varepsilon _0}$ should lead to independence results for $ID_1$ .

8 Conclusion

This article has treated the proof-theoretic relations between Higman’s and Kruskal’s theorems in the framework of reverse mathematics considering both their finite and infinite versions. After a brief summary of wqo theory in reverse mathematics, including also novel results regarding the closure of wqo under order-preserving and order-reflecting functions, the main elements of Higman’s and Kruskal’s theorems, namely ordered algebras and labelled trees, have been introduced. The equivalence between the finite versions of the two theorems, denoted, respectively, as $\forall n$ HT $(n)$ and $\forall n$ K $\text {T}_\ell (n)$ , has been thoroughly presented, followed by the salient points for the infinitary case, that is, HT $(\omega )$ and K $\text {T}_\ell (\omega )$ . The previous equivalences, together with some other recent findings related to Kruskal’s theorem, have been summarized in an exhaustive schema depicting the proof-theoretic relations over ${\textsf {RCA}}_0$ of the results under consideration. Furthermore, also the connections between Higman’s lemma and Dickson’s lemma have been scrutinized, collecting the main references concerning their relations and proof-theoretic ordinals.

In addition, and enriching previous findings, some independence results over first- and second-order theories were treated. In particular, tree-like structures, involving either Ackermannian terms or exponential expressions, have been studied unveiling well-foundedness properties that are independent from Peano arithmetic and relevant fragments of second-order arithmetic.

Finally, two conjectures regarding the proof-theoretic strength of the aforementioned versions of Kruskal’s theorems with labels have been stated.