THE MAXIMAL LINEAR EXTENSION THEOREM IN SECOND ORDER ARITHMETIC

ALBERTO MARCONE AND RICHARD A. SHORE

Abstract. We show that the maximal linear extension theorem for well partial orders is equivalent over RCA_{0} to ATR_{0}. Analogously, the maximal chain theorem for well partial orders is equivalent to ATR_{0} over RCA_{0}.

1. Introduction

A wpo (well partial order) is a partial order (P, ≤_{P}) such that for every infinite sequence (x_{i}) of elements of P we can find i < j with x_{i} ≤_{P} x_{j}. This notion emerged several times in mathematics, as reported in [Kru72].

There are many characterizations of wpo’s, supporting the claim that this is indeed a very natural notion. Wpo’s are exactly the partial orders such that any nonempty subset has a finite set of minimal elements, or those which are well founded and contain no infinite antichains. For the purpose of this paper, the most important characterization of wpo’s is the one stating that a partial order is a wpo if and only if all its linear extensions (see Definition 2.4) are well-orders.

We mention here only two major results about wpo’s and wqo’s (see below for the distinction between these two notions). Fraïssé’s conjecture states that embeddability on countable linear orders is a wqo. Laver’s proved this in [Lav71] by establishing a stronger statement using Nash-Williams’ notion of better-quasi-order ([NW68]). Robertson and Seymour proved in a long list of papers culminating in [RS04] (see [Tho95, §5] for an overview) that the minor relation on finite graphs is a wpo.

Date: Saved: January 18, 2011. Compiled: January 18, 2011.

1991 Mathematics Subject Classification. Primary: 03B30; Secondary: 06A07.

Marcone’s research was partially supported by PRIN of Italy. Part of this work was carried out while Shore was a GNSAGA Visiting Professor at the Department of Mathematics and Computer Science “Roberto Magari” of the University of Siena.

He was also partially supported by NSF Grant DMS-0852811 and Grant 13408 from the John Templeton Foundation. We thank Andreas Weiermann for some useful bibliographic references. We thank the anonymous referee for pointing out an error in an earlier version of the proof of Theorem 6.4.

The characterization of wpo’s in terms of linear extensions leads to the following natural definition.

Definition 1.1. If P is a wpo, its maximal order type o(P) is the supremum of all ordinals which are order types of linear extensions of P.

The following theorem was originally proved by de Jongh and Parikh ([dJP77]).

Theorem 1.2. If P is a wpo, the supremum in the definition of o(P) is actually a maximum, i.e. there exist a linear extension of P with order type o(P). Such a well-order is called a maximal linear extension of P.

An exposition of (essentially) the original proof appears in [Har05, §8.4]. A proof of Theorem 1.2 based on the study of the partial order of the initial segments of P is included in [Fra00, §4.11]. Kříž and Thomas ([KT90, Theorem 4.7]) and Blass and Gurevich ([BG08, Proposition 52]) gave proofs with a strong set-theoretic flavor.

In any well founded partial order (and in particular in a wpo), one can look at chains (i.e. linear suborderings of the partial order) and give the following definition.

Definition 1.3. If P is a well founded partial order, its height χ(P) is the supremum of all ordinals which are order types of chains in P.

The following theorem is contained in [KT90, Theorem 4.9]. Kříž and Thomas attribute the result and the proof to Wolk ([Wol67, Theorem 9]), whose statement is actually a bit stronger (see Theorem 6.5 below).

Theorem 1.4. If P is a wpo, the supremum in the definition of χ(P) is actually a maximum, i.e. there exist a chain in P with order type χ(P). Such a well-order is called a maximal chain in P.

Wolk’s result appears also in Harzheim’s book ([Har05, Theorem 8.1.7]). The result was extended to a wider class of well founded partial orders by Schmidt ([Sch81]) in the countable case, and by Milner and Sauer ([MS81]) in general.

In this paper we study Theorems 1.2 and 1.4 from the viewpoint of reverse mathematics. The goal of reverse mathematics is to calibrate the proof-theoretic strength of mathematical statements by establishing the subsystem of second order arithmetic needed for their proof. We refer the reader to [Sim09] for background information on reverse mathematics and the relevant subsystems of second order arithmetic. The weakest subsystem is RCA_{0}, which consists of the axioms of ordered semi-ring, plus Δ_{1}^{0} comprehension and Σ_{1}^{0} induction. Adding set-existence axioms to RCA_{0} we obtain WKL_{0}, ACA_{0}, ATR_{0}, and Π_{1}^{1}-CA_{0}, completing the so-called “big five” of reverse mathematics. In this paper we deal with RCA_{0}, ACA_{0}, and ATR_{0}. ACA_{0} is obtained by adding to RCA_{0} the axiom scheme of arithmetic comprehension, while ATR_{0} further extends ACA_{0} by allowing transfinite iterations of arithmetic comprehension. ATR_{0} implies Δ_{1}^{1} comprehension ([Sim09, Lemma VIII.4.1]) and hence Δ_{1}^{1} transfinite induction.

The question of the proof-theoretic strength of Theorem 1.2 was raised by the first author in the Open Problems session of the workshop “Computability, Reverse Mathematics and Combinatorics” held at the Banff International Research Station (Alberta, Canada) in December

2008 (a list of those open problems is available at http://www.math.cornell.edu/~shore/papers/pdf/BIRSProb91.pdf).

Denoting by MLE and MC the formal versions (to be defined precisely in Section 2 below) of Theorems 1.2 and 1.4 we can state the main results of the paper.

Theorem 1.5. Over RCA_{0}, the following are equivalent:

(1) ATR_{0};

(2) MLE;

(3) MLE restricted to disjoint unions of two linear orders.

Theorem 1.6. Over RCA_{0}, the following are equivalent:

(1) ATR_{0};

(2) MC;

(3) MC restricted to disjoint unions of two linear orders.

Theorem 1.5 is connected to the following results which are due to Antonio Montalbán ([Mon07]).

Theorem 1.7. Every computable wpo has a computable maximal linear extension, yet there is no hyperarithmetic way of computing (an index for) a computable maximal linear extension from (an index for) the computable wpo.

Notice that the first part of Theorem 1.7 does not imply that Theorem 1.2 is true in the ω-model of computable sets (in fact Theorem 1.5 implies that this is not the case), as there exists computable partial orders which are not wpo’s but that “look” wpo’s in that model. The second part of Theorem 1.7 suggests ATR_{0} as a lower bound for the strength of Theorem 1.2. However we are not able to use Montalbán’s proof (which assumes Theorem 1.2) in our proof of (2) ⟹ (1) of Theorem 1.5.

Theorem 1.2 obviously suggests explicitly computing the maximal order types of different wpo’s. In [dJP77] de Jongh and Parikh already computed the maximal order type of the wpo investigated by Higman ([Hig52]). Immediately afterwards Schmidt studied maximal order types in her Habilitationsschrift ([Sch79]) and she gave upper bounds for the maximal order types of the wpo’s investigated by Kruskal ([Kru60]) and Nash-Williams ([NW65]) (although the latter proof is flawed and apparently has not been fixed yet). Much more recently the first author and Montalbán ([MM09]) computed the maximal order type of the scattered linear orders of finite Hausdorff rank under embeddability.

The use of maximal order types to calibrate the strength of statements about wpo’s in reverse mathematics is crucial. Harvey Friedman (see [Sim85]) used the maximal order type of the relevant wpo to prove that Kruskal’s theorem cannot be proved in ATR_{0}. Further extensions of Friedman’s method were then used to show that Robertson and Seymour’s result about graph minors is not provable in Π_{1}^{1}-CA_{0} ([FRS87]). Steve Simpson ([Sim88]) used the maximal order type (computed by way of “reifications”) of certain wpo’s to establish the strength of the Hilbert basis theorem. In [MM09] the computation of the maximal order type of the scattered linear orders of finite Hausdorff rank is instrumental in the reverse mathematics results about the restriction of Fraïssé’s conjecture to those linear orders.

Let us mention that in the literature the notion of wqo is probably more common than that of wpo. Well quasi orders are defined by applying the definition of wpo given above to a quasi order (i.e. a binary relation which is reflexive and transitive, but not necessarily anti-symmetric). Since a quasi order can always be turned into a partial order by taking the quotient with respect to the equivalence relation induced by the quasi order, there is nothing lost in dealing with wpo’s rather than wqo’s. Moreover, for the purposes of this paper it is more convenient to deal with partial orders (e.g. the definition of linear extension of a quasi order is more cumbersome).

We now explain the organization of the paper. In Section 2 we detail the formalization of partial and linear orders in subsystems of second order arithmetic and define MLE. In Section 3 we begin the proof of Theorem 1.5 by showing that ATR_{0} proves MLE. Our proof of MLE is related to the proof of Theorem 1.2 in [KT90] and in some sense simpler than those of [dJP77] and [Har05]. In Section 4 we start the proof of the reversal by showing that RCA_{0} + MLE implies ACA_{0}. The reversal is completed in Section 5 by arguing in ACA_{0} that MLE implies ATR_{0}. In these two sections MLE is applied only to partial orders which are the disjoint union of two linear orders. In Section 6 we prove Theorem 1.6. To show that ATR_{0} proves MC we apply the ideas of Section 3 to chains (the resulting proof is similar to the proof of Theorem 1.4 in [Sch81]), while the reversal (in which MC is applied to a disjoint union of two linear orders) is straightforward.

2. Partial and linear orders in subsystems of second order arithmetic

The formalization of the notion of linear order in subsystems of second order arithmetic is straightforward and can be carried out in RCA_{0} (see e.g. [Mar05]). We typically write L = (L, ≤_{L}) to denote a linear order defined on the set L with order relation ≤_{L}. The corresponding irreflexive relation is denoted by <_{L}. If x ∈ L we write L_{(≤_{L}x)} = { y ∈ L | y ≤_{L} x }. Similarly, L_{(≥_{L}x)} = { y ∈ L | y ≥_{L} x }. If x, y ∈ L we write [x, y]_{L} to denote the set { z ∈ L | x ≤_{L} z ≤_{L} y }. A specific linear order is ω = (ℕ, ≤).

In RCA_{0} we define well-orders as the linear orders which have no descending chains. In [Hir05a] Hirst studied the equivalence between this definition of well-order and other possible (classically equivalent) definitions. An element of a well-order is often identified with the restriction of the well-order to the strict predecessors of the element. For a survey of the provability of results about well-orders in subsystems of second order arithmetic see [Hir05b].

An important relation between linear orders is embeddability: L_{0} embeds into L_{1} (and we write L_{0} ⪯ L_{1}) if there exists an order preserving function (also called an embedding) from the domain of L_{0} to the domain of L_{1}. We write L_{0} ≡ L_{1} when L_{0} ⪯ L_{1} ⪯ L_{0}, and L_{0} ≺ L_{1} when L_{0} ⪯ L_{1} and L_{1} ⪯̸ L_{0}. The following Theorem shows that ATR_{0} is necessary to show that well orders are comparable under embeddability. (The equivalence between (1) and (2) is proved in [FH90], while the equivalence between (1) and (3) was obtained in [Sho93].) Theorem 2.1. Over RCA_{0}, the following are equivalent:

(1) ATR_{0};

(2) if L_{0} and L_{1} are well-orders then either L_{0} ⪯ L_{1} or L_{1} ⪯ L_{0};

(3) if for every n L_{n} is a well-order then there exist i ≠ j such that L_{i} ⪯ L_{j}.

An immediate, yet very useful, consequence of comparability of wellorders is the following.

Corollary 2.2. In ATR_{0} if L_{0} and L_{1} are well-orders the formulas L_{0} ⪯ L_{1}, L_{0} ≺ L_{1} and L_{0} ≡ L_{1} are Δ_{1}^{1}.

Proof. The formula L_{0} ⪯ L_{1} is clearly Σ_{1}^{1}. In ATR_{0}, by Theorem 2.1, if L_{0} and L_{1} are well-orders L_{0} ⪯ L_{1} is equivalent to L_{1} + 1 ⪯̸ L_{0}. The latter formula is clearly Π_{1}^{1}, and hence L_{0} ⪯ L_{1} is Δ_{1}^{1}.

¿From this and the definitions it follows that L_{0} ≺ L_{1} and L_{0} ≡ L_{1} are also Δ_{1}^{1}. □

In RCA_{0} we can define basic operations on linear orders. Suppose L_{n} = (L_{n}, ≤_{L_{n}}) is a linear order for every n. We may also assume that the L_{n}’s are pairwise disjoint. Then we define the linear order L_{0} + L_{1} = (L_{0} ∪ L_{1}, ≤_{L_{0}+L_{1}}) by setting x ≤_{L_{0}+L_{1}} y if and only if x ∈ L_{0} and y ∈ L_{1} or x, y ∈ L_{n} and x ≤_{L_{n}} y for some n < 2. The infinitary generalization of this operation ∑_{n} L_{n} = (⋃_{n} L_{n}, ≤_{∑_{n} L_{n}}) is defined similarly. The linear order L_{0} · L_{1} = (L_{0} × L_{1}, ≤_{L_{0}·L_{1}}) is defined by (x_{0}, x_{1}) ≤_{L_{0}·L_{1}} (y_{0}, y_{1}) iff either x_{1} <_{L_{1}} y_{1} or x_{1} = y_{1} and x_{0} ≤_{L_{0}} y_{0}. RCA_{0} proves that if the L_{n}’s are well-orders then L_{0} + L_{1}, ∑_{n} L_{n} and L_{0} · L_{1} are also well-orders.

In RCA_{0} we can also define the exponentiation L_{0}^{L_{1}} of two linear orders (details are e.g. in [Hir05b]). However RCA_{0} cannot prove that when L_{0} and L_{1} are well-orders L_{0}^{L_{1}} is a well-order. In fact this statement is equivalent to ACA_{0} over RCA_{0} ([Gir87, p. 299], see [Hir94] for a direct proof).

Using ordinal exponentiation we can define Cantor normal forms, and Jeff Hirst ([Hir94, Theorem 5.2]) proved the following:

Theorem 2.3. Over RCA_{0}, the following are equivalent:

(1) ATR_{0};

(2) every well order has a Cantor normal form, i.e. it is equivalent to a finite sum of exponentials with base ω and nonincreasing exponents.

We now turn to partial orders, which are formalized in a way similar to linear orders. We typically write P = (P, ≤_{P}) for a partial order defined on the set P with order relation ≤_{P}. If P_{0} and P_{1} are partial orders with disjoint domains, P_{0} + P_{1} is defined in RCA_{0} as in the case of linear orders. We also define the disjoint union P_{0} ⊕ P_{1} = (P_{0} ∪ P_{1}, ≤_{P_{0}⊕P_{1}}) by setting x ≤_{P_{0}⊕P_{1}} y if and only if x, y ∈ P_{n} and x ≤_{P_{n}} y for some n < 2.

Definition 2.4. Within RCA_{0}, if P = (P, ≤_{P}) is a partial order, a linear extension of P is a linear order L = (P, ≤_{L}) such that x ≤_{P} y implies x ≤_{L} y for every x, y ∈ P. We denote by Lin(P) the class of all linear extensions of P (this is just a convenient shorthand: Lin(P) does not exist in second order arithmetic).

We will often deal with linear extensions of partial orders which are the disjoint sum of two linear orders.

Definition 2.5. For I and J linear orders, we call any element of Lin(I ⊕ J) a shuffle of I and J.

Now we can formally define the notion of wpo in RCA_{0}.

Definition 2.6. Within RCA_{0}, a partial order P = (P, ≤_{P}) is a wpo if for every f : ℕ → P there exists i < j such that f(i) ≤_{P} f(j).

The different characterizations of wpo have been studied from the viewpoint of reverse mathematics in [Mar05, CMS04]: it turns out that not all equivalences are provable in RCA_{0}, but that WKL_{0} augmented with the chain-antichain principle CAC (i.e. the statement that every infinite partial order has either an infinite chain or an infinite antichain) suffices. (Thus all definitions of wpo are equivalent in, say, ACA_{0}). In particular we have the following results ([CMS04, Lemma 3.12, Theorem 3.17, Corollary 3.4]).

Lemma 2.7. RCA_{0} proves that every linear extension of a wpo is a well-order. WKL_{0} proves that if a partial order is such that all its linear extensions are well-orders, then it is a wpo.

Lemma 2.8. RCA_{0} plus CAC (and, a fortiori, ACA_{0}) proves that if P is a wpo then for every f : ℕ → P there exists an infinite A ⊆ ℕ such that for all i, j ∈ A with i < j we have f(i) ≤_{P} f(j).

We need to make the last statement effective, but for our purposes it suffices to be quite coarse in this effectivization (e.g. we do not use the results of [CJS01] or [HS07]).

Lemma 2.9. ACA_{0} proves that there exists a construction which is uniformly recursive in the double jump of the input and that starting from the wpo P and f : ℕ → P outputs an infinite A ⊆ ℕ such that for all i, j ∈ A with i < j we have f(i) ≤_{P} f(j).

Proof. Lemma 2.8 is proved using CAC, which is a consequence of Ramsey theorem for pairs. An inspection of the proof of Ramsey Theorem in ACA_{0} ([Sim09, Lemma III.7.4]) shows that a homogenous set for a coloring of pairs is computable from any branch in an infinite finitely branching tree which is computable in the coloring. Such a branch is computable in the double jump of the tree. □

We need to formalize Theorem 1.2 within RCA_{0}. Let P be a wpo. ¿From [Sim09, Theorem V.6.9] it follows that ATR_{0} proves the existence of a well-order Q such that R ⪯ Q for all R ∈ Lin(P). From this, in Π_{1}^{1}-CA_{0} we can define o(P) = sup(Lin(P)) as an element of Q. In systems below Π_{1}^{1}-CA_{0} (including ATR_{0}) it is not clear that we can define o(P) in this way. Therefore we need to state Theorem 1.2 without mentioning o(P). Since the theorem states that wpo’s have maximal linear extensions, the following is a natural translation.

Definition 2.10. Within RCA_{0} we denote by MLE the following statement: every wpo P has a linear extension Q such that R ⪯ Q for all R ∈ Lin(P).

We refer to such a Q as a maximal linear extension of P.

Following the ideas which led to MLE, we now formalize Theorem 1.4.

Definition 2.11. Within RCA_{0}, if P = (P, ≤_{P}) is a partial order, a chain in P is a linear order C = (C, ≤_{P}) where C ⊆ P. We denote by Ch(P) the class of all chains P (again, this is just a convenient shorthand).

Definition 2.12. Within RCA_{0} we denote by MC the following statement: every wpo P has a chain C such that C′ ⪯ C for all C′ ∈ Ch(P).

We refer to such a C as a maximal chain in P.

3. ATR_{0} proves MLE

Before starting with the proof, let us mention that the proofs of Theorem 1.2 in [dJP77], [Har05], and [KT90], when translated into the language of second order arithmetic, require at least Σ_{1}^{1} induction, which is not available in ATR_{0}. The proof of Theorem 1.2 in [Fra00] uses a partial order of sets, and thus cannot be immediately reproduced in second order arithmetic.

We need some preliminaries, starting with the following important tool in the study of wpo’s. (Our notation for finite sequences follows [Sim09, Definition II.2.6], although we use Greek letters to denote sequences.)

Definition 3.1. In RCA_{0} we define, for a partial order P = (P, ≤_{P}), the tree of bad sequences of P:

Bad(P) = { σ ∈ ℕ^{<ℕ} | (∀i < lh(σ))(σ(i) ∈ P ∧ (∀j < i) σ(j) ≰_{P} σ(i)) }.

Notice that P is a wpo if and only if Bad(P) is well founded (i.e. does not have infinite branches). Thus if P is a wpo we can define by transfinite recursion the rank function on Bad(P) (taking ordinals as values), which we denote by rk_{P}, by setting

rk_{P}(σ) = sup{ rk_{P}(σ^{⌢}⟨x⟩) + 1 | σ^{⌢}⟨x⟩ ∈ Bad(P) },

and define the ordinal rk(P) = rk_{P}(∅) (where ∅ denotes the sequence of length 0), so that rk_{P} : Bad(P) → rk(P) + 1.

Using transfinite recursion we can mimic this definition in ATR_{0} (where ordinals are represented by well-orders), thus obtaining a wellorder rk(P) and a function rk_{P} : Bad(P) → rk(P) + 1.

Definition 3.2. In RCA_{0} we define, for a partial order P = (P, ≤_{P}) and σ ∈ Bad(P), P_{σ} = { p ∈ P | (∀i < lh(σ)) σ(i) ≰_{P} p }. We also write P_{σ} = (P_{σ}, ≤_{P}).

Notice that P_{σ} = { p ∈ P | σ^{⌢}⟨p⟩ ∈ Bad(P) }. Actually, for every sequence τ we have τ ∈ Bad(P_{σ}) if and only if σ^{⌢}τ ∈ Bad(P). ¿From this it follows that rk_{P}(σ) = rk(P_{σ}). Notice also that P = P_{∅}.

Lemma 3.3. ATR_{0} proves that if L is a well-order then L ≡ rk(L).

Proof. By transfinite induction on rk_{L}(σ) for σ ∈ Bad(L) show that L_{σ} ≡ rk_{L}(σ). This formula is Δ_{1}^{1} in ATR_{0} by Corollary 2.2. So we can carry out the induction in ATR_{0}. All cases of the induction are immediate. □

Lemma 3.4. ATR_{0} proves that if P is a wpo and L ∈ Lin(P) then L ⪯ rk(P).

Proof. By Lemma 2.7 L is a well-order. Notice that Bad(L) is a subtree of Bad(P) and obviously rk_{L}(σ) ⪯ rk_{P}(σ) for every σ ∈ Bad(L), so that rk(L) ⪯ rk(P). Therefore, using the previous Lemma, L ⪯ rk(P). □

Notice that the above result implies that if P is a computable wpo then o(P) is a computable ordinal, as it is at most rk(P) and Bad(P) is a computable tree. This formally answers a question of [Sch79], but a real answer and much more information is provided by Montalbán in Theorem 1.7.

Lemma 3.4 suggests our strategy for proving MLE within ATR_{0}: define, for each wpo P, an L ∈ Lin(P) such that rk(P) ⪯ L (so that actually L ≡ rk(P)).

Our last preliminary result (Lemma 3.7 below) shows that ATR_{0} proves a special case of MLE, and indeed computes the maximal order type of a linear extension of the disjoint union of two well-orders. (In Lemma 5.3 we will obtain a much weaker result in ACA_{0}.)

Before stating the Lemma, we need to adapt the definition of natural (also called Hessenberg, or commutative) sum of ordinals to well-orders.

By Theorem 2.3 ATR_{0} proves that every well-order has a Cantor Normal Form: this is what is needed for the definition of natural sum.

Definition 3.5. In ATR_{0}, suppose I ≡ ∑_{i≤m} ω^{K_{i}} and J ≡ ∑_{j≤n} ω^{L_{j}} are well-orders with K_{i+1} ⪯ K_{i} and L_{j+1} ⪯ L_{j} for i < m and j < n. Order the set { K_{i} | i ≤ m } ∪ { L_{j} | j ≤ n } as { M_{k} | k ≤ m + n } so that M_{k+1} ⪯ M_{k} for k < m + n. Then we let I # J be ∑_{k≤m+n} ω^{M_{k}}.

The precise definition of the well-order I # J obviously depends on the well-orders K_{i} and L_{j} used in the Cantor Normal Forms of I and J. It is therefore to be considered as a definition “up to equivalence”. Notice that # is obviously commutative. The following Lemma states another basic property of the natural sum.

Lemma 3.6. ATR_{0} proves that if I and J are well-orders and I ≺ I′ then I # J ≺ I′ # J.

Lemma 3.7. ATR_{0} proves that if I and J are well-orders there exists Q ≡ I #J which is a maximal shuffle of I and J (i.e. Q is a maximal linear extension of I ⊕ J).

Proof. Let P = I ⊕J. It is easy to define Q ∈ Lin(P) with Q ≡ I #J: using the notation of the previous definition, elements of I ∪ J are identified in the obvious way with elements of ∑_{k≤m+n} ω^{M_{k}}.

To prove that Q is a maximal linear extension of P, by Lemma 3.4, it suffices to show that rk(P) ⪯ I # J.

For σ ∈ Bad(P) we let I_{σ} = P_{σ} ∩I and J_{σ} = P_{σ} ∩J and denote by I_{σ} and J_{σ} the corresponding linear orders. We use transfinite induction on rk_{P}(σ) to prove that rk_{P}(σ) ⪯ I_{σ} # J_{σ} for every σ ∈ Bad(P) (this is again a Δ_{1}^{1} transfinite induction in ATR_{0}). Fix σ ∈ Bad(P). For every p ∈ I_{σ} and q ∈ I_{σ^{⌢}⟨p⟩} we have q <_{I} p, and thus I_{σ^{⌢}⟨p⟩} ≺ I_{σ}. In this case we also have J_{σ^{⌢}⟨p⟩} = J_{σ}. When p ∈ J_{σ} the situation is symmetric. Thus, for every p ∈ P_{σ}, either I_{σ^{⌢}⟨p⟩} ≺ I_{σ} and J_{σ^{⌢}⟨p⟩} = J_{σ}, or J_{σ^{⌢}⟨p⟩} ≺ J_{σ} and I_{σ^{⌢}⟨p⟩} = I_{σ}. In both cases, by Lemma 3.6, we have I_{σ^{⌢}⟨p⟩} # J_{σ^{⌢}⟨p⟩} ≺ I_{σ} # J_{σ}, i.e. (I_{σ^{⌢}⟨p⟩} # J_{σ^{⌢}⟨p⟩}) + 1 ⪯ I_{σ} # J_{σ}. Thus, using the induction hypothesis,

rk_{P}(σ) = sup{ rk_{P}(σ^{⌢}⟨p⟩) + 1 | p ∈ P_{σ} }
⪯ sup{ (I_{σ^{⌢}⟨p⟩} # J_{σ^{⌢}⟨p⟩}) + 1 | p ∈ P_{σ} }
⪯ I_{σ} # J_{σ}.

When σ = ∅ we have rk_{P}(∅) ⪯ I # J and thus rk(P) ⪯ I # J. □

We can now prove the main result of this section.

Theorem 3.8. ATR_{0} proves MLE.

Proof. Let P = (P, ≤_{P}) be a wpo. Using arithmetical transfinite recursion on rank we will define, for each σ ∈ Bad(P), a linear order L_{σ}. We will then prove by Δ_{1}^{1} transfinite induction on rank that L_{σ} ∈ Lin(P_{σ}) and rk_{P}(σ) ⪯ L_{σ}. Since P_{∅} = P, we have L_{∅} ∈ Lin(P) and rk(P) ⪯ L_{∅}. By Lemma 3.4, L_{∅} is a maximal linear extension of P and the proof is complete.

To define the L_{σ}’s we need some preliminaries. Let

S = { σ ∈ Bad(P) | rk_{P}(σ) is a successor } and
L = { σ ∈ Bad(P) | rk_{P}(σ) is a limit }.

In ATR_{0} we can define a function p : S → P such that p(σ) ∈ P_{σ} and rk_{P}(σ) = rk_{P}(σ^{⌢}⟨p(σ)⟩) + 1 for every σ ∈ S. We also need, for every σ ∈ L, a sequence ⟨x_{i}⟩ of elements of P_{σ} such that rk_{P}(σ) = sup{ rk_{P}(σ^{⌢}⟨x_{i}⟩) | i ∈ ℕ }. However we want ⟨x_{i}⟩ to enjoy further properties, so we are going to describe its construction in detail.

Fix σ ∈ L and suppose rk_{P}(σ) = λ = ∑_{k≤m} ω^{α_{k}} with α_{k} ≥ α_{k+1} > 0 for every k < m. Let γ = ∑_{k<m} ω^{α_{k}} and look at α_{m}. If α_{m} is a successor β +1 let β_{n} = β for every n. If α_{m} is a limit, we can compute (from the realization of α_{m} as a concrete well-order) a sequence (β_{n}) such that β_{n} < β_{n+1} and α_{m} = sup{ β_{n} | n ∈ ℕ }. In both cases let λ_{n} = γ + ∑_{j<n} ω^{β_{j}}, so that λ = sup{ λ_{n} | n ∈ ℕ }. Notice also that λ = γ + ∑_{i∈ℕ} ω^{β_{n_{i}}} for any infinite increasing sequence (n_{i}). We can define by recursion infinite sequences (x_{i}) and (n_{i}) such that for all i

(1) x_{i} ∈ P_{σ},

(2) n_{i} < n_{i+1},

(3) λ_{n_{i}} ≤ rk_{P}(σ^{⌢}⟨x_{i}⟩) < λ_{n_{i}+1}. Lemma 2.8 implies that we can refine the sequence ⟨x_{i}⟩ so that for all i we also have

(4) x_{i} ≤_{P} x_{i+1}. Notice that in fact x_{i} ≠ x_{i+1} and hence x_{i} <_{P} x_{i+1} and P_{σ^{⌢}⟨x_{i}⟩} ⊊ P_{σ^{⌢}⟨x_{i+1}⟩} hold.

In the preceding paragraph we showed that for every σ ∈ L there exist the well-orders α_{k}’s representing rk_{P}(σ) in Cantor normal form, the sequence (β_{n}) obtained from α_{m} (which we use to define the λ_{n}’s), and sequences (x_{i}) and (n_{i}) satisfying conditions (1)–(4) above. Using Σ_{1}^{1}-AC_{0}, which is provable in ATR_{0}, we can associate to every σ ∈ L objects satisfying these conditions, which will be used in the definition of L_{σ}.

Before going on, we notice some further properties of the x_{i}’s. First, we have γ = λ_{0} ≤ rk_{P}(σ^{⌢}⟨x_{0}⟩).

We claim also that P_{σ} = ⋃_{i∈ℕ} P_{σ^{⌢}⟨x_{i}⟩}. In fact if y ∈ P_{σ} is such that y ∉ P_{σ^{⌢}⟨x_{i}⟩} for all i, we have x_{i} <_{P} y for all i (if y = x_{i} then y ∈ P_{σ^{⌢}⟨x_{i+1}⟩}, as x_{i} <_{P} x_{i+1}). Then σ^{⌢}⟨y, x_{i}⟩ ∈ Bad(P) and rk_{P}(σ^{⌢}⟨y, x_{i}⟩) = rk_{P}(σ^{⌢}⟨x_{i}⟩) for every i (since P_{σ^{⌢}⟨y,x_{i}⟩} = P_{σ^{⌢}⟨x_{i}⟩}). Therefore rk_{P}(σ^{⌢}⟨y⟩) ≥ sup rk_{P}(σ^{⌢}⟨x_{i}⟩) = rk_{P}(σ), which is impossible.

We also let Q_{0} = P_{σ^{⌢}⟨x_{0}⟩} and Q_{i+1} = P_{σ^{⌢}⟨x_{i+1}⟩} \ P_{σ^{⌢}⟨x_{i}⟩}. Notice that P_{σ} = ⋃_{i∈ℕ} Q_{i} follows from P_{σ} = ⋃_{i∈ℕ} P_{σ^{⌢}⟨x_{i}⟩}.

We can now define by transfinite recursion the function σ ↦ L_{σ}. When rk_{P}(σ) = 0 we let L_{σ} be the empty well-order. When σ ∈ S let L_{σ} = L_{σ^{⌢}⟨p(σ)⟩} + {p(σ)}. If σ ∈ L we let

L_{σ} = ∑_{i∈ℕ}(L_{σ^{⌢}⟨x_{i}⟩} ↾ Q_{i}) .

Here, of course, we are using the x_{i}’s (and hence the resulting Q_{i}’s) fixed in correspondence with σ before the recursion started.

Now we prove by Δ_{1}^{1} transfinite induction on rank that L_{σ} ∈ Lin(P_{σ}) and that rk_{P}(σ) ⪯ L_{σ} for all σ ∈ Bad(P).

When rk_{P}(σ) = 0 we have P_{σ} = ∅ and the proof is immediate.

When σ ∈ S let τ = σ^{⌢}⟨p(σ)⟩ and recall that rk_{P}(σ) = rk_{P}(τ) + 1. First notice that P_{σ} = P_{τ} ∪ {p(σ)}. In fact, one inclusion is obvious. For the other, observe that if p′ ∈ P_{σ} \ (P_{τ} ∪ {p(σ)}) then p(σ) <_{P} p′ and τ′ = σ^{⌢}⟨p′, p(σ)⟩ ∈ Bad(P). Moreover P_{τ′} = P_{τ} and rk_{P}(τ′) = rk_{P}(τ), which is impossible because rk_{P}(σ) ≥ rk_{P}(τ′) + 2. By the induction hypothesis L_{τ} ∈ Lin(P_{τ}) and rk_{P}(τ) ⪯ L_{τ}. It is clear that L_{σ} = L_{τ} + {p(σ)} is a linear extension of P_{σ} (if q ∈ P_{τ} then p(σ) ≤_{P} q is impossible) and that rk_{P}(σ) ⪯ L_{σ}.

When σ ∈ L let γ, (β_{n}), (λ_{n}), (x_{i}), (n_{i}), and (Q_{i}) be the objects fixed in correspondence with σ. To simplify the notation we write Q_{i} in place of L_{σ^{⌢}⟨x_{i}⟩} ↾ Q_{i}. Notice that since Q_{0} = L_{σ^{⌢}⟨x_{0}⟩} the induction hypothesis implies γ ⪯ Q_{0}.

We now claim that ω^{β_{n_{i}}} ⪯ Q_{i+1}. If this is not the case then we have Q_{i+1} ≺ ω^{β_{n_{i}}}. Notice that, by Lemma 3.4, L_{σ^{⌢}⟨x_{i+1}⟩} ↾ P_{σ^{⌢}⟨x_{i}⟩} ⪯ rk_{P}(σ^{⌢}⟨x_{i}⟩) ≡ λ_{n_{i}} + α for some α < ω^{β_{n_{i}}}. Since L_{σ^{⌢}⟨x_{i+1}⟩} is a shuffle of L_{σ^{⌢}⟨x_{i+1}⟩} ↾ P_{σ^{⌢}⟨x_{i}⟩} and Q_{i+1}, by Lemma 3.7 we would have

L_{σ^{⌢}⟨x_{i+1}⟩} ⪯ (L_{σ^{⌢}⟨x_{i+1}⟩} ↾ P_{σ^{⌢}⟨x_{i}⟩}) # Q_{i+1}
≡ (λ_{n_{i}} + α) # Q_{i+1}
≺ λ_{n_{i}} + ω^{β_{n_{i}}} ≡ λ_{n_{i}+1} ≤ λ_{n_{i+1}}.

On the other hand the induction hypothesis implies that λ_{n_{i+1}} ≤ rk_{P}(σ^{⌢}⟨x_{i+1}⟩) ⪯ L_{σ^{⌢}⟨x_{i+1}⟩}. The contradiction establishes the claim.

Then

λ = γ + ∑_{i∈ℕ}ω^{β_{n_{i}}} ⪯ L_{σ}.

To check that L_{σ} ∈ Lin(P_{σ}) recall that P_{σ} = ⋃_{i∈ℕ} Q_{i} and notice that when x ∈ Q_{i} and y ∈ Q_{j+1} with i ≤ j we have x_{i} ≰_{P} x and x_{i} ≤_{P} x_{j} ≤_{P} y, which imply y ≰_{P} x. □

We can also prove MLE in ATR_{0} using ideas from Montalbán’s proof of the first part of Theorem 1.7. Many modifications are needed, since Montalbán did assume Theorem 1.2. This alternative proof is more complex than the one above, and we have not included it in this paper.

If instead one begins the proof of Theorem 3.8 with the tree of bad sequences with each node labeled with the Cantor normal forms of its rank (in a unified recursive notation system), then the only noneffective step in the transfinite recursion needed for the construction is the extraction of the subsequence to satisfy condition (4) from the sequence satisfying (1)–(3). This step can easily be done computably in the double jump of this labeled tree by Lemma 2.9. Thus relative to the double jump of the labeled tree of bad sequences, the entire construction can be seen as an effective transfinite recursion. This procedure thus provides a uniform construction of a maximal linear extension computable in the double jump of the assignments of ranks and the corresponding Cantor normal forms to the nodes of the tree. So one can compute the level of the hyperarithmetic hierarchy at which one has a uniformly recursive construction of a maximal linear extension. This contrasts with Montalbán’s result in 1.7 that while there is always a recursive maximal linear extension, it cannot be computed uniformly even hyperarithmetically.

After we had essentially the proof presented above of MLE in ATR_{0} (in its effective form), Harvey Friedman (in response to a lecture given by the second author on some of the material in this paper) informed us that he had a proof of this result using the tree of bad sequences in some handwritten notes that also contained many calculations of the ranks of such trees for many specific partial orders. He dates these notes probably to 1984. We have not seen his proof and do not know if it is the same or different from the one we presented here.

4. MLE implies ACA_{0}

The first part of Theorem 1.7 suggests that to exploit the strength of MLE within RCA_{0} we need to use partial orders which RCA_{0} cannot recognize as not being wpo’s. Such a partial order will be defined using the linear order supplied by Lemma 4.2. Before stating it, we recall the following definitions from [HS07].

Definition 4.1. Within RCA_{0} we say that a linear order L = (L, ≤_{L}) has order type ω if L is infinite and each element of L has finitely many ≤_{L}-predecessors.

L has has order type ω + ω^{∗} if each element of L has either finitely many ≤_{L}-predecessors or finitely many ≤_{L}-successors, and there are infinitely many elements of both types.

The existence of a linear order satisfying the first two conditions of the following lemma is folklore.

Lemma 4.2. RCA_{0} proves that there exists a (computable) linear order L = (L, ≤_{L}) such that

(a) L has order type ω + ω^{∗};

(b) if there exists a descending sequence in L then ∅′ exists;

(c) the formula “x has finitely many ≤_{L}-predecessors” is Σ_{1}^{0} (and thus “x has finitely many ≤_{L}-successors” is Π_{1}^{0});

(d) for all x with finitely many ≤_{L}-successors and for all k ∈ ℕ there exists y with finitely many ≤_{L}-successors such that |[y, x]_{L}| > k (this means that there exist a one-to-one sequence σ of length k such that y ≤_{L} σ(i) ≤_{L} x for every i < k).

Proof. Fix a computable total one-to-one function f with range ∅′. We first define L satisfying (a), (b) and (c). Then we modify it to satisfy (d) as well.

We let L = ℕ and define ≤_{L} by stages: at stage s we have defined ≤_{L} on {0, …, s}. At stage s = 0 there are no decisions to make. At stage s + 1 we add s + 1 to the order as follows:

• if f(s + 1) > f(s) then s + 1 occurs immediately before s;

• if f(s + 1) < f(s) then let t ≤ s be the ≤_{L}-largest element such that f(s + 1) < f(t), and put s + 1 immediately after t.

This completes the definition of ≤_{L}, which is clearly computable. ¿From the construction it is immediate that

(1) if s < t is such that s <_{L} t then s <_{L} r for every r > t;

(2) if r < s is such that f(s) < f(r) then r <_{L} s.

To check that (a) holds we need to show that each element of L has either finitely many ≤_{L}-predecessors or finitely many ≤_{L}-successors, and there are infinitely many elements of each type.

If s is a true stage for f, i.e. (∀t > s) f(t) > f(s), we have (∀t > s) t <_{L} s. In fact, if t > s were least such that t >_{L} s there would exist r < s with s <_{L} r <_{L} t such that f(t) < f(r). Since s <_{L} r and r < s, by (2), we have f(s) > f(r), which implies f(s) > f(t). Thus if s is a true stage for f, L_{(≥_{L}s)} ⊆ {0, …, s} is finite.

If s is not a true stage for f, i.e. (∃t > s) f(t) < f(s), let t_{0} + 1 be the least such t. Then f(t_{0} + 1) < f(s) ≤ f(t_{0}) and s <_{L} t_{0} + 1. By (1), L_{(≤_{L}s)} ⊆ {0, …, t_{0}} is finite.

There exist infinitely many true stages for f, otherwise we could easily define a descending sequence in ℕ. There also exist infinitely many nontrue stages for f: otherwise if n_{0} is such that all n ≥ n_{0} are true stages, we have (∃n) f(n) = m if and only if (∃n ≤ n_{0} +m) f(n) = m for every m, which contradicts the incomputability of ∅′.

We now show that every descending sequence in L computes ∅′, establishing (b). If (s_{m}) is a <_{L}-descending sequence, by the observations above we have that each s_{m} is a true stage for f and that s_{m} < s_{m+1}, so that f(s_{m}) < f(s_{m+1}). Hence f(s_{m}) ≥ m. Therefore

(∀m)((∃n) f(n) = m ⟺ (∃n ≤ s_{m}) f(n) = m).

Thus ∅′ can be computed from (s_{m}).

Since “s is a true stage for f” is a Π_{1}^{0} statement, (c) holds.

Thus L satisfies (a), (b) and (c). Notice that proving (d) for L appears to require Σ_{2}^{0} induction, which is not available in RCA_{0}. We define a linear order L′ = (L′, ≤_{L′}) satisfying (d) by replacing each n ∈ L by n + 1 distinct elements and otherwise respecting the order of L. To be precise, we set

L′ = { (n, i) | n ∈ L ∧ i ≤ n } and
(n, i) ≤_{L′} (m, j) ⟺ n <_{L} m ∨ (n = m ∧ i ≤ j).

It is easy to check that L′ satisfies (a), (b) and (c).

To prove (d) consider x = (n, i) with finitely many ≤_{L}-successors and a given k. Let m ∈ L be such that m <_{L} n, L_{(≥_{L}m)} is finite, and m ≥ k. Such an m exists because there exist infinitely many m ∈ L such that L_{(≥_{L}m)} is finite. Let y = (m, 0) ∈ L′: since [y, x]_{L′} ⊇ { (m, j) | j ≤ m }, we have |[y, x]_{L′}| > m ≥ k, as required. □

Theorem 4.3. RCA_{0} proves that MLE implies ACA_{0}.

Proof. To prove ACA_{0} it suffices to show that for every X the jump of X, X′, exists. We will do so for X = ∅, as the obvious relativization extends the proof to every X.

In RCA_{0} let L = (L, ≤_{L}) be the linear order of Lemma 4.2. We will use the following notation:

D = { x ∈ L | L_{(≤_{L}x)} is finite }, U = { x ∈ L | L_{(≥_{L}x)} is finite }.

Notice that the existence of D and U as sets is not provable in RCA_{0}, and expressions such as x ∈ D should be viewed only as shorthand for more complex formulas. It is immediate that D is downward closed and U is upward closed in L. By (a) U and D are nonempty and form a partition of L. Moreover by (c) the formulas x ∈ U and x ∈ D are respectively Π_{1}^{0} and Σ_{1}^{0}.

We will apply MLE to the partial order P = L ⊕ L. To be precise, P = (P, ≤_{P}) where P = L × 2 and

(x, i) ≤_{P} (y, j) ⟺ i = j ∧ x ≤_{L} y.

For i < 2 we write L_{i}, D_{i} and U_{i} for L × {i}, D × {i}, and U × {i} respectively. L_{i} = (L_{i}, ≤_{P}) is obviously isomorphic to L.

If P is not a wpo then, using the pigeonhole principle for two colors in RCA_{0}, there is a descending sequence in either L_{0} or L_{1}. Hence there exists a descending sequence in L and, by (b), ∅′ exists.

We thus assume that P is a wpo, so that MLE applies and there exists a maximal linear extension Q = (P, ≤_{Q}) of P. The proof of the existence of ∅′ now splits in two cases, depending on the properties of Q.

Case I. For all i < 2, x ∈ D_{i} and y ∈ U_{1−i} we have x <_{Q} y.

If for some i < 2 there exists x ∈ D_{i} such that y <_{Q} x for all y ∈ D_{1−i} then notice that U_{1−i} = { y ∈ L_{1−i} | x <_{Q} y } exists as a set and therefore U exists a set. Then we can define a function which maps each x ∈ U to some y ∈ U with y <_{L} x. We can use this function to define a descending sequence in L and apply (b). Hence ∅′ exists, so that the proof is complete. The same argument applies if for some i < 2 there exists x ∈ U_{i} such that x <_{Q} y for all y ∈ U_{1−i}.

We thus assume that (∀i < 2) (∀x ∈ D_{i}) (∃y ∈ D_{1−i}) x <_{Q} y and (∀i < 2) (∀x ∈ U_{i}) (∃y ∈ U_{1−i}) y <_{Q} x. This implies that for every x ∈ P either P_{(≤_{Q}x)} or P_{(≥_{Q}x)} is finite. (Thus Q has order type ω +ω^{∗}.) Now consider the linear extension K = (P, ≤_{K}) of P defined by

(x, i) ≤_{K} (y, j) ⟺ i < j ∨ (i = j ∧ x ≤_{L} y).

In other words, K = L_{0} + L_{1}. Every x ∈ U_{0} ∪ D_{1} is such that both P_{(≤_{K}x)} ⊇ D_{0} and P_{(≥_{K}x)} ⊇ U_{1} are infinite. This implies K ⪯̸ Q, contradicting the maximality of Q.

Case II. There exist i < 2, x ∈ D_{i} and y ∈ U_{1−i} such that y <_{Q} x. To simplify the notation, we assume i = 0.

Now consider the linear extension J = (P, ≤_{J}) of P defined by

(x, i) ≤_{J} (y, j) ⟺ x <_{L} y ∨ (x = y ∧ i ≤ j).

In other words, J = 2 · L. Notice that it is easily provable in RCA_{0} that for all z, w ∈ U_{i} with z ≤_{L_{i}} w, we have |[z, w]_{J} | = 2 · |[z, w]_{L_{i}}| − 1.

Since Q is maximal there exists g : P → P which witnesses J ⪯ Q. The proof splits in two subcases.

Subcase IIa. There exists w_{0} ∈ U_{1} such that g(w_{0}) ≤_{Q} x.

We claim that there exists w ∈ U_{1} with w ≤_{L_{1}} w_{0} satisfying g(z) ∈ L_{1} for all z ∈ U_{1} such that z ≤_{L_{1}} w. To see this let

A = { x′ ∈ L_{0}_{(≤_{L_{0}}x)} | (∃w ∈ L_{1}) g(w) = x′ }, and
B = { x′ ∈ L_{0}_{(≤_{L_{0}}x)} | (∃w ∈ D_{1}) g(w) = x′ }.

Since x ∈ D_{0}, RCA_{0} proves the existence of A and B by bounded Σ_{1}^{0}- comprehension (recall that D_{1} is Σ_{1}^{0}). Let C = A \ B. Then RCA_{0} proves that C exists and is finite. The subcase hypothesis implies that C ≠ ∅, as g(w_{0}) ∈ C. Let x′_{0} be the minimum of C with respect to ≤_{L_{0}} and let (since x′_{0} ∈ A) w′ ∈ L_{1} be such that g(w′) = x′_{0}. Since x′_{0} ∉ B and g is one-to-one we have w′ ∈ U_{1}. Any w ∈ U_{1} such that w <_{L_{1}} w′ has the required property.

Fix w as above, and notice that g(z) ∈ U_{1} for any z ∈ U_{1} with z ≤_{L_{1}} w. In fact, P_{(<_{J} z)} ⊇ L_{1}_{(<_{L_{1}}z)} is infinite while P_{<_{Q}x′} ⊆ L_{0}_{(<_{L_{0}}x)} ∪ L_{1}_{(<_{L_{1}}x′)} is finite when x′ ∈ D_{1} (recall that in this case x′ ≤_{Q} y ≤_{Q} x).

We now wish to find z_{0} ≤_{L_{1}} w such that g(z_{0}) <_{Q} z_{0} (and hence g(z_{0}) <_{L_{1}} z_{0}, because g(z_{0}) ∈ L_{1} by our choice of w). If g(w) <_{L_{1}} w it suffices to let z_{0} = w. If w ≤_{L_{1}} g(w) let, by (d), z_{0} ∈ U_{1} be such that z_{0} ≤_{L_{1}} w and

|[z_{0}, w]_{L_{1}}| > |[w, g(w)]_{L_{1}}| + |L_{0}_{(<_{L_{0}}x)}|.

Then, using g(w) ≤_{Q} x, we have

|[z_{0}, w]_{J} | = 2 · |[z_{0}, w]_{L_{1}}| − 1
> |[z_{0}, w]_{L_{1}}| + |[w, g(w)]_{L_{1}}| + |L_{0}_{(<_{L_{0}}x)}| − 1
= |[z_{0}, g(w)]_{L_{1}}| + |L_{0}_{(<_{L_{0}}x)}|
≥ |[z_{0}, g(w)]_{Q}|.

Since g maps the interval [z_{0}, w]_{J} injectively into the interval [g(z_{0}), g(w)]_{Q}, this implies that g(z_{0}) <_{Q} z_{0}, as we wanted.

Now recursively define z_{n+1} = g(z_{n}). By Π_{1}^{0} induction on n it is straightforward to show that z_{n} ∈ U_{1} and z_{n+1} <_{L_{1}} z_{n} ≤_{L_{1}} w. We have thus defined a descending sequence in L_{1} and hence in L. By (b), ∅′ exists.

Subcase IIb. For every w ∈ U_{1} we have x <_{Q} g(w).

Since for all w ∈ U_{0} there exists w′ ∈ U_{1} such that w′ <_{J} w we also have x <_{Q} g(w) for every w ∈ U_{0}.

We claim that w ∈ U_{0} and g(w) ∈ L_{0} imply g(w) ∈ U_{0}. To see this, we argue by contradiction and assume that there exists w ∈ U_{0} with g(w) ∈ D_{0}. Then [x, g(w)]_{Q} ⊆ L_{0}_{(≤_{L_{0}}g(w))} ∪L_{1}_{(>_{L_{1}}y)} is finite. If, by (d), w′ ∈ U_{0} is such that |[w′, w]_{L_{0}}| ≥ |[x, g(w)]_{Q}| then g(w′) ≤_{Q} x, which contradicts what we noticed above.

Notice also that w ∈ L_{0}_{(≥_{L_{0}}x)} and g(w) ∈ L_{1} imply y <_{L_{1}} g(w). Since L_{1}_{(>_{L_{1}}y)} is finite, this can happen only finitely many times. Thus, arguing as in the previous subcase, we can find w ∈ U_{0} such that g(z) ∈ U_{0} for all z ∈ U_{0} such that z ≤_{L_{0}} w.

We mimic the argument used in the previous subcase, finding z_{0} ∈ U_{0} with z_{0} ≤_{L_{0}} w such that g(z_{0}) <_{Q} z_{0}. When g(w) <_{L_{0}} w we set z_{0} = w. If w ≤_{L_{0}} g(w), we pick, by (d), z_{0} ∈ U_{0} with z_{0} ≤_{L_{0}} w such that

|[z_{0}, w]_{L_{0}}| > |[w, g(w)]_{L_{0}}| + |L_{1}_{(>_{L_{1}}y)}|.

Then, using y <_{Q} x <_{Q} z_{0}, we have

|[z_{0}, w]_{J} | = 2 · |[z_{0}, w]_{L_{0}}| − 1
> |[z_{0}, w]_{L_{0}}| + |[w, g(w)]_{L_{0}}| + |L_{1}_{(>_{L_{1}}y)}| − 1
= |[z_{0}, g(w)]_{L_{0}}| + |L_{1}_{(>_{L_{1}}y)}|
≥ |[z_{0}, g(w)]_{Q}|.

Since g maps the interval [z_{0}, w]_{J} injectively into the interval [g(z_{0}), g(w)]_{Q}, this implies g(z_{0}) <_{Q} z_{0}, as we wanted.

We now define z_{n+1} = g(z_{n}) for all n. Using again Π_{1}^{0} induction, we can show that this is a descending sequence in L_{0}. By (b), ∅′ exists. □

5. MLE implies ATR_{0}

Although most properties of well-orders require ATR_{0}, some of them (such as the fact that well-orders are closed under exponentiation) can be proved in ACA_{0}. In this section we will use two of these facts, both due to Jeff Hirst ([Hir94, Theorem 3.5 and Lemma 4.3]).

Theorem 5.1. ACA_{0} proves that if L is a well order, then ω^{L} is indecomposable, i.e. if ω^{L} ⪯ I + J then either ω^{L} ⪯ I or ω^{L} ⪯ J.

Theorem 5.2. ACA_{0} proves that if L_{0} and L_{1} are well-orders then L_{0} ⪯ L_{1} if and only if ω^{L_{0}} ⪯ ω^{L_{1}}.

We will also need the following Lemma, which is a much weaker version of Lemma 3.7.

Lemma 5.3. ACA_{0} proves that if I and J are well-orders without a maximum element and L is a shuffle of I and J, then L ⪯ I · J or L ⪯ J · I.

Proof. Let I = (I, ≤_{I}), J = (J, ≤_{J}) and (assuming I and J are disjoint) L = (I ∪ J, ≤_{L}). At least one of I and J is cofinal in L. We assume that I is cofinal in L and we define an embedding f of L into J ·I (if J is cofinal we obtain L ⪯ I·J). Let m be the ≤_{J}-least element of J. Using ACA_{0} we can define the operations s_{I} and s_{J} mapping each element of I and J to its successor according to I and J. Similarly, again using ACA_{0}, we can define the function t which maps x ∈ J to the ≤_{I}-least y ∈ I such that x <_{L} y. Define f : I ∪ J → J × I as follows:

f(x) = \begin{cases}(m, s_{I}(x)) & if x ∈ I; \\ (s_{J}(x), t(x)) & if x ∈ J. \end{cases}

To see that f preserves order, consider the four possible cases. If x <_{I} y then s_{I}(x) <_{I} s_{I}(y) and so (m, s_{I}(x)) <_{J×I} (m, s_{I}(y)). If x <_{J} y, then t(x) ≤_{J} t(y) and s_{J}(x) <_{J} s_{J}(y) and so (s_{J}(x), t(x)) <_{J×I} (s_{J}(y), t(y)). If x ∈ I, y ∈ J and x <_{L} y, then s_{I}(x) ≤_{I} t(y) and, of course, m <_{J} s_{J}(y) and so (m, s_{I}(x)) <_{J×I} (s_{J}(y), t(y)). Finally, if x ∈ J, y ∈ I and x <_{L} y, then t(x) ≤_{I} y <_{I} s_{I}(y) and so (s_{J}(x), t(x)) <_{J×I} (m, s_{I}(y)) as required. □

Theorem 5.4. ACA_{0} proves that MLE implies ATR_{0}.

Proof. We work in ACA_{0}, assume that ATR_{0} fails and work toward a contradiction. By Theorem 2.1, the failure of ATR_{0} implies the existence of a sequence ⟨I_{n}⟩ of well-orders that are pairwise mutually nonembeddable. For every n let J_{n} = ω^{ω^{In}}. Using Theorem 5.2 twice we have that the J_{n}’s are also pairwise mutually nonembeddable. Let J_{n} = (J_{n}, ≤_{J_{n}}): without loss of generality, we may assume that the J_{n}’s are pairwise disjoint.

We claim that if k, m and n are distinct then J_{n} is not embeddable in any shuffle of J_{k} and J_{m}. To see this notice that by Lemma 5.3 it suffices to prove that J_{n} ⪯̸ J_{m} · J_{k}. Suppose the contrary, i.e. that ω^{ω^{In}} ⪯ ω^{ω^{Im}} · ω^{ω^{I_{k}}} = ω^{ω^{Im}+ω^{I_{k}}} (where the equality, which is really an isomorphism, is provable in RCA_{0}). Theorem 5.2 implies ω^{I_{n}} ⪯ ω^{I_{m}} + ω^{I_{k}}. As ω^{I_{n}} is indecomposable (Theorem 5.1) we would then have either ω^{I_{n}} ⪯ ω^{I_{m}} or ω^{I_{n}} ⪯ ω^{I_{k}}, and so, by Theorem 5.2 again, I_{n} ⪯ I_{m} or I_{n} ⪯ I_{k}, contrary to our choice of the I_{i}.

Let L_{0} = ∑_{n} J_{2n} and L_{1} = ∑_{n} J_{2n+1}: these are well-orders by

[Hir05b, Theorem 12], and we can define the wpo P = (P, ≤_{P}) as L_{0} ⊕ L_{1}. By MLE let Q = (P, ≤_{Q}) be a maximal linear extension of P.

For every n let x_{n} be the least element of J_{n} with respect to ≤_{J_{n}} (and hence also to ≤_{Q}). Notice that, for example, x_{2n} <_{P} x_{2n+2} and x_{2n+1} <_{P} x_{2n+3} (and hence also x_{2n} <_{Q} x_{2n+2} and x_{2n+1} <_{Q} x_{2n+3}) for every n.

We claim that

(*)  if F ⊆ ℕ is finite and m ∉ F, then J_{m} ⪯̸ Q ↾ (⋃_{i∈F} J_{i})

To prove (*) suppose f witnesses J_{m} ⪯ Q ↾ (⋃_{i∈F} J_{i}). Let i and k be such that x_{2i} and x_{2k+1} are the largest of the x_{l} for l ∈ F, l even and odd respectively, such that f(x), f(x̂) ∈ J_{l}, respectively, for some x, x̂ ∈ J_{m} (if the range of f intersects only J_{l} with l even, or only J_{l} with l odd, the argument is even simpler). For any y >_{m} x, x̂, we must have f(y) ∈ J_{2i} or f(y) ∈ J_{2k+1} as i and k are the largest of their type and f(y) >_{Q} f(x), f(x̂). Now f provides an embedding of a final segment of J_{m} (and so, by indecomposability, of J_{m} itself) into a shuffle of J_{2i} and J_{2k+1}, contradicting what we proved earlier and establishing (*).

Now consider the order of the x_{n} in Q. This is a linear extension of ω ⊕ ω (and so classically of order type ω + ω or ω corresponding to Cases I and II below).

Case I. There exists k such that x_{2n} <_{Q} x_{2k+1} for all n (the reverse situation, where some x_{2k} is above all the x_{2n+1}, is similar). Notice that for every n and x ∈ J_{2n} we have x <_{Q} x_{2n+2} <_{Q} x_{2k+1}. Now consider the linear extension L = ∑ J_{n} of P and suppose f witnesses L ⪯ Q.

Subcase Ia. There exists x ∈ P such that x_{2k+1} ≤_{Q} f(x). By the definition of L we have that for some n we have x_{2k+1} <_{Q} f(x_{2n}). Fix x ∈ J_{2n}: since f(x) ≥_{Q} f(x_{2n}), the case hypothesis implies the existence of l ≥ k such that f(x) ∈ J_{2l+1}. Analogously, f(x_{2n+1}) ∈ J_{2m+1} for some m ≥ k. Therefore f ↾ J_{2n} witnesses J_{2n} ⪯ Q ↾ (⋃_{l=k}^{m} J_{2l+1}), contradicting (*).

Subcase Ib. f(x) <_{Q} x_{2k+1} for all x ∈ P. If f(x_{2k+2}) >_{Q} x_{2n} for all n then for every y ≥_{L} x_{2k+2} we have f(y) ∈ J_{2n+1} for some n < k, so that f ↾ J_{2k+2} witnesses J_{2k+2} ⪯ Q ↾ (⋃_{n<k} J_{2n+1}), against (*). Otherwise f(x_{2k+2}) ≤_{Q} x_{2m} for some m, and f ↾ J_{2k+1} witnesses J_{2k+1} ⪯ Q ↾ (⋃_{n<m} J_{2n} ∪ ⋃_{n<k} J_{2n+1}), again violating (*).

Case II. Neither version of Case I holds and so the x_{2n} and x_{2n+1} are cofinal in each other in Q and each has only finitely many of them preceding it in Q. Consider now the linear extension K = L_{0} + L_{1} of P and an embedding g witnessing K ⪯ Q. By the cofinality assumption there is a k such that g(x_{1}) <_{Q} x_{2k}, x_{2k+1}. Thus P_{(≤_{Q}g(x_{1}))} ⊆ ⋃_{i<2k} J_{i}. Notice that g maps every J_{2n} to P_{(≤_{Q}g(x_{1}))}. In particular g ↾ J_{2k} witnesses J_{2k} ⪯ Q ↾ (⋃_{i<2k} J_{i}), for one more contradiction to (*). □

6. ATR_{0} and MC are equivalent

We prove MC in ATR_{0} in a fashion similar to the way we proved MLE. For this purpose, we adapt the proof in [Sch81], which translated literally into the language of second order arithmetic requires the use of Σ_{1}^{1} induction. We will avoid the use of Σ_{1}^{1} induction by using the same approach we took in Section 3. The proof of MC in [Wol67, KT90, Har05] is based on Radó Selection Lemma (a weak form of the Axiom of Choice) and can also be formalized in ATR_{0}.

Definition 6.1. In RCA_{0} we define, for a partial order P = (P, ≤_{P}), the tree of descending sequences of P:

Desc(P) = { σ ∈ ℕ^{<ℕ} | (∀i < lh(σ))(σ(i) ∈ P ∧ (∀j < i) σ(i) <_{P} σ(j)) }.

Notice that P is well founded (as a partial order) if and only if Desc(P) is well founded as a tree. Thus if P is well founded we can define by transfinite recursion the rank function on Desc(P) (taking ordinals as values), which we denote by ht_{P}, and define the ordinal ht(P) = ht_{P}(∅). As in Section 3, using transfinite recursion we mimic this definition in ATR_{0}.

We let, for σ ∈ Desc(P), P_{σ}^{c} = { p ∈ P | (∀i < lh(σ)) p <_{P} σ(i) } = { p ∈ P | σ^{⌢}⟨p⟩ ∈ Desc(P) }, and we write P_{σ}^{c} = (P_{σ}^{c}, ≤_{P}).

When L is a well-order we have Desc(L) = Bad(L). Hence from Lemma 3.3 it follows immediately that ATR_{0} proves that if L is a wellorder then L ≡ ht(L). We can now prove the next Lemma exactly as we proved Lemma 3.4.

Lemma 6.2. ATR_{0} proves that if P is a well founded partial order and C ∈ Ch(P) then C ⪯ ht(P).

We need the following version of Lemma 2 in [Sch81].

Lemma 6.3. ATR_{0} proves that for each wpo P = (P, ≤_{P}) and each { y_{i}^{j} | j ≤ i } ⊆ P there exists a strictly increasing g : ℕ → ℕ satisfying y_{g(j)}^{j} ≤_{P} y_{g(j+1)}^{j} for every j. Moreover we can require g to be uniformly recursive in the ω-jump of P ⊕ { y_{i}^{j} | j < i }.

Proof. We follow Schmidt’s proof. Fix the wpo P and { y_{i}^{j} | j ≤ i }. Let Z = P ⊕ { y_{i}^{j} | j < i }. We define recursively a sequence of infinite sets (A_{j}) so that A_{j} is computable in Z^{(2j+2)} (the (2j + 2)th jump of Z) as follows.

By applying Lemma 2.9 to the function i ↦ y_{i}^{0} we can find A_{0} infinite, computable in Z′′, and such that y_{i}^{0} ≤_{P} y_{i′}^{0} for all i, i′ ∈ A_{0} with i < i′. If we have defined A_{j} infinite and computable in Z^{(2j+2)} we choose A_{j+1} ⊆ A_{j} infinite and computable in (Z ⊕ A_{j})′′ (and hence in Z^{(2j+4)}) such that y_{i}^{j+1} ≤_{P} y_{i′}^{j+1} for all i, i′ ∈ A_{j+1} with i < i′. Again, the existence of A_{j+1} follows from Lemma 2.9.

Let now for all j, h_{j} be the function enumerating in increasing order A_{j}. Set g(j) = h_{j}(j). To prove that g has the desired property notice that, since A_{j+1} ⊆ A_{j}, there exists i ≥ j + 1 such that g(j + 1) = h_{j+1}(j + 1) = h_{j}(i). This implies g(j + 1) > g(j) and y_{g(j)}^{j} = y_{h_{j}(j)}^{j} ≤_{P} y_{h_{j}(i)}^{j} = y_{g(j+1)}^{j} for every j. Moreover g is computable in ⨁_{j} A_{j} and, by the uniformity of our construction, ⨁_{j} A_{j} is computable in the ω-jump of Z. □

We can now prove the main theorem.

Theorem 6.4. ATR_{0} proves MC.

Proof. By Lemma 6.2 to prove MC within ATR_{0} it suffices to define, for each wpo P, C ∈ Ch(P) such that ht(P) ⪯ C. We adapt the strategy of the proof of Theorem 3.8. In fact, we define, for each σ ∈ Desc(P), a set C_{σ} and a function f_{σ}. We then prove by Δ_{1}^{1} transfinite induction on rank that C_{σ} ⊆ P_{σ}^{c}, that C_{σ} is totally ordered by ≤_{P} (so that C_{σ} = (C_{σ}, ≤_{P}) ∈ Ch(P_{σ}^{c})), and that f_{σ} is an isomorphism between C_{σ} and ht_{P}(σ). Since P_{∅}^{c} = P, we have C_{∅} ∈ Ch(P) and ht(P) ≡ C_{∅}.

As in the proof of Theorem 3.8, but using Desc(P), ht_{P}, and P_{σ}^{c} in place of Bad(P), rk_{P}, and P_{σ}, respectively, we define S, L, p : S → P and for every σ ∈ L the sequences (λ_{n}), (x_{i}) and (n_{i}). Notice that here we use that P is a wpo (and not only a well founded order) when we require x_{i} <_{P} x_{i+1} for every i.

We now define by arithmetical transfinite recursion on rank C_{σ} and f_{σ}. When ht_{P}(σ) = 0 we let C_{σ} = ∅ and f_{σ} be the empty function. When σ ∈ S let C_{σ} = C_{σ^{⌢}⟨p(σ)⟩} ∪ {p(σ)} and, recalling that ht_{P}(σ) = ht_{P}(σ^{⌢}⟨p(σ)⟩) + 1, let f_{σ} extend f_{σ^{⌢}⟨p(σ)⟩} by mapping p(σ) to ht_{P}(σ^{⌢}⟨p(σ)⟩).

When σ ∈ L let us write λ_{n_{−1}} for the least element of ht_{P}(σ) and for j ≤ i let y_{i}^{j} be the element such that f_{σ^{⌢}⟨x_{i}⟩}(y_{i}^{j}) = λ_{n_{j−1}}. (To be scrupulous, at this stage we are not sure that such a y_{i}^{j} exists and is unique, and we should let y_{i}^{j} to be some fixed member of P if this is not the case, an event we will later show never occurs.) By Lemma 6.3 we can find a strictly increasing g : ℕ → ℕ which is uniformly recursive in the ω-jump of P ⊕ { y_{i}^{j} | j < i } satisfying y_{g(j)}^{j} ≤_{P} y_{g(j+1)}^{j} for every j. (To be precise, this definition of a set computable in the ω-jump can be replaced by ω + 1 arithmetic steps.) For j > 0 let

D_{j} = { p ∈ C_{σ^{⌢}⟨x_{g(j)}⟩} | y_{g(j)}^{j−1} ≤_{P} p <_{P} y_{g(j)}^{j} } and set C_{σ} = ⋃_{j>0} D_{j}.

To define f_{σ}, for every p ∈ C_{σ} find the least j such that p ∈ D_{j} (it will follow that there exists only one such j) and set f_{σ}(p) = f_{σ^{⌢}⟨x_{g(j)}⟩}(p).

Now we prove by Δ_{1}^{1} transfinite induction on rank that C_{σ} ⊆ P_{σ}^{c}, that C_{σ} = (C_{σ}, ≤_{P}) ∈ Ch(P_{σ}^{c}) and that f_{σ} is an isomorphism between C_{σ} and ht_{P}(σ). When ht_{P}(σ) = 0 there is nothing to prove. When σ ∈ S it suffices to notice that p <_{P} p(σ) for every p ∈ C_{σ^{⌢}⟨p(σ)⟩} and apply the induction hypothesis.

Fix now σ ∈ L. First, the induction hypothesis implies that y_{i}^{j} ∈ C_{σ^{⌢}⟨x_{i}⟩} and f_{σ^{⌢}⟨x_{i}⟩}(y_{i}^{j}) = λ_{n_{j−1}} for every j ≤ i. Moreover we have D_{j} ⊆ C_{σ^{⌢}⟨x_{g(j)}⟩} ⊆ P_{σ^{⌢}⟨x_{g(j)}⟩}^{c} ⊂ P_{σ}^{c}, and hence C_{σ} ⊆ P_{σ}^{c}. To check that C_{σ} is a chain fix p, p′ ∈ C_{σ}. If p, p′ ∈ D_{j} ⊆ C_{σ^{⌢}⟨x_{g(j)}⟩} for some j, comparability of p and p′ follows from the induction hypothesis. If p ∈ D_{j} and p′ ∈ D_{j′} for j < j′ then p <_{P} y_{g(j)}^{j} ≤_{P} y_{g(j+1)}^{j} ≤_{P} ⋯ ≤_{P} y_{g(j′)}^{j′−1} ≤_{P} p′ (where the first ≤_{P} follows from the property of g) and we have p <_{P} p′. This shows also that C_{σ} = ∑_{j>0} D_{j}, where D_{j} is of course (D_{j}, ≤_{P}). Notice also that by the induction hypothesis and the definition of y_{i}^{j}, f_{σ} restricted to D_{j} is an isomorphism between D_{j} and the interval [λ_{n_{j−2}}, λ_{n_{j−1}}) of ht_{P}(σ). This means that f_{σ} is an isomorphism between C_{σ} and ∑_{j>0}[λ_{n_{j−2}}, λ_{n_{j−1}}) = ht_{P}(σ). □

Our proof of MC in ATR_{0} actually shows the following stronger result.

Theorem 6.5. ATR_{0} proves that any wpo P contains a chain C such that

(∀α < ht(P)) (∃p ∈ C) ht_{P}(p) = α,

where ht_{P}(p) = ht_{P}(⟨p⟩) = ht(P_{(<_{P} p)}).

Proof. In the preceding proof it can be shown inductively that f_{σ}(p) = ht_{P}(p) for every σ ∈ Desc(P) and p ∈ C_{σ}. □

The statement contained in Theorem 6.5 (let us call it MC^{+}) is Wolk’s original result. One reason for focusing on MC rather than on MC^{+} is that stating the latter requires the existence of the function ht_{P} which is defined using ATR_{0}. Thus we cannot state MC^{+} in RCA_{0}. Another reason for our preference for MC is the strong similarity with MLE.

As mentioned in the introduction, the proof of (3) ⟹ (1) in Theorem 1.6 is very simple.

Theorem 6.6. RCA_{0} proves that MC implies ATR_{0}.

Proof. By Theorem 2.1 it suffices to prove that if L_{0} and L_{1} are wellorders then either L_{0} ⪯ L_{1} or L_{1} ⪯ L_{0}. Given well-orders L_{0} and L_{1} let P = L_{0} ⊕ L_{1}. P is a wpo and by MC it has a maximal chain C = (C, ≤_{P}). It is immediate that either C ⊆ L_{0} or C ⊆ L_{1}, and we may assume the first possibility holds, so that C ⪯ L_{0}. Since L_{1} ∈ Ch(P) we have L_{1} ⪯ C and thus L_{1} ⪯ L_{0}. □

References

[BG08] Andreas Blass and Yuri Gurevich. Program termination and well partial orderings. ACM Trans. Comput. Log., 9(3):Art. 18, 26, 2008.

[CJS01] Peter A. Cholak, Carl G. Jockusch, and Theodore A. Slaman. On the strength of Ramsey’s theorem for pairs. J. Symbolic Logic, 66(1):1–55, 2001.

[CMS04] Peter Cholak, Alberto Marcone, and Reed Solomon. Reverse mathematics and the equivalence of definitions for well and better quasi-orders. J. Symbolic Logic, 69(3):683–712, 2004.

[dJP77] D. H. J. de Jongh and Rohit Parikh. Well-partial orderings and hierarchies. Nederl. Akad. Wetensch. Proc. Ser. A 80=Indag. Math., 39(3):195– 207, 1977.

[FH90] Harvey Friedman and Jeffry L. Hirst. Weak comparability of well orderings and reverse mathematics. Ann. Pure Appl. Logic, 47(1):11–29, 1990.

[Fra00] Roland Fraïssé. Theory of relations, volume 145 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, revised edition, 2000. With an appendix by Norbert Sauer.

[FRS87] Harvey Friedman, Neil Robertson, and Paul Seymour. The metamathematics of the graph minor theorem. In Stephen G. Simpson, editor, Proceedings of the AMS-IMS-SIAM joint summer research conference on applications of mathematical logic to finite combinatorics held at Humboldt State University, Arcata, Calif., August 4–10, 1985, pages 229–261. American Mathematical Society, Providence, R.I., 1987.

[Gir87] Jean-Yves Girard. Proof theory and logical complexity. Bibliopolis, Naples, 1987.

[Har05] Egbert Harzheim. Ordered sets, volume 7 of Advances in Mathematics (Springer). Springer, New York, 2005.

[Hig52] Graham Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2:326–336, 1952.

[Hir94] Jeffry L. Hirst. Reverse mathematics and ordinal exponentiation. Ann. Pure Appl. Logic, 66(1):1–18, 1994.

[Hir05a] Jeffry L. Hirst. Reverse mathematics and ordinal suprema. In Simpson [Sim05], pages 235–243.

[Hir05b] Jeffry L. Hirst. A survey of the reverse mathematics of ordinal arithmetic. In Simpson [Sim05], pages 222–234.

[HS07] Denis R. Hirschfeldt and Richard A. Shore. Combinatorial principles weaker than Ramsey’s theorem for pairs. J. Symbolic Logic, 72(1):171– 206, 2007.

[Kru60] J. B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture. Trans. Amer. Math. Soc., 95:210–225, 1960.

[Kru72] Joseph B. Kruskal. The theory of well-quasi-ordering: A frequently discovered concept. J. Combinatorial Theory Ser. A, 13:297–305, 1972.

[KT90] Igor Kříž and Robin Thomas. Ordinal types in Ramsey theory and wellpartial-ordering theory. In Mathematics of Ramsey theory, volume 5 of Algorithms Combin., pages 57–95. Springer, Berlin, 1990.

[Lav71] Richard Laver. On Fraïssé’s order type conjecture. Ann. of Math. (2), 93:89–111, 1971.

[Mar05] Alberto Marcone. Wqo and bqo theory in subsystems of second order arithmetic. In Simpson [Sim05], pages 303–330.

[MM09] Alberto Marcone and Antonio Montalbán. On Fraïssé’s conjecture for linear orders of finite Hausdorff rank. Ann. Pure Appl. Logic, 160(3):355– 367, 2009.

[Mon07] Antonio Montalbán. Computable linearizations of well-partial-orderings. Order, 24(1):39–48, 2007.

[MS81] E. C. Milner and N. Sauer. On chains and antichains in well-founded partially ordered sets. J. London Math. Soc. (2), 24(1):15–33, 1981.

[NW65] C. St. J. A. Nash-Williams. On well-quasi-ordering transfinite sequences. Proc. Cambridge Philos. Soc., 61:33–39, 1965.

[NW68] C. St. J. A. Nash-Williams. On better-quasi-ordering transfinite sequences. Proc. Cambridge Philos. Soc., 64:273–290, 1968.

[RS04] Neil Robertson and P. D. Seymour. Graph minors. XX. Wagner’s conjecture. J. Combin. Theory Ser. B, 92(2):325–357, 2004.

[Sch79] Diana Schmidt. Well-partial Orderings and Their Maximal Order Types. Habilitationschrift, Heidelberg University, 1979.

[Sch81] Diana Schmidt. The relation between the height of a well-founded partial ordering and the order types of its chains and antichains. J. Combin. Theory Ser. B, 31(2):183–189, 1981.

[Sho93] Richard A. Shore. On the strength of Fraïssé’s conjecture. In John N. Crossley, Jeffrey B. Remmel, Richard A. Shore, and Moss E. Sweedler, editors, Logical methods, volume 12 of Progress in Computer Science and Applied Logic, pages 782–813. Birkhäuser Boston Inc., Boston, MA, 1993. Papers from the conference in honor of Anil Nerode’s sixtieth birthday held at Cornell University, Ithaca, New York, June 1–3, 1992.

[Sim85] Stephen G. Simpson. Nonprovability of certain combinatorial properties of finite trees. In L. A. Harrington, M. D. Morley, A. Ščedrov, and S. G. Simpson, editors, Harvey Friedman’s research on the foundations of mathematics, pages 87–117. North-Holland, Amsterdam, 1985.

[Sim88] Stephen G. Simpson. Ordinal numbers and the Hilbert basis theorem. J. Symbolic Logic, 53(3):961–974, 1988.

[Sim05] Stephen G. Simpson, editor. Reverse mathematics 2001, volume 21 of Lecture Notes in Logic. Association for Symbolic Logic, La Jolla, CA, [Sim09] Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives

in Logic. Cambridge University Press, Cambridge, second edition, 2009.

[Tho95] Carsten Thomassen. Embeddings and minors. In R. L. Graham, M. Grötschel, and L. Lovász, editors, Handbook of combinatorics, Vol. 1, pages 301–349. Elsevier Science, Amsterdam, 1995.

[Wol67] E. S. Wolk. Partially well ordered sets and partial ordinals. Fund. Math., 60:175–186, 1967.

Dipartimento di Matematica e Informatica, Università di Udine, 33100 Udine, Italy

  E-mail address: alberto.marcone@dimi.uniud.it

Department of Mathematics, Cornell University, Ithaca, NY 14853, USA

  E-mail address: shore@math.cornell.edu