Combinatorial Principles Weaker than Ramsey’s Theorem for Pairs

Denis R. Hirschfeldt Department of Mathematics

University of Chicago Chicago IL 60637

Richard A. Shore Department of Mathematics Cornell University Ithaca NY 14853

Abstract

We investigate the complexity of various combinatorial theorems about linear and partial orders, from the points of view of computability theory and reverse mathematics. We focus in particular on the principles ADS (Ascending or Descending Sequence), which states that every infinite linear order has either an infinite descending sequence or an infinite ascending sequence, and CAC (Chain-AntiChain), which states that every infinite partial order has either an infinite chain or an infinite antichain. It is well-known that Ramsey’s Theorem for pairs (RT_{2}^{2}) splits into a stable version (SRT_{2}^{2}) and a cohesive principle (COH). We show that the same is true of ADS and CAC, and that in their cases the stable versions are strictly weaker than the full ones (which is not known to be the case for RT_{2}^{2} and SRT_{2}^{2}). We also analyze the relationships between these principles and other systems and principles previously studied by reverse mathematics, such as WKL_{0}, DNR, and BΣ_{2}. We show, for instance, that WKL_{0} is incomparable with all of the systems we study. We also prove computability-theoretic and conservation results for them. Among these results are a strengthening of the fact, proved by Cholak, Jockusch, and Slaman, that COH is Π_{1}^{1}-conservative over the base system RCA_{0}. We also prove that CAC does not imply DNR which, combined with a recent result of Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman, shows that CAC does not imply SRT_{2}^{2} (and so does not imply RT_{2}^{2}). This answers a question of Cholak, Jockusch, and Slaman.

Our proofs suggest that the essential distinction between ADS and CAC on the one hand and RT_{2}^{2} on the other is that the colorings needed for our analysis are in some way transitive. We formalize this intuition as the notions of transitive and semitransitive colorings and show that the existence of homogeneous sets for such colorings is equivalent to ADS and CAC, respectively. We finish with several open questions.

Hirschfeldt’s research was partially supported by NSF Grants DMS-0200465 and DMS-0500590.

Shore’s research was partially supported by NSF Grant DMS-0100035.

We thank the Institute for Mathematical Sciences of the National University of Singapore for its generous support during the period July 18 – August 15, 2005, when part of this research was done.

1 Introduction

In this paper we investigate the complexity of various combinatorial theorems about linear and partial orders. We are interested in both computational (computability theoretic) and proof theoretic (reverse mathematical) calibrations and in the interplay between them. The theorems of interest in such investigations are typically of the form ∀A (Θ(A) → ∃B Φ(A, B)) where Θ and Φ are arithmetic and A, B ∈ 2^{ω}. Thus, from the computability theoretic point of view,we want to bound or characterize the computational complexity of B given an A satisfying Θ (typically in terms of Turing degree or place in one of the standard arithmetic/analytic definability or jump hierarchies). From the reverse mathematics point of view we want to determine the axiom systems in which the theorem is provable (typically subsystems of second order arithmetic determined by the amount of comprehension assumed). Here, characterizations correspond to reversals in the sense that one proves (over some weak system) the axioms of one of the subsystems of second order arithmetic from the statements of the mathematical theorems being investigated.

We briefly review the five standard systems of reverse mathematics. For completeness, we include systems stronger than arithmetical comprehension, but these will play no part in this paper. Details, general background, and results, as well as many examples of reversals, can be found in Simpson [1999], the standard text on reverse mathematics. Each of the systems is given in the language of second order arithmetic, that is, the usual first order language of arithmetic augmented by set variables and the membership relation ∈. Each contains the standard basic axioms for +, ·, and < (which say that ℕ is an ordered semiring). In addition, they all include a form of induction that applies only to sets (that happen to exist):

(I_{0}) (0 ∈ X ∧ ∀n (n ∈ X → n + 1 ∈ X)) → ∀n (n ∈ X).

We call the system consisting of I_{0} and the basic axioms of ordered semirings P_{0}. All the five standard systems are defined by adding various types of set existence axioms to P_{0}. They also correspond to classical construction principles in computability theory.

(RCA_{0}) Recursive Comprehension Axioms: This is a system just strong enough to prove the existence of the computable sets but not of 0′ nor indeed of any noncomputable set. In addition to P_{0} its axioms include the schemes of Δ_{1}^{0} comprehension and Σ_{1}^{0} induction:

(Δ_{1}^{0}-CA_{0}) ∀n (φ(n) ↔ ψ(n)) → ∃X ∀n (n ∈ X ↔ φ(n)) for all Σ_{1}^{0} formulas φ and Π_{1}^{0} formulas ψ in which X is not free.

(IΣ_{1}) (φ(0) ∧ ∀n (φ(n) → φ(n + 1))) → ∀n φ(n) for all Σ_{1}^{0} formulas φ.

The next system says that every infinite binary tree has an infinite path. It is connected to the Low Basis Theorem (Jockusch and Soare [1972]) of computability theory, which says that every such tree has an infinite path whose jump is computable in that of the tree itself.

(WKL_{0}) Weak König’s Lemma: This system consists of RCA_{0} plus the statement that every infinite subtree of 2^{<ω} has an infinite path.

We next move up to arithmetic comprehension.

(ACA_{0}) Arithmetic Comprehension Axioms: This system consists of RCA_{0} plus the axioms ∃X ∀n (n ∈ X ↔ φ(n)) for every arithmetic formula φ in which X is not free.

In computability theoretic terms, ACA_{0} proves the existence of 0′ and by relativization it proves, and in fact is equivalent to, the existence of X′ for every set X.

The next system corresponds to the existence of all (relativized) H-sets, i.e. the existence, for every set X, of the H_{e}^{X} (and so the hyperarithmetic hierarchy up to e) for each e ∈ O^{X}, the hyperjump of X. It says that arithmetic comprehension can be iterated along any countable well order.

(ATR_{0}) Arithmetical Transfinite Recursion: This system consists of RCA_{0} plus the following axiom. If X is a set coding a well order <_{X} with domain D and Y is a code for a set of arithmetic formulas φ_{x}(z, Z) (indexed by x ∈ D) each with one free set variable and one free number variable, then there is a sequence ⟨K_{x} | x ∈ D⟩ of sets such that if y is the immediate successor of x in <_{X}, then ∀n (n ∈ K_{y} ↔ φ_{x}(n, K_{x})), and if x is a limit point in <_{X}, then K_{x} is ⨁{K_{y} | y <_{X} x}.

The systems climbing up to full second order arithmetic (i.e. comprehension for all formulas) are classified by the syntactic level of the second order formulas for which we assume a comprehension axiom.

(Π_{n}^{1}-CA_{0}) Π_{n}^{1} Comprehension Axioms: ∃X ∀k (k ∈ X ↔ φ(k)) for every Π_{n}^{1} formula φ in which X is not free.

The computability theoretic equivalent of the simplest of these systems, Π_{1}^{1}-CA_{0}, is the existence of O^{X} for every set X. Together with the four systems listed above, it makes up the standard list of the axiomatic systems of reverse mathematics. Almost all theorems of classical mathematics whose proof theoretic complexity has been determined have turned out to be equivalent to one of them.

The early connections between computability theoretic ideas and methods on the one hand and reverse mathematics in the other typically involved computable mathematics, diagonalization or finite injury arguments, and coding. Consider, for example, a theorem of the form ∀A (Θ(A) → ∃B Φ(A, B)) where Θ and Φ are arithmetic. We call B a solution for the instance of the theorem specified by A if Θ(A) → Φ(A, B).

A construction of computable mathematics that shows that there is a solution B computable in any given A generally shows that the theorem is provable in RCA_{0}. One that shows that B can be obtained arithmetically in A usually shows that the theorem is provable in ACA_{0}. Standard forms of applications of computability theoretic diagonalization or finite injury results to reverse mathematical calibrations are as follows:

1. If there is no solution B computable in some given A then the theorem is not provable in RCA_{0}.

2. If there is no solution B that is low over A, i.e. (B ⊕ A)′ ≡_{T} A′, then the theorem is not provable in WKL_{0}.

3. If there is no solution B arithmetic in A then the theorem is not provable in ACA_{0}.

Coding methods tend to give reversals.

1. If, for any computable tree T, there is a computable instance of the theorem such that any solution codes a path through T then the theorem usually implies WKL_{0}.

2. If there is a computable instance of the theorem such that any solution computes 0′ then the theorem usually implies ACA_{0}.

3. If there is a computable instance of the theorem such that any solution computes O then the theorem usually implies Π_{1}^{1}-CA_{0}.

We are particularly interested in relations derived from more complex computability theoretic results and constructions, and in theorems that do not correspond to any of the standard systems. In this paper we deal with ones that are strictly below ACA_{0}. A special inspiration for our investigations here comes from the work of Cholak, Jockusch, and Slaman [2001] (hereafter CJS). They deal with various versions of Ramsey’s Theorem and some of their consequences. (Their paper is also a good source of background information and history.) We will summarize some of their results to set the stage for ours, which deal with other consequences of Ramsey’s Theorem applied to linear and partial orders. We begin with the statements of some of the theorems they analyze and basic results about their strength. We view each of these theorems as a subsystem of second order arithmetic by adding it to RCA_{0}. For a map f and a subset X of its domain, we denote the image of X under f by f“X.

Definition 1.1. An n-coloring (partition) of [ℕ]^{k}, the unordered k-tuples (n_{1}, …, n_{k}) of natural numbers (listed by convention in increasing order), is a map f : [ℕ]^{k} → n. A subset H of ℕ is homogeneous for the coloring f if H is infinite and |f“[H]^{k}| = 1. Unless otherwise stated all colorings will be 2-colorings of [ℕ]^{2}.

(RT_{2}^{2}) Ramsey’s Theorem for pairs: Every 2-coloring of [ℕ]^{2} has a homogeneous set.

It is easy to show that the number of colors does not matter, in the sense that for each n > 2, Ramsey’s Theorem for 2-colorings of pairs is equivalent to Ramsey’s Theorem for n-colorings of pairs. As we will see, however, the size of the tuples does matter.

Ramsey’s Theorem, its variants and their consequences have long been a subject of great interest in terms of characterizing their complexity in both computability theoretic and proof theoretic terms. Specker [1971] constructed a computable coloring of [ℕ]^{2} with no computable homogeneous set. Thus RCA_{0} ⊬ RT_{2}^{2}. A now classic early result concerns the analog for colorings of triples. Jockusch [1972] constructed a computable coloring of [ℕ]^{3} such that every homogeneous set computes 0′. This construction can be carried out in RCA_{0}, and thus shows that Ramsey’s Theorem for triples implies ACA_{0}. (All such statements about implications will be understood to be over the base theory RCA_{0} unless some other system is specifically mentioned.) In fact, one of the standard proofs of Ramsey’s Theorem for k-tuples works in ACA_{0} (for any fixed k), and so for each k > 2, Ramsey’s Theorem for k-tuples is equivalent to ACA_{0}. Whether RT_{2}^{2} itself also implies ACA_{0} remained open for twenty years. Seetapun (see Seetapun and Slaman [1995]) proved a degree theoretic cone avoiding theorem (for every set Z, coloring f of [ℕ]^{2} computable in Z, and sets C_{i} ⩽̸_{T} Z, there is a homogeneous set not computing any C_{i}) that implies that RT_{2}^{2} does not imply ACA_{0} (even over WKL_{0}).

Another view of the proof theoretic strength of such theorems and systems is provided by the analysis of their first order consequences and conservativity results. For example, even though WKL_{0} is strictly stronger than RCA_{0}, the former is Π_{1}^{1}-conservative over the latter (Harrington, see Simpson [1999, §IX.2]), i.e. any Π_{1}^{1} sentence provable in WKL_{0} is already provable in RCA_{0}. Thus, in particular, the first order consequences and consistency strengths of the two systems are the same. While it is a major open question whether RT_{2}^{2} actually implies WKL_{0}, RT_{2}^{2} is known to be strictly stronger than WKL_{0} in this proof theoretic sense. The relevant principle is Σ_{2}-bounding. We state the bounding principle as well as the related induction principle for an arbitrary class Γ of formulas.

(BΓ) (∀i < n)(∃x)φ(x) → (∃u)(∀i < n)(∃x < u)φ(x) for every formula φ(x) ∈ Γ.

(IΓ) (φ(0) ∧ ∀n (φ(n) → φ(n + 1))) → ∀n φ(n) for every formula φ(x) ∈ Γ.

Now these principles produce a strict hierarchy in both first and second order arithmetic, with BΣ_{n+1} caught strictly between IΣ_{n} and IΣ_{n+1} (Paris and Kirby [1978], see also Hájek and Pudlák [1998. IV]). Moreover, even in the first order case, BΣ_{n+1} is not Σ_{n+2}^{0}-conservative over IΣ_{n} (Paris [1980, p. 331]). Thus, as Hirst [1987] showed that RT_{2}^{2} implies BΣ_{2}, RT_{2}^{2} is not even Σ_{3}^{0}-conservative over RCA_{0}. (By Friedman [1976], any model M of IΣ_{n} can always be extended to a model of RCA_{0} + IΣ_{n} with the same first order part by taking the sets to be those with Δ_{1}^{0} definitions over M.) On the other hand, CJS show that RT_{2}^{2} is Π_{1}^{1}-conservative over IΣ_{2} and so far weaker, in this sense, than ACA_{0}, which obviously implies IΣ_{n} for each n.

The more recent analyses of RT_{2}^{2}, both computability theoretic and proof theoretic, have crucially relied on splitting the theorem/system into two parts. One (COH) is used to simplify the coloring and make it stable. The other (SRT_{2}^{2}) restricts the assertion of the existence of homogeneous sets to stable colorings.

Definition 1.2. A coloring f of [ℕ]^{2} is stable if (∀x)(∃y)(∀z > y)[f(x, y) = f(x, z)].

Definition 1.3. If R⃗ = ⟨R_{i} | i ∈ ℕ⟩ is a sequence of sets, an infinite set S is R⃗-cohesive if (∀i)(∃s)[(∀j > s)(j ∈ S → j ∈ R_{i}) ∨ (∀j > s)(j ∈ S → j ∉ R_{i})].

(SRT_{2}^{2}) Stable Ramsey’s Theorem for pairs: Every stable coloring of [ℕ]^{2} has a homogeneous set.

(COH) Cohesive Principle: For every sequence R⃗ = ⟨R_{i} | i ∈ ℕ⟩ there is an R⃗- cohesive set.

Note that COH easily implies the following principle, which asserts that for every coloring of [ℕ]^{2} there is a set such that the coloring restricted to that set is stable (in the obvious sense).

(CRT_{2}^{2}) Cohesive Ramsey’s Theorem for pairs: For every coloring f of [ℕ]^{2} there is an infinite set S such that (∀x ∈ S)(∃y)(∀z ∈ S)[z > y → f(x, y) = f(x, z)].

Proposition 1.4 (CJS). RCA_{0} ⊢ COH → CRT_{2}^{2}.

Proof. If f is a coloring of [ℕ]^{2} and we set R_{i} = {j > i | f(i, j) = 0} then any R⃗-cohesive set S is as required in CRT_{2}^{2}.

By the theorem and system RT_{2}^{2} splitting into SRT_{2}^{2} and COH we mean the fact that RCA_{0} ⊢ RT_{2}^{2} ↔ COH ∧ SRT_{2}^{2}. It is immediate from the above proposition that COH ∧ SRT_{2}^{2} implies RT_{2}^{2}, and RT_{2}^{2} obviously implies SRT_{2}^{2}. The fact that RT_{2}^{2} implies COH is harder to show. CJS provide (in the proof of Theorem 12.5) an easy proof that requires IΣ_{2}. Their proof in RCA_{0} (in Theorem 7.11) is not correct but a more complicated argument that dispenses with IΣ_{2} is given by Mileti [2004] (and was independently discovered by Jockusch and Lempp). The converse of Proposition 1.4 is clearly related to this issue as well as to alternate versions of other principles related to BΣ_{2} that we consider in §4. For now we note that there are natural stronger forms of each of these principles (StCRT_{2}^{2} and StCOH, respectively) that are equivalent to each other and to CRT_{2}^{2} + BΣ_{2} and COH + BΣ_{2}, respectively, and so CRT_{2}^{2} + BΣ_{2} implies COH (Proposition 4.8).

Principles lying below WKL_{0} have also been studied. A function f is diagonally noncomputable relative to A if ∀e (f(e) ≠ Φ_{e}^{A}(e)), where Φ_{e} is the eth Turing functional.

(DNR) Diagonally Nonrecursive Principle: For every set A there is a function f that is diagonally noncomputable relative to A.

Clearly, DNR fails in COMP, the ω-model of RCA_{0} whose sets are precisely the computable sets. (An ω-model is a structure in the language of second order arithmetic whose first order part is standard.) Giusto and Simpson [2000] showed that DNR follows from the system WWKL_{0}, which states that if a binary tree T has no infinite path then lim_{n} |{σ ∈ T | |σ| = n}|/2^{n} = 0, and has played a role in studying the proof theoretic content of theorems from analysis, as it is strong enough to develop a fair amount of measure theory. The system WWKL_{0} was shown to be strictly weaker than WKL_{0} by Simpson and Yu [1990] but strictly stronger than DNR by Ambos-Spies, Kjos-Hanssen, Lempp, and Slaman [2004]. Recently, Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta] have shown that DNR follows from SRT_{2}^{2} over RCA_{0}.

We now summarize the known degree theoretic results (primarily from CJS) about the above principles related to Ramsey’s Theorem. Some of them directly give reverse mathematical results and the proofs of others play a crucial role in conservativity results. We also include previous results about WKL_{0} to help place it with respect to these systems.

Definition 1.5. A degree a is PA over b, written a ≫ b, if a computes a separating set for any pair of disjoint sets c.e. in b; or, equivalently, an infinite path in any infinite tree computable in b; or a total extension for any {0, 1}-valued function partial computable in b. (See Simpson [1977, pp. 648-649] and CJS, §4.8.) In this case, if A ∈ a and B ∈ b, we also write A ≫ B.

COH: Every uniformly computable sequence R⃗ has a Δ_{2}^{0} cohesive set, but for some such R⃗ the only Δ_{2}^{0} cohesive sets S are high, i.e. S′ ≡_{T} 0′′ (Cooper [1972], Jockusch and Stephan [1993]). Moreover, for any degree d ≫ 0′ every uniformly computable sequence R⃗ has a cohesive set S with S′ ⩽_{T} d. As there are d ≫ 0′ with d′ = 0′′ we may always take S to be low_{2}, i.e. S′′ ≡_{T} 0′′. There is also a single such R⃗ (the sequence of primitive recursive sets) such that for any S cohesive for it, S′ ≫ 0′ (Jockusch and Stephan [1993]). COH is also Π_{1}^{1}-conservative over RCA_{0} (CJS).

SRT_{2}^{2}: It is easy to see that every computable stable coloring of [ℕ]^{2} has a Δ_{2}^{0} homogeneous set, but there are such colorings that have no low homogeneous set (Downey, Hirschfeldt, Lempp and Solomon [2001]). On the other hand, every such coloring has a low_{2} homogeneous set (CJS). SRT_{2}^{2}, like RT_{2}^{2}, proves BΣ_{2} and so is not even Σ_{3}^{0}- conservative over RCA_{0} (CJS).

RT_{2}^{2}: There are computable colorings of [ℕ]^{2} with no Δ_{2}^{0} homogeneous sets (Jockusch [1972]) but, by combining the above results for COH and SRT_{2}^{2}, all have low_{2} ones (CJS). Indeed, for any degree d ≫ 0′ and any computable coloring of [ℕ]^{2} there is a homogeneous set H with H′ ⩽_{T} d (CJS). Moreover, there is a computable coloring of [ℕ]^{2} such that H′ ≫ 0′ for any homogeneous set H. As RT_{2}^{2} proves BΣ_{2}, it is not Σ_{3}^{0}-conservative over RCA_{0}.

WKL_{0}: As mentioned before, WKL_{0} is Π_{1}^{1}-conservative over RCA_{0} (Harrington). The degree theoretic precursor to this conservation result is the Low Basis Theorem of Jockusch and Soare [1972], which says that every infinite computable tree has a low infinite path. Indeed, there is a single low degree d that computes an infinite path through any computable infinite tree, i.e. a low d ≫ 0 (this follows from the Low Basis Theorem and the equivalence of various standard characterizations of a ≫ 0 as in CJS, Lemma 8.17).

The following diagram summarizes our state of knowledge about the relations among these four systems (as well as DNR and BΣ_{2}) as presented primarily in CJS. Double arrows indicate a strict implication and single ones an implication that is not known to be strict. Negated arrows indicate known nonimplications.

[figure: ACA_{0}; (1); (3,6); _{RT2 2}; (2); _{WKL_{0}}; |; (3); (4); |; (6); _{SRT2 2}; (7); (2,6); COH; |; (2); (7); |; (3,5); DNR; (7); BΣ_{2}; |; (6,7); (7); DNR; |; (6,7); (7); BΣ_{2}; (7); _{RCA_{0}}]

Diagram 1

The reasons for the nonimplications indicated here have all been described and attributed above and are listed below. The implications are all easy except for the following: RT_{2}^{2} → COH, which was shown by CJS in the presence of IΣ_{2} and in general by Mileti [2004] and Jockusch and Lempp; SRT_{2}^{2} → BΣ_{2} (CJS); and SRT_{2}^{2} → DNR (Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta]).

1. The degree theoretic cone avoiding argument of Seetapun (in Seetapun and Slaman [1995]) or the conservation result over IΣ_{2} of CJS, Theorem 10.2.

2. COH is Π_{1}^{1}-conservative over RCA_{0} (CJS, Theorem 9.1) but RT_{2}^{2} is not as it implies BΣ_{2} (Hirst [1987]). In fact, even SRT_{2}^{2} implies BΣ_{2} (CJS).

3. WKL_{0}, and hence DNR, have a model with only low sets but COH does not.

4. The results of Simpson and Yu [1990] and Giusto and Simpson [2000] mentioned above.

5. That COH does not imply WKL_{0} is proved in CJS by a direct forcing argument. (See CJS, §9.5 for both directions.) We supply a stronger, more general conservation result along these lines in Theorem 2.20 and Proposition 2.21, which also applies to DNR. Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta] have also shown that COH does not imply DNR.

6. WKL_{0}, and hence DNR, are Π_{1}^{1}-conservative over RCA_{0} (Harrington, see Simpson [1999, §IX.2]) and so do not imply BΣ_{2}.

7. None of the five principles RT_{2}^{2}, SRT_{2}^{2}, COH, WKL_{0}, and DNR follow from RCA_{0} (even with full induction) as they all have computable instances without computable solutions as described above. BΣ_{2} is not a consequence of RCA_{0} either (Paris and Kirby [1978], see also Hájek and Pudlák [1998, Chapter IV]).

The primary combinatorial/reverse mathematical questions left open here are whether SRT_{2}^{2} implies COH (and so RT_{2}^{2}) and whether SRT_{2}^{2} or RT_{2}^{2} implies WKL_{0}. The primary purely proof theoretic one is whether SRT_{2}^{2} or RT_{2}^{2} is arithmetically conservative over BΣ_{2}. In addition, CJS raise the issue of a specific application of RT_{2}^{2} to partial orders and ask about its relation to RT_{2}^{2}.

(CAC) Chain-AntiChain: Every infinite partial order (P, ⩽_{P}) has an infinite subset S that is either a chain, i.e. (∀x, y ∈ S)(x ⩽_{P} y ∨ y ⩽_{P} x), or an antichain, i.e. (∀x, y ∈ S)(x ≠ y → (x ⩽̸_{P} y ∧ y ⩽̸_{P} x)).

It is easy to see that RT_{2}^{2} implies CAC just by coloring (x, y) 0 (red) if x and y are comparable in ⩽_{P} and 1 (blue) otherwise. Any homogeneous set is the required chain or antichain. It was left as Question 13.8 in CJS whether CAC implies RT_{2}^{2}. CAC is degree theoretically similar to RT_{2}^{2}, as by Herrmann [2001] there are computable partial orders with no Δ_{2}^{0} infinite chains or antichains. However, we show (Corollary 3.11) that CAC does not imply DNR (over RCA_{0}). Combining this with the result of Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta] mentioned above, we now know that CAC does not imply even SRT_{2}^{2}.

There is a well known analogous principle for linear orders. (We typically use ⩽ to denote the usual ordering on ℕ, though in some cases we use ⩽_{ℕ} to avoid possible confusion.)

(ADS) Ascending or Descending Sequence: Every infinite linear order (L, ⩽_{L}) has an infinite subset S that is either an ascending sequence, i.e. (∀s < t)(s, t ∈ S → s <_{L} t), and so of order type ω, or a descending sequence, i.e. (∀s < t)(s, t ∈ S → t <_{L} s), and so of order type ω^{∗}.

This principle also follows easily from RT_{2}^{2} by coloring (x, y) red if x <_{L} y and blue otherwise, i.e. x >_{L} y. Here it is known that there is a computable linear order (even one of type ω + ω^{∗}) with no computable ascending or descending sequence (Tennenbaum (see Rosenstein [1982]) and Denisov (see Goncharov and Nurtazin [1973])). Thus RCA_{0} ⊬ ADS. On the other hand, every computable linear order has an ascending or descending sequence computable in 0′, in fact one that is Π_{1}^{0} (Manaster; see Downey [1998, §5] for this and all the results we mention about these issues).

Our goal is to analyze both CAC and ADS computability theoretically and in the terms of reverse mathematics along the lines followed for RT_{2}^{2} in CJS. Each will be split into a stable version (SCAC; SADS) and a cohesive principle (CCAC; CADS (or related principles that work for both)). In these situations, however, along with various other degree and proof theoretic results, we will be able to show that the splittings are strict (that is, SCAC and SADS do not imply CAC and ADS, respectively, nor do CADS, COH, or CCAC). Moreover, none of these principles will imply DNR or be implied by WKL_{0}. We will also study the relationship between BΣ_{2} and these principles and prove some conservation results extending those for COH over RCA_{0}. Our methods will include priority arguments, forcing constructions, and computable combinatorics.

Our proofs suggest that the essential distinction between ADS and CAC on the one hand and RT_{2}^{2} on the other is that the colorings needed for our analysis are in some way transitive. We formalize this intuition in §5 as the notions of transitive and semitransitive colorings and show that the existence of homogeneous sets for such colorings is equivalent to ADS and CAC, respectively.

We begin with linear orders and some classical computability theoretic results about ADS which motivated our choice of principles and analysis. From now on, all linear or partial orders and chains or antichains within them will be assumed to be infinite unless otherwise stated. When we consider a linear order L, we denote its order relation by ⩽_{L}. Similarly, we denote the order relation of a partial order P by ⩽_{P}.

2 Linear Orders and ADS

An infinite linear order is computable if it has domain ℕ and its ordering relation is computable. There are a number of interesting classical results of computable mathematics about the existence and complexity types of suborders of, and embeddings into, an arbitrary computable linear order. A good reference including proofs is Downey [1998]. The ones relevant to our investigations have to do with suborders of a given order L of order type ω, ω^{∗}, or ω + ω^{∗} (or embeddings of canonical representatives of these types into L). We now state the ones we need.

Theorem 2.1. (Tennenbaum (see Rosenstein [1982]) and Denisov (see Goncharov and Nurtazin [1973]); see also Downey [1998]) There is a computable linear order of type ω + ω^{∗} with no computable suborder of type ω or ω^{∗}.

The proof involves a finite injury priority argument.

Theorem 2.2. (Lerman [1981]) There is a computable linear order with no computable suborder of type ω, ω^{∗}, or ω + ω^{∗}.

The proof here uses an infinite injury priority argument.

These theorems suggest principles that would be shown by them to be not provable in RCA_{0}. To state and analyze them in the setting of reverse mathematics we should first be precise about what we mean by having order type ω, ω^{∗}, and ω + ω^{∗} in RCA_{0}.

Definition 2.3. An infinite linear order in which all nonfirst elements have immediate predecessors and all nonlast ones have immediate successors has type • ω if every element has finitely many predecessors;.

• ω^{∗} if every element has finitely many successors;

• ω + ω^{∗} if it is not of type ω or ω^{∗} and every element has either finitely many predecessors or finitely many successors.

Proposition 2.4. ADS is equivalent over RCA_{0} to the statement that every linear order L has a suborder of type ω or ω^{∗}.

Proof. An ascending or descending sequence in L is clearly a suborder of type ω or ω^{∗}, respectively. In the other direction, suppose we are given a subset R of L of order type ω in the order inherited from L (the ω^{∗} case being symmetric). We can, in RCA_{0}, define by recursion a function that lists an infinite subset S = ⟨s_{i} | i ∈ ℕ⟩ of R in increasing natural order (the order of ℕ). Having defined s_{n}, we need only find an a ∈ R such that a >_{L} s_{n} and a >_{ℕ} s_{n}, which exists because R has order type ω, and define s_{n+1} = a, so this recursion can be performed in RCA_{0}. The range of S exists provably in RCA_{0}, because every element b of R has only finitely many predecessors, and hence there is an i such that b <_{L} s_{i}. If b ≠ s_{j} for j < i, then b is not in the range of S. The range of S is the desired ascending sequence in L.

Corollary 2.5. RCA_{0} ⊬ ADS.

Proof. By Theorem 2.1, COMP, the ω-model of RCA_{0} whose sets are precisely the computable sets, is not a model of ADS.

Every linear order L of type ω +ω^{∗} is stable in a sense analogous to that for colorings, i.e. (∀x)(∃y)(∀z > y)[x <_{L} y ↔ x <_{L} z]. Thus the analog of SRT_{2}^{2} is SADS:

(SADS) Stable ADS: Every linear order of type ω + ω^{∗} has a subset of order type ω or ω^{∗}.

Similarly, reducing to an order of type ω + ω^{∗} corresponds to producing a cohesive set, as in such an order S, we have (∀i ∈ S)(∃s)[(∀j > s)(j ∈ S → i <_{L} j) ∨ (∀j > s)(j ∈ S → i >_{L} j)]. This gives us CADS as the analog of COH.

(CADS) Cohesive ADS: Every linear order has a subset S of order type ω, ω^{∗}, or ω + ω^{∗}.

Of course, CADS says that every linear order has a stable suborder the same way that CRT_{2}^{2} or COH say that for every coloring there is a set on which the coloring is stable. Theorems 2.1 and 2.2 now prove that these principles do not hold in COMP and so do not follow from RCA_{0}.

Corollary 2.6. RCA_{0} ⊬ SADS; RCA_{0} ⊬ CADS.

As with RT_{2}^{2}, it is immediate that these principle split ADS.

Proposition 2.7. RCA_{0} ⊢ ADS ↔ SADS + CADS.

We show that they also follow from SRT_{2}^{2} and COH, respectively.

Proposition 2.8. RCA_{0} ⊢ SRT_{2}^{2} → SADS.

Proof. Given a linear order L of type ω + ω^{∗}, color (m, n) blue if m <_{L} n; otherwise, i.e. if n <_{L} m, color (m, n) red. This is a stable coloring by the definition of order type ω + ω^{∗}. A blue homogeneous set has order type ω. A red one has order type ω^{∗}.

Proposition 2.9. RCA_{0} ⊢ CRT_{2}^{2} → CADS and so RCA_{0} ⊢ COH → CADS.

Proof. Given a linear ordering L, color (m, n) blue if m <_{L} n; otherwise color (m, n) red. Let S be a set given by CRT_{2}^{2} for this coloring. Then the coloring restricted to S is stable, which means that each element of S has either finitely many <_{L}-predecessors in S or finitely many <_{L}-successors in S, as required.

In addition, we have one more combinatorial connection between ADS and COH.

Proposition 2.10. RCA_{0} ⊢ ADS → COH.

Proof. Given R⃗ = ⟨R_{i} | i ∈ ℕ⟩ define a linear order L on ℕ by setting x <_{L} y ↔ ⟨R_{i}(x) | i ⩽ x⟩ <_{lex} ⟨R_{i}(y) | i ⩽ y⟩, where <_{lex} is the lexicographic order on 2^{<ω}. This order is just the lexicographic order on a subset of 2^{<ω} that contains exactly one string of each length. We claim that any infinite ascending or descending sequence S in this order is R⃗-cohesive. Suppose S is ascending (the descending case being symmetric) and consider any j ∈ ℕ. Let σ ∈ 2^{j+1} be the lexicographically largest element of 2^{j+1} such that σ ⩽_{lex} ⟨R_{i}(x) | i ⩽ x⟩ for some x ∈ S. (Such a σ exists by Σ_{1}^{0} induction.) Fix such an x. Since S is ascending in L, for every element y ⩾_{ℕ} x of S, we have σ ⩽

lex⟨R_{i}(y) | i ⩽ j⟩. But no such sequence can be to the right of σ by our choice of σ. Thus ⟨R_{i}(y) | i ⩽ j⟩ = σ for every y ⩾_{ℕ} x in S. In particular, R_{j}(y) has the same value for cofinitely many y ∈ S, and so S is R⃗-cohesive as desired.

We now turn to a degree theoretic analysis of these principles that will provide proofs that most of the above implications cannot be reversed. For the first one we provide a priority argument here and a forcing one for a related result that could be adapted to a proof of this theorem in Proposition 3.4. The forcing argument is simpler and probably easier to understand than this one, so readers who prefer that kind of argument may wish to skip this proof. On the other hand, this argument is relevant to issues of conservativity, and in particular contrasts with a similar argument in an upcoming paper by Hirschfeldt, Shore, and Slaman on the Atomic Model Theorem, in which a blocking technique is employed that does not work in this case. See §6 for further discussion of conservativity issues in relation to the following proof.

Theorem 2.11. Every X-computable linear order of type ω + ω^{∗} contains a suborder A of type ω or ω^{∗} that is low over X, i.e. (A ⊕ X)′ ⩽_{T} X′.

Proof. We consider the case that X is computable. The general one follows by relativization. Let ≺ be a computable linear order of type ω + ω^{∗}. Let U be the ω part of ≺. Clearly, U is Δ_{2}^{0}. We build an infinite Δ_{2}^{0} subset A of U such that if A is not low then ≺ contains an infinite computable descending sequence. Of course, from A we can computably obtain an infinite ascending sequence in ≺.

We have two kinds of requirements:

P_{e} : (∃n > e)(n ∈ A)

and

N_{e} : ∃^{∞}s (Φ_{e}^{A}(e)[s]↓) → Φ_{e}^{A}(e)↓ .

We assign priorities to these requirements in the usual way. We denote the use function of Φ_{e} by φ_{e}.

The idea for satisfying N_{e} is that, whenever Φ_{e}^{A}(e)[s] ↓, we try to preserve A[s] ↾ φ_{e}^{A}(e)[s] to the extent allowed by the need to ensure that A ⊆ U. If we fail, then U[s] ↾ φ_{e}^{A}(e)[s] must contain an element not in U. Because U is an initial segment of ≺, this means that the ≺-last element of U[s] ↾ φ_{e}^{A}(e)[s] must be in \overline{U}. So if ∃^{∞}s (Φ_{e}^{A}(e)[s]↓) but Φ_{e}^{A}(e)↑, which means that all our attempts at preservation fail, then we have a computable list of elements of \overline{U}, from which we can obtain a computable infinite descending sequence in ≺.

We adopt the convention that if a computation changes then it becomes undefined for at least one stage. We also assume we have speeded up the computable approximation to U so that for any s there is an element of U[s] greater than every number mentioned in the construction before stage s. We also assume that the approximation obeys the order, i.e. if n ≺ m and m ∈ U[t] then n ∈ U[t].

At stage s, we say that P_{e} requires attention if the ≺-least element of U[s] larger (in the ℕ sense) than e and the restraints of stronger priority N-requirements is not in A. We say that N_{e} requires attention if either

1. Φ_{e}^{A}(e)[s − 1]↑ and Φ_{e}^{A}(e)[s]↓, or

2. Φ_{e}^{A}(e)[s]↑ and there is a t < s such that

(a) t is greater than the last stage before s at which a requirement stronger than N_{e} required attention,

(b) Φ_{e}^{A}(e)[t]↓,
(c) A[t] ↾ φ_{e}^{A}(e)[t] ⊆ U[s], and
(d) A[t] ↾ φ_{e}^{A}(e)[t] ⊈ A[s].

We begin the stage by removing from A all elements not in U[s]. Then, for the strongest requirement X that requires attention at stage s, we act as follows.

If X = P_{e} then let n be the ≺-least element of U[s] larger (in the ℕ sense) than e and the restraints of stronger priority N-requirements and put n in A.

If X = N_{e} then there are two cases. If condition 1 above holds then declare the restraint of N_{e} to be the maximum of its previous value (if any) and φ_{e}^{A}(e)[s]. If condition 2 holds then let t be the least stage satisfying the condition. For every n ∈ A[t] ↾ φ_{e}^{A}(e)[t] such that n is larger (in the ℕ sense) than the restraints of stronger priority N-requirements, put n in A.

This completes the construction. We now verify its correctness.

Assume by induction that all requirements stronger than P_{e} are satisfied and eventually stop requiring attention. Then each such N-requirement has a final restraint. Let r be the maximum of these restraints, and let n be the ≺-least element of U larger (in the ℕ sense) than e and r. There is a stage s after which no requirement stronger than P_{e} requires attention and n does not leave U. If there is a stage t > s such that n ∉ A[t] then n enters A at stage t and never leaves A after that. So P_{e} is satisfied, and hence eventually stops requiring attention.

Now assume by induction that all requirements stronger than N_{e} are satisfied and eventually stop requiring attention. Let s be the least stage after which no such requirement ever requires attention. Note that A is constant up to the maximum of the restraints imposed by these requirements from stage s onward. There are three cases.

First suppose that for some t > s we have Φ_{e}^{A}(e)[t] ↓ and A[t] ↾ φ_{e}^{A}(e)[t] ⊆ U. For the least such t, there is a u such that for all v > u we have A[t] ↾ φ_{e}^{A}(e)[t] ⊆ U[v]. If Φ_{e}^{A}(e)[v]↓ for all v > u then by convention Φ_{e}^{A}(e)↓, and hence N_{e} is satisfied. Otherwise, at the least stage v > u such that Φ_{e}^{A}(e)[v] ↑, the requirement N_{e} will act to put every element of A[t] ↾ φ_{e}^{A}(e)[t] into A if this is not already the case. Furthermore, no such number will ever leave A, and because of the restraint imposed by N_{e}, no number will ever enter A ↾ φ_{e}^{A}(e)[t] after stage t. Thus A ↾ φ_{e}^{A}(e)[t] = A[t] ↾ φ_{e}^{A}(e)[t], which implies that Φ_{e}^{A}(e)↓, and hence that N_{e} is satisfied.

Otherwise, for every t > s such that Φ_{e}^{A}(e)[t]↓, we have A[t] ↾ φ_{e}^{A}(e)[t] ⊄ U. If there are only finitely many such t then N_{e} is vacuously satisfied, and it is easy to check that in this case N_{e} eventually stops requiring attention.

So we are left with the case in which ∃^{∞}t (Φ_{e}^{A}(e)[t] ↓), but for every t > s such that Φ_{e}^{A}(e)[t]↓, we have A[t] ↾ φ_{e}^{A}(e)[t] ⊄ U. In this case we can define a computable infinite descending sequence n_{0} ≻ n_{1} ≻ ⋯ by recursion as follows. Let n_{0} be the last element of ≺. Assuming that we have defined n_{k} so that n_{k} ∉ U, search for a t > s such that Φ_{e}^{A}(e)[t] ↓ and every n ∈ A[t] ↾ φ_{e}^{A}(e)[t] is ≺-less than n_{k}. Such a t must eventually be found, since A[u] ⊆ U[u] for all u. Let n_{k+1} be the ≺-greatest element of A[t] ↾ φ_{e}^{A}(e)[t]. Since A[t] ↾ φ_{e}^{A}(e)[t] ⊄ U, we must have n_{k+1} ∉ U, and thus the recursion can continue. Since n_{0} ≻ n_{1} ≻ ⋯ and the sequence of n_{k}’s is defined recursively, we are done.

Corollary 2.12. There is an ω-model of RCA_{0} + SADS consisting entirely of low sets.

Proof. Iterate and dovetail the construction of Theorem 2.11 to produce a sequence of low sets X_{0}, X_{1}, … so that for each i, every linear order of type ω + ω^{∗} computable in X_{i} has a suborder of type ω or ω^{∗} computable in some X_{j}. The class of all sets computable in X_{i} for some i forms the second order part of an ω-model of RCA_{0} + SADS.

On the other hand, Downey, Hirschfeldt, Lempp and Solomon [2001] have constructed a computable stable coloring of [ℕ]^{2} with no low homogeneous set, and so the model of SADS constructed in Corollary 2.12 cannot be a model of SRT_{2}^{2}.

Corollary 2.13. SADS ⊬ SRT_{2}^{2}.

Carl Jockusch has pointed out a surprising, purely degree theoretic consequence of Theorem 2.11:

Corollary 2.14. (Jockusch): Every c ⩽_{T} 0′ is c.e. in a low degree.

Proof. By Harizanov [1998] there is a C ∈ c and a computable linear order L of type ω+ω^{∗} such that C is the ω part of L and C̄ is the ω^{∗} part. By the Theorem there is a low A which is an infinite ascending (descending) sequence in L. Thus C = {n|(∃a ∈ A)(n ⩽_{L} a)} (C̄ = {n|(∃a ∈ A)(a ⩽_{L} n)}) as required.

We next show that neither SADS nor WKL_{0} implies CADS, as each of them has an ω-model with only low sets while CADS does not.

Proposition 2.15. There is a computable linear order with no low suborder of type ω, ω^{∗}, or ω + ω^{∗}.

Proof. Start with a computable infinite partial order P of ℕ with no chain or antichain computable in 0′, as given by Herrmann [2001]. Extend P to a computable linear order L, i.e. x ⩽_{P} y → x ⩽_{L} y. (That there is such an L is cited as a folklore version of the classical theorem of Szpilrajn [1930] and proven in Downey [1998, Observation 6.1].) We claim L is the desired linear order. Suppose not. Then, by Theorem 2.11, L has a low ascending or descending sequence K = {k_{i} | i ∈ ℕ}. Suppose that K is ascending; the other case is symmetric. We construct a chain or antichain in P computably in K′ = 0′ for the required contradiction. For each i < j, either k_{i} <_{P} k_{j} or k_{i} |_{P} k_{j}. Computably in K′ build a series of subsequences l_{i,n} as follows. Let l_{0,0} = k_{0}. Given l_{i,n}, let l_{i,n+1} be k_{j} for the least j such that l_{i,n} <_{P} k_{j} if there is such a j; otherwise terminate the i^{th} subsequence with k_{n_{i}} = l_{i,n} and begin the (i + 1)^{st} with l_{i+1,0} = k_{n_{i}+1}. Note that if k_{n_{i}} is defined then k_{n_{i}} ≮_{P} k_{j} for any j > n_{i} and so all the k_{n_{i}} are incomparable in P. Thus, if one of the subsequences l_{i,n} is infinite it is the desired chain in P, and if not, then the k_{n_{i}} form the desired antichain in P.

Corollary 2.16. SADS ⊬ CADS; WKL_{0} ⊬ CADS.

We next show that WKL_{0} does not imply SADS, by proving two technical computability theoretic theorems involving the following ad-hoc notion. We write X ⩽_{T}^{b} Y ⊕ Z if there is a functional Φ and a computable function f such that Φ^{Y ⊕Z} = X and for each n the computation of Φ^{Y ⊕Z}(n) queries at most the first f(n) many bits of Y.

Theorem 2.17. Let A and B be c.e. sets. There is a computable linear order of type ω + ω^{∗} with the following property: For any ascending or descending suborder C, either B ⩽_{T}^{b} A ⊕ C or A ⩽_{T}^{b} B ⊕ C.

Proof. Let A and B be infinite, coinfinite c.e. sets. We make it a convention that at each stage s at most one element k enters at most one of A or B, and k ⩽ s.

We build a computable linear order ≺ while simultaneously defining Δ_{2}^{0} sets U and D. The idea is that ≺ will have order type ω + ω^{∗}, with U being the elements in the ω part and D those in the ω^{∗} part. We will also have movable markers M_{i} and N_{i} for i ∈ ω. The positions of M_{i} and N_{i} at stage s of the construction will be denoted by m_{i}^{s} and n_{i}^{s}, respectively, and the limits m_{i} = lim_{s} m_{i}^{s} and n_{i} = lim_{s} n_{i}^{s} will exist. Furthermore, m_{i} will be computable from B ↾ i + 1 and A ↾ i, and n_{i} will be computable from A ↾ i + 1 and B ↾ i. Let s be the least stage such that B ↾ i + 1 and A ↾ i have settled. Then we will have i ∈ A if and only if either i ∈ A[s] or m_{i} ∈ D. Similarly, letting s be the least stage such that A ↾ i + 1 and B ↾ i have settled, we will have i ∈ B if and only if either i ∈ B[s] or n_{i} ∈ U. As we will argue below, these facts will be enough to establish the theorem.

At stage s, we proceed as follows. First we provide the needed positions for markers:

1. Let j_{0} < ⋯ < j_{n} be all numbers j ⩽ s such that M_{j} does not currently have a position. Let c_{0}, …, c_{n} be fresh large numbers. Declare l ≺ c_{0} ≺ ⋯ ≺ c_{n} for all l currently in U, put each c_{i} in U, and give each M_{j_{i}} the position m_{j_{i}}^{s} = c_{i}.

2. Let j_{0} < ⋯ < j_{n} be all numbers j ⩽ s such that N_{j} does not currently have a position. Let c_{0}, …, c_{n} be fresh large numbers. Declare c_{n} ≺ ⋯ ≺ c_{0} ≺ r for all r currently in D, put each c_{i} in D, and give each N_{j_{i}} the position n_{j_{i}}^{s} = c_{i}.

If a number k (by convention unique) enters A or B (again, necessarily only one of them) at this stage, then we act to reflect this enumeration. (If not, we proceed to the next stage.)

1. If k enters A then for each l ∈ U that is equal to, or to the right of, m_{k}^{s}, put l in D. Cancel the position of all markers N_{i} with i ⩾ k and all markers M_{i} with i > k.

2. If k enters B then for each r ∈ D that is equal to, or to the left of, n_{k}^{s}, put r in U. Cancel the position of all markers M_{i} with i ⩾ k and all markers N_{i} with i > k.

This completes the construction. Clearly ≺ is a computable linear order. We now verify that it has the desired properties.

An element x of U[s] can move to D at a stage t > s only if it is equal to, or to the right of, m_{k}^{t} for k entering A at stage t. If this happens then x will henceforth be to the right of every marker N_{i} with i ⩾ k, so it will return to U at a stage u > t only if an element k′ < k enters B. Repeating this argument, we see that x will once again move to D only if an element k′′ < k′ enters A, and so forth. So x can shift between U and D only finitely often. Thus U and D are Δ_{2}^{0}, and the domain of ≺ is U ∪ D.

Let j ∉ A and k ∉ B, and let l = max(j, k). If s is a stage such that A ↾ l + 1 and B ↾ l+1 have settled then m_{j}^{s} is permanently in U and n_{k}^{s} is permanently in D. So U and D are infinite, and hence, by the way elements are put into the order, (U, ≺) and (D, ≺) have order types ω and ω^{∗}, respectively, and every element of U is ≺ every element of D. So ≺ has order type ω + ω^{∗}.

Let s be the least stage such that A ↾ j + 1 = A[s] ↾ j + 1 and B ↾ j = B[s] ↾ j. Then N_{j} is never moved from its position n_{j}^{s} at a later stage, so n_{j} = lim_{t} n_{j}^{t} exists and is computable from A ↾ j + 1 and B ↾ j. If j enters B after stage s then n_{j} is put into U, and it cannot be moved to D, since that would require either that a number less than or equal to j enter A or that a number less than j enter B. On the other hand, if j ∉ B then n_{j} is initially put into D, and cannot be moved to U, since that would require a number less than or equal to j to enter either A or B. Thus we have j ∈ B if and only if either j ∈ B[s] or n_{j} ∈ U (or both).

Similarly, let s be the least stage such that B ↾ j+1 = B[s] ↾ j+1 and A ↾ j = A[s] ↾ j. The same argument as in the previous paragraph shows that m_{j} = lim_{t} m_{j}^{t} exists and is computable from B ↾ j + 1 and A ↾ j, and j ∈ A if and only if either j ∈ A[s] or m_{j} ∈ D (or both).

Now let C be a descending suborder of ≺ (the ascending case being symmetric). We show that B ⩽_{T}^{b} A ⊕ C by induction. Suppose that we have already computed B ↾ j using A ↾ j and C. To compute B(j) using A ↾ j + 1 and C, find the least stage s such that A ↾ j + 1 = A[s] ↾ j + 1 and B ↾ j = B[s] ↾ j. If j ∈ B[s] then we are done. Otherwise, we can use A ↾ j + 1 and B ↾ j to compute n_{j}, and we know that j ∈ B if and only if n_{j} ∈ U. But x ∈ D if and only if x is to the right of some element of C, so D is c.e. in C. Thus, to compute B(j), we simultaneously enumerate B and D. Either j enters B or n_{j} enters D, in which case j ∉ B.

Theorem 2.18. Given any low set X there are c.e. sets A_{0} and A_{1} such that A_{0} ⩽̸_{T}^{b} A_{1} ⊕ X and A_{1} ⩽̸_{T}^{b} A_{0} ⊕ X.

Proof. We have requirements

R_{e,i,k} : Φ_{e}^{A_{k}⊕X} total ∧ Φ_{i} total ∧ ∀n (the computation Φ_{e}^{A_{k}⊕X}(n) queries at most the first Φ_{i}(n) many bits of A_{k}) → ∃n (Φ_{e}^{A_{k}⊕X}(n) ≠ A_{1−k}(n)),

arranged in a priority order in the usual way.

To each R_{e,i,k} we associate a number n_{e,i,k} ∈ ℕ^{[⟨e,i,k⟩]}, a set N_{e,i,k} (containing values of n_{e,i,k}) and a c.e. set of binary strings W_{e,i,k}, into which we enumerate strings during the construction. Each time R_{e,i,k} is initialized, a fresh new value is picked for n_{e,i,k}, the set N_{e,i,k} is redefined to be {n_{e,i,k}}, and W_{e,i,k} is redefined to be a new, currently empty, set. By the Recursion Theorem and the lowness of X, there is a computable approximation w_{e,i,k}(t) (which is uniformly computable over all requirements) such that if R_{e,i,k} is initialized only finitely often then lim_{t} w_{e,i,k}(t) = w_{e,i,k} exists, and w_{e,i,k} = 1 if and only if, for the final version of W_{e,i,k}, there is a σ ∈ W_{e,i,k} such that σ is an initial segment of X.

At stage 0, set the restraint imposed by each requirement to 0, pick values for the n_{e,i,k}, and let each N_{e,i,k} = {n_{e,i,k}}.

At stage s > 0, proceed as follows. For each R_{e,i,k}, let r_{e,i,k}[s] be the maximum of the union of all sets {Φ_{i′}(n)[s] | n ∈ N_{e′,i′,k′}} taken over all R_{e′,i′,k′} stronger than R_{e,i,k}. If min(N_{e,i,k}) < r_{e,i,k}[s] then initialize R_{e,i,k}.

Say that R_{e,i,k} requires attention at stage s if w_{e,i,k}(s) = 0 and for all n ∈ N_{e,i,k}, it is the case that Φ_{i}(n)[s] ↓, that Φ_{e}^{A_{k}⊕X}(n)[s] ↓= A_{1−k}(n)[s], and that the computation Φ_{e}^{A_{k}⊕X}(n)[s] queries at most Φ_{i}(n) many bits of A_{k}.

For each R_{e,i,k} requiring attention (if any), proceed as follows. Enumerate X ↾ φ_{e}^{A_{k}⊕X}(n_{e,i,k})[s] into W_{e,i,k} and wait until either w_{e,i,k}(t) = 1 for some t > s or X changes below φ_{e}^{A_{k}⊕X}(n_{e,i,k})[s]. One of these must happen by the choice of w_{e,i,k}. In the first case, enumerate n_{e,i,k} into A_{1−k}, choose a fresh new value for n_{e,i,k}, and enumerate this value into N_{e,i,k}. This completes the construction. We now verify its correctness.

Assume by induction that for all strategies R_{e′,i′,k′} stronger than R_{e,i,k}, the value of n_{e′,i′,k′} eventually settles, so that lim_{s} r_{e,i,k}[s] exists and hence R_{e,i,k} eventually stops being initialized, say by stage u, which implies that N_{e,i,k} and W_{e,i,k} have final versions. Every time n_{e,i,k} gets redefined at a stage s > u we must have w_{e,i,k}(s) = 0 and w_{e,i,k}(t) = 1 for some t > s. Since w_{e,i,k} = lim_{s} w_{e,i,k}(s) exists, this means that n_{e,i,k} eventually settles to a final value.

Now suppose that Φ_{e}^{A_{k}⊕X} and Φ_{i} are total and for all n, the computation Φ_{e}^{A_{k}⊕X}(n) queries at most Φ_{i}(n) many bits of A_{k}. Then Φ_{i}(n_{e,i,k})↓ and Φ_{e}^{A_{k}⊕X}(n)↓ for all n ∈ N_{e,i,k}. We claim Φ_{e}^{A_{k}⊕X}(n)↓≠ A_{1−k}(n) for some n ∈ N_{e,i,k}.

First suppose that w_{e,i,k} = 0. Then there is a stage u after which w_{e,i,k} has settled and R_{e,i,k} always requires attention. But then at each stage s > u we see X change below φ_{e}^{A_{k}⊕X}(n_{e,i,k})[s] (since otherwise we would have t > s with w_{e,i,k}(t) = 1). This contradicts the totality of Φ_{e}^{A_{k}⊕X}.

Now suppose w_{e,i,k} = 1. Then there is a σ ∈ W_{e,i,k} such that σ is an initial segment of X. But by the definition of W_{e,i,k}, at the stage s at which σ enters W_{e,i,k}, we have Φ_{e}^{A_{k}⊕σ}(n)[s] ↓= 0, where n is the value of n_{e,i,k} at that stage, and we put n into A_{1−k}. Furthermore, the computation Φ_{e}^{A_{k}⊕σ}(n)[s] queries at most Φ_{i}(n) many bits of A_{k}, and A_{k} ↾ Φ_{i}(n) never changes after stage s, so in fact Φ_{e}^{A_{k}⊕σ}(n) ↓= 0, whence Φ_{e}^{A_{k}⊕X}(n) ↓= 0 ≠ A_{1−k}(n).

Corollary 2.19. WKL_{0} ⊬ SADS.

Proof. By Theorems 2.17 and 2.18, no low set can bound (in Turing degree) the sets of an ω-model of SADS. As there are low sets that bound the sets of an ω-model of WKL_{0} (see Simpson [1999, proof of Theorem VIII.2.17]), WKL_{0} does not imply SADS.

We remark that Theorem 2.18 cannot be extended by replacing our ad-hoc reducibility ⩽_{T}^{b} with Turing reducibility. This is because Downey (see Arslanov, Cooper, and Li [2004]) has shown that there is a low degree that cups all nonzero c.e. degrees to 0′.

Another consequence of Theorems 2.17 and 2.18 is that there is no universal instance of SADS. That is, there is no computable linear order L of type ω+ω^{∗} such that for every infinite ascending or descending suborder C of L and every computable linear order L′ of type ω + ω^{∗}, there is an infinite ascending or descending suborder of L′ computable in C.

The next series of results will all be of the form that one can add a solution for an arbitrary instance of one problem by forcing without adding a solution to an instance of another problem that does not have one in the original model. These types of results give various nonimplications among the relevant systems even for ω-models. When it is possible to implement them over arbitrary models, they yield conservation results as well. The basic situation here is that we start with a countable model M of RCA_{0} and a notion of forcing P defined over M. Moreover, if G is sufficiently generic over P (usually 1-generic plus satisfying a specific list of requirements that guarantee that if we force an instance of a Σ_{1}^{0} (or Π_{1}^{0}) formula then there is a least instance that can be forced and we do so), we can show that IΣ_{1} holds for formulas over M with G as an added set parameter. (This typically relies on a sufficiently simple definition of forcing for one quantifier sentences.) In this situation, M is an ω-submodel of the model M[G] gotten by adding on to the sets of M all sets definable over M by Δ_{1}^{0} formulas with G as an added set parameter, and M[G] is itself a model of RCA_{0} (Friedman [1976], or see Simpson [1999] or CJS §6). (Warning: in CJS, M[G] is first officially defined as the model of IΣ_{1} gotten by adding on just G to the sets of M. What we generally want, however, is its extension to a model of RCA_{0}.)

We begin with COH and Mathias forcing as in CJS §9; see CJS for more on Mathias forcing (including the formal definition of the forcing relation). Conditions are pairs (D, L) where D is M-finite, L is M-infinite and max D < min L. We say that (D′, L′) extends (D, L), and write (D′, L′) ⩽ (D, L), if D ⊆ D′ ⊆ D ∪ L and L′ ⊆ L. CJS show that if G is Mathias 1-generic (i.e. every Π_{1}^{0} formula or its negation is forced and the conditions specific to forcing IΣ_{1} are met) then adding G to M preserves IΣ_{1} and so M[G] ⊨ RCA_{0} and every sequence ⟨A_{i}⟩ coded by an A ∈ M has a cohesive set in M[G]. They note that, by iteration, this proves that COH is Π_{1}^{1}-conservative over RCA_{0}. We strengthen their results to a stronger conservation result that shows that none of the principles that we have discussed follow from COH, except those already shown to follow from it.^{1}

Theorem 2.20. Let M be a countable model of RCA_{0} and let Φ(A, B) be a Σ_{3}^{0} predicate of two set variables such that for some fixed A ∈ M there is no B ∈ M with M ⊨ Φ(A, B). If G is Mathias 2-generic over M then there is no B ∈ M[G] with M[G] ⊨ Φ(A, B).

Proof. Suppose that Φ(A, B) = ∃x ∀y ∃z φ(A, B, x, y, z) where φ is Δ_{0}^{0} and, for the sake of a contradiction, that there is a B ∈ M[G] such that M[G] ⊨ Φ(A, B). Now M is an ω-submodel of M[G], and B is of the form Φ_{e}^{G⊕C} for some Turing functional Φ_{e} and set C in M, so for some x ∈ M,

M[G] ⊨ Φ_{e}^{G⊕C} is a total characteristic function and ∀y ∃z φ(A, Φ_{e}^{G⊕C}, x, y, z).

As this whole formula is equivalent (even in RCA_{0}) to a Π_{2}^{0}(G) (over M) formula ∀y ∃z Ψ(G, C, A, x, y, z) and G is 2-generic, there is a condition (D, L) ∈ M such that (D, L) ⊩ ∀y ∃z Ψ(G, C, A, x, y, z).

By the general definition of forcing this means that for every y in M and every condition (D′, L′) ⩽ (D, L), there is a z ∈ M and a condition (D′′, L′′) ⩽ (D′, L′) such that (D′′, L′′) ⊩ Ψ(G, C, A, x, y, z). By the definition of Mathias forcing for Δ_{0}^{0}-formulas, however, this last assertion depends on only a finite part of the forcing condition. More precisely, it depends on certain numbers being in D′′ and certain numbers being out of L′′. Thus, for every y ∈ M and every D′ ⊇ D with D′ − D ⊆ L, there is a finite set F_{y}(D′) ⊇ D′ of M and a number z ∈ M such that F_{y}(D′) − D′ ⊆ L and M ⊨ Ψ(F_{y}(D′), C, A, x, y, z). We can now define by recursion the function f such that f(0) = D and f(n + 1) = F_{n}(f(n)). As M is a model of RCA_{0}, this function is an element of M and so gives the characteristic function of a set H ∈ M which by construction satisfies ∀y ∃z Ψ(H, C, A, x, y, z). Finally, if B′ = Φ_{e}^{H⊕C} then B′ ∈ M and M ⊨ ∀y ∃z φ(A, B′, x, y, z) for the desired contradiction.

We now have our conservation and nonimplication results. In the terminology of Simpson [1999, Definition VII.2.28], a model M is a restricted β-submodel of a model M′ if M is an ω-submodel of M′ and for every sentence of the form ∃X ψ where ψ is Π_{2}^{0} with parameters in M, we have M ⊨ ∃X ψ if and only if M′ ⊨ ∃X ψ. (This condition says that a subtree of ω^{<ω} in M has a path in M if and only if it has a path in M′, whence the terminology.)

Corollary 2.21. COH is conservative over RCA_{0} for sentences of the form ∀A (Θ(A) → ∃B Φ(A, B)) where Θ is arithmetic and Φ is Σ_{3}^{0}. Furthermore, every model of RCA_{0} is a restricted β-submodel of a model of COH.

1In the aforementioned upcoming joint paper with Slaman, we prove the analogous theorem about Cohen forcing and so conservation and nonimplication results for the principle AMT which says that every atomic theory has an atomic model.

Proof. Consider any sentence of the specified form and any model M of RCA_{0} not satisfying the sentence. Thus there is a set A of M such that M ⊨ Θ(A) for which there is no B in M such that M ⊨ Φ(A, B). Construct a sequence ⟨G_{i} | i ∈ ω⟩ of subsets of ℕ^{M} such that G_{i+1} is Mathias 2-generic over M[G_{1}] … [G_{i}]. Let M′ = ⋃{M[G_{0}] … [G_{i}] | i ∈ ω}. By the results of CJS mentioned above, M[G_{0}] … [G_{i}] ⊨ RCA_{0} for each i, and every sequence R⃗ in M[G_{0}] … [G_{i}] has a cohesive set in M[G_{0}] … [G_{i}][G_{i+1}]. Thus M′ ⊨ RCA_{0} + COH as the first order part of every element of this ascending sequence of models is the same. By induction (on ω) our theorem shows that there is no B ∈ M[G_{0}] … [G_{i}] such that M[G_{0}] … [G_{i}] ⊨ Φ(A, B). Again, as each successive model in this list is an ωextension of the preceding one and M′ is just their union, we see that while M′ ⊨ Θ(A), there is no B ∈ M′ such that M′ ⊨ Φ(A, B). Thus our original sentence is not a theorem of RCA_{0} + COH, as required.

The version of the corollary in terms of restricted β-extensions follows by taking Θ to be empty and Φ to be Π_{2}^{0}. Our argument shows that if M′ ⊨ ∃B Φ then M ⊨ ∃B Φ. The other direction follows from the fact that M is an ω-submodel of M′.

We note that this result also literally extends the one of CJS for Π_{1}^{1} sentences by taking Φ to be any vacuously true sentence. Moreover, the result is the best possible one of this form as COH itself is a sentence of the form ∀A (Θ(A) → ∃B Φ(A, B)) with Θ arithmetic and Φ a Π_{3}^{0} formula. It is, however, strong enough to show that any principle that asserts, for example, the existence of an infinite set satisfying some computable condition such as being homogeneous, a path through a tree, or a chain or antichain in a linear or partial order cannot be implied by COH, as all of these statements are ones in which Φ is Π_{2}^{0}.

Corollary 2.22. None of the following principles are implied by COH (nor CADS, which follows from it): RT_{2}^{2}, SRT_{2}^{2}, WKL_{0}, DNR, CAC, ADS, SADS.

Of course, as discussed above, this result was already known for RT_{2}^{2}, SRT_{2}^{2}, and WKL_{0}. For DNR, it has also been proved by Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta].

By Corollary 2.16 we now have the desired independence for our splittings of ADS.

Corollary 2.23. CADS and SADS are incomparable over RCA_{0} and both are strictly weaker than ADS.

We now investigate the relationships with WKL_{0} by first showing that adding it to COH does not yield any of the other principles mentioned in Corollary 2.22, except for DNR, of course. It suffices to prove this for SADS as it is implied by all the principles other than WKL_{0} and DNR on this list. We then show that ADS does not imply WKL_{0} or even DNR. CAC is considered in the next section.

Proposition 2.24. For any set X, if L is a linear order computable in X with no ascending or descending sequence computable in X and T is an infinite binary tree computable in X, then there is a path f in T such that no ascending or descending sequence in L is computable in f ⊕ X.

Proof. We consider the case that X is computable. The full proposition then holds by relativization. We use forcing (in standard arithmetic) with infinite computable subtrees S of T. Of course, any 1-generic G gives us a path P = P_{G} through T as the union of the roots of the trees S ∈ G. Suppose G is 2-generic and Φ_{e}^{P} is total and an ascending sequence in L. (The case of a descending sequence is symmetric.) Thus we have a tree S ⊆ T with P ∈ [S] such that S ⊩ (Φ_{e}^{P} is total and (∀m)(∀n < m)(Φ_{e}^{P} (n) <_{L} Φ_{e}^{P} (m))).

As S ⊩ (Φ_{e}^{P} is total), for each n there is an s such that Φ_{e}^{σ} ↾ n is defined for every σ on level s of S. (Otherwise, {τ ∈ S | (∃i < n) Φ_{e}^{τ}(i)↑} is infinite and, in fact, a subtree of S that forces Φ_{e}^{P} not to be defined on some i < n, contrary to our choice of S.) Consider now the computable subtree Ŝ of S consisting of all σ such that (∀i < |σ|)(Φ_{e}^{σ}(i) ↓ ∧ Φ_{e}^{σ}(i + 1)↓ → Φ_{e}^{σ}(i) <_{L} Φ_{e}^{σ}(i + 1)). If this Ŝ were not infinite, then the subtree S̃ of S consisting of the downward closure of the nodes where this condition fails would be an infinite computable subtree of S that forces Φ_{e}^{P} not to be an ascending sequence in L, contrary to our assumption on S.

We now define an ascending sequence ⟨a_{i} | i ∈ ω⟩ in L computably in Ŝ for our contradiction. To find a_{i} find the least s_{i} such that Φ_{e}^{σ} ↾ (i + 1)↓ for every σ on level s_{i} of Ŝ. Let a_{i} be the L-least member of {Φ_{e}^{σ}(i) | σ ∈ Ŝ ∧ |σ| = s_{i}}. (All of these values must be in the domain of L by our definition of Ŝ.) We claim that ⟨a_{i}⟩ is ascending in L, i.e. a_{i} <_{L} a_{i+1} for every i. Consider any a_{i} and a_{i+1}. They were chosen L-least from among the values of Φ_{e}^{σ}(i) and Φ_{e}^{τ}(i + 1) for σ on level s_{i} and τ on level s_{i+1} of Ŝ. Say a_{i+1} = Φ_{e}^{τ}(i + 1) for some τ on level s_{i+1}. There must be a σ on level s_{i} such that σ ⊆ τ. By our definition of Ŝ and choice of s_{i}, we have Φ_{e}^{σ}(i) ↓= Φ_{e}^{τ}(i) <_{L} Φ_{e}^{τ}(i + 1). On the other hand, our definition of a_{i} makes a_{i} ⩽_{L} Φ_{e}^{σ}(i) <_{L} Φ_{e}^{τ}(i + 1) = a_{i+1} as required.

Corollary 2.25. COH + WKL_{0} ⊬ SADS.

Proof. Start with the standard model COMP with second order part consisting of all computable sets, and a computable linear order L of type ω + ω^{∗} with no computable ascending or descending sequence. Iterate and dovetail the forcing constructions of Theorem 2.20 and Proposition 2.24 to produce an ω-model of COH and WKL_{0} in which L still has no ascending or descending sequence.

We next work at showing that ADS does not imply WKL_{0}, or even DNR. We begin with SADS.

Proposition 2.26. Let L be a linear order of type ω+ω^{∗} computable in a set X such that there is no diagonally noncomputable function computable in X. There is then a subset G of L of order type ω or ω^{∗} with no diagonally noncomputable function computable in G ⊕ X.

Proof. We again treat the case that X is computable and note that the general case holds by relativization. If there is a computable subset G of L of order type ω^{∗} we are done, so suppose not. Let U be the subset of L consisting of all elements in the ω part of L, i.e. all elements with only finitely many predecessors in L.

We consider the notion of forcing F in which conditions are finite sequences σ ∈ ω^{<ω} that are strictly ascending in both natural order (<_{ℕ}) and the order of L (<_{L}), with all elements in U (or equivalently with last element in U). Extension is as usual for finite sequences: σ extends τ if τ ⊇ σ. Let G be 2-generic for this forcing. Then G is obviously an ascending sequence in L. We claim that no Φ_{e}^{G} is a diagonally noncomputable function. If one were then there would be a condition σ ⊩ (Φ_{e}^{G} is total ∧ ∀k (Φ_{k}(k) ↓→ Φ_{e}^{G}(k) ≠ Φ_{k}(k))). Fix such a σ to argue for a contradiction.

For each k let τ(k) be the first string ρ found in a computable search through ω^{<ω} that is increasing in both <_{ℕ} and <_{L} such that ρ ⊇ σ and Φ_{e}^{ρ}(k) ↓. We do not assume here that ρ(|ρ|) ∈ U and so τ is a partial computable function. In fact, τ is total as σ ⊩ (Φ_{e}^{G} is total) and so for any k there is actually a ρ ⊇ σ in F such that Φ_{e}^{ρ}(k) ↓. If there are infinitely many k such that Φ_{k}(k) ↓ and Φ_{e}^{τ(k)}(k) = Φ_{k}(k) then we can computably find infinitely many such k. If for such k, τ(k) ∈ F then τ(k) extends σ and τ(k) ⊩ Φ_{e}^{G}(k) ↓= Φ_{k}(k) ↓, contradicting our choice of σ. By standard conventions |τ(k)| ⩾ k. Thus for each of these k we have effectively produced an element, τ(k)(|τ(k)|) of Ū (the ω^{∗} part of L) larger (in natural order) than k. Thus we can produce an infinite computable subset of Ū. We can then computably thin out this set to require that the elements be descending in ⩽_{L} and ascending in ⩽_{ℕ}, as for each a_{i} there are only finitely many a_{j} that are above it in ⩽_{L}, since a_{i} is in the ω^{∗} part of L. This contradicts our assumption that there is no computable descending sequence in L. Thus there are only finitely many k such that Φ_{k}(k) ↓ and Φ_{e}^{τ(k)}(k) = Φ_{k}(k) and so a finite variation of the computable function taking k to Φ_{e}^{τ(k)}(k) would be DNR for the desired contradiction.

Corollary 2.27. SADS ⊬ DNR.

Proof. By the usual iteration and dovetail argument we can use Proposition 2.26 to build an ω-model of SADS in which there is no diagonally noncomputable function and so DNR fails.

Corollary 2.28. ADS ⊬ DNR.

Proof. We can combine the forcing of Proposition 2.26 with that of Theorem 2.20 to get an ω-model in which both SADS and COH hold but in which there is no diagonally noncomputable function and so DNR fails. By Propositions 2.7 and 2.9 this model is also one of ADS.

Corollary 2.29. ADS ⊬ SRT_{2}^{2} and so ADS ⊬ RT_{2}^{2}.

Proof. Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta] show that SRT_{2}^{2} ⊢ DNR and so neither SRT_{2}^{2} nor RT_{2}^{2} can be a consequence of ADS.

It is interesting to note that we can use the forcing notion of Proposition 2.26 to provide an alternate proof of Theorem 2.11. We provide a stronger version in Theorem 3.4 as part of our analysis of CAC.

We have now shown that ADS does not imply WKL_{0}, or even DNR, and also does not imply RT_{2}^{2}, or even SRT_{2}^{2}. We have also shown that it splits into two incomparable principles, SADS (implied by SRT_{2}^{2} but with low solutions) and CADS (implied by COH and almost equivalent to it as will be shown in Theorem 4.4). Moreover, neither of these principles is implied by WKL_{0}. The results of this section are summarized and depicted in the diagram below, which uses the same notation as the diagram in the previous section. We proceed to do a similar analysis for CAC in the next section.

[figure: RT_{2}^{2}; (1,2); _{SRT2 2}; (3); (1); DNR; ADS; |; (2); (4); (5); _{WKL_{0}}; |; (9); COH + WKL_{0}; |; (6); SADS; (7); COH; (8); CADS; (7); _{RCA_{0}}]

Diagram 2

The references for these results are as follows: (1) Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta]; (2) Corollary 2.28; (3) Proposition 2.8 and Corollary 2.13;

(4) Proposition 2.7 and Corollary 2.16; (5) Proposition 2.10 and Corollary 2.22; (6) Corollaries 2.19 and 2.25; (7) Corollary 2.6; (8) Proposition 2.9; (9) Corollary 2.16.

3 Partial Orders and CAC

In this section we will analyze CAC. We begin with a connection to ADS.

Proposition 3.1. RCA_{0} + CAC ⊢ ADS.

Proof. Let L be a linear order on ℕ. We define a partial order P on ℕ by setting m ⩽_{P} n if and only if m ⩽_{L} n ∧ m ⩽_{ℕ} n. If C is a chain in P and we list it in increasing natural order, then it is an ascending sequence in L, as if x <_{ℕ} y the only way x and y can be comparable in P is if x <_{L} y. On the other hand, if A is an antichain in P and we list it in increasing natural order, then it is a descending sequence in L, as if x <_{ℕ} y and x <_{L} y then x <_{P} y.

We next define the appropriate notion of stability for CAC.

Definition 3.2. A partial order P is stable if either

(1) (∀i ∈ P)(∃s)[(∀j > s)(j ∈ P → i <_{P} j) ∨ (∀j > s)(j ∈ P → i |_{P} j)]

or

(2) (∀i ∈ P)(∃s)[(∀j > s)(j ∈ P → i >_{P} j) ∨ (∀j > s)(j ∈ P → i |_{P} j)].

Now for the associated principle and system:

(SCAC) Stable CAC: Every infinite stable partial order has an infinite chain or antichain.

While this might not be one’s first guess at the right notion of stability for a partial order, our analysis (especially Proposition 5.4) will bear out the analogy with the previous notions of stability. We begin with a couple of easy combinatorial facts that place SCAC between SRT_{2}^{2} and SADS.

Proposition 3.3. RCA_{0} ⊢ SRT_{2}^{2} → SCAC → SADS.

Proof. For the first implication, let P be a stable partial order with domain ℕ. Define a coloring f by f(x, y) = 0 if x and y are comparable in P and f(x, y) = 1 if x |_{P} y. By the definition of stability for a partial order, f is a stable coloring. If H is homogeneous to 0 then it is a chain in P and if H is homogeneous to 1 then it is an antichain in P.

For the second, given a linear order L on ℕ of type ω + ω^{∗} we define a partial order P on ℕ as in Proposition 3.1. Consider any m. If m is in the ω part of L, then almost every n is larger than m in both the natural order and that of L, and so above it in P. If m is in the ω^{∗} part of L, then almost every n is above it in the natural order but below it in the order of L. Thus almost every n is incomparable with m in P. So P is a stable partial order. As shown in Proposition 3.1, a chain in P is an ascending sequence in L and an antichain in P is a descending sequence in L.

We next show that SCAC has low solutions and does not imply DNR, as we did for SADS in Theorem 2.11, Proposition 2.26, and Corollary 2.27, but now entirely by forcing arguments.

Theorem 3.4. Every stable partial order P computable in X has a chain or antichain S that is low over X, i.e. (S ⊕ X)′ ⩽_{T} X′.

Proof. As usual, we assume that X is computable and that the domain of P is ℕ. We also assume that P satisfies (1) in the definition of a stable partial order. (The argument if P satisfies (2) is symmetric.) If P has a computable antichain, we are done, so we assume not and construct a low chain in P. Let U = {i | (∃s)(∀j > s)(i <_{P} j)}. Note that by the definition of stability U and its complement are both Σ_{2}^{0} and so computable in 0′. We use the same notion of forcing F as in Proposition 2.26 with P replacing L. Thus conditions are sequences σ ∈ ω^{<ω} that are ascending in both natural order and in <_{P} and all of whose elements are in U (or equivalently, whose last elements are in U). Extension is defined as usual.

We construct the low generic G as the union of a sequence ⟨σ_{i}⟩ in F computable in 0′. For each i, let C_{i} be the set of ρ ∈ ω^{<ω} such that ρ is strictly ascending in both ⩽_{ℕ} and ⩽_{P}, and Φ_{i}^{ρ}(i) ↓. We want to define the σ_{i} so that for every i either Φ_{i}^{σ_{i}}(i) ↓ (and so i ∈ G′) or there is no ρ ⊇ σ_{i} in C_{i} (and so σ_{i} ⊩ Φ_{i}^{G}(i) ↑ and i ∉ G′). Given σ_{i} we can clearly search computably in 0′ for a τ ⊃ σ_{i} in F with the properties desired for σ_{i+1}. Assume for a contradiction that there is no such τ. Then there are infinitely many ρ ⊇ σ_{i} in C_{i+1} (as there are infinitely many τ ⊃ σ in F and for each such τ there is a ρ ⊇ τ in C_{i+1}). For each such ρ, we have ρ(|ρ|) ∈ \overline{U} as otherwise ρ would be a witness for convergence in F, and hence could be taken as σ_{i+1}. As the required property for ρ is computable, we can computably enumerate an infinite increasing (in <_{ℕ}) sequence ⟨b_{i}⟩ with all b_{i} ∈ \overline{U} = \{i | (∃s)(∀j > s)(i |_{P} j)\}. We can now computably thin out this sequence to get a computable antichain in P, contrary to our original assumption. More precisely, we define the subsequence ⟨b_{i_{j}}⟩ constituting the antichain by induction so that b_{i_{j+1}} is the first b_{i} with i > i_{j} and b_{i} |_{P} b_{i_{k}} for all k ⩽ j. Such an i exists since each b_{i_{k}} is comparable with only finitely many elements of P.

Note that a similar argument for linear orders of type ω +ω^{∗} in which U is taken to be the ω part provides low solutions for SADS and so an alternate proof of Theorem 2.11. As for SADS, the existence of low solutions for SCAC establishes various nonimplications.

Corollary 3.5. There is an ω-model of SCAC consisting entirely of low sets.

Proof. Iterate and dovetail as usual.

Corollary 3.6. SCAC ⊬ SRT_{2}^{2}; SCAC ⊬ CADS and so SCAC ⊬ COH; SCAC ⊬ ADS.

Proof. Neither SRT_{2}^{2} nor CADS have ω-models consisting of low sets by Downey, Hirschfeldt, Lempp and Solomon [2001] and Proposition 2.15, respectively. The second pair of nonimplications then follows by Propositions 2.9 and 2.10.

We now turn to the question of what is needed on the side of the cohesiveness principle to join SCAC up to CAC. An obvious first choice is the following:

(CCAC) Cohesive CAC: Every partial order has a stable suborder.

This principle, however, is equivalent to ADS.

Proposition 3.7. RCA_{0} ⊢ CCAC ↔ ADS.

Proof. If L is a linear order and we view it as a partial order then by definition any stable suborder is of type ω or ω^{∗} (depending on whether it satisfies (1) or (2) in the definition of stability). For the other direction assume ADS and consider a partial order P. Let L be a linearization of P (as mentioned in the proof of Proposition 2.15, L can be obtained computably, and it is easy to see that the proof of its existence works in RCA_{0}). Now apply ADS to get an ascending or descending sequence S = ⟨s_{i}⟩ in L. Assume that S is ascending in L. Thus (∀i)(∀j > i)(s_{i} <_{P} s_{j} ∨ s_{i} |_{P} s_{j}). Now apply COH (which follows from ADS by Proposition 2.10) to S and the sequence ⟨R_{i}⟩ where R_{i} = {s_{j} | s_{i} <_{P} s_{j}}. Any R⃗-cohesive subset of S with the order of P is a suborder satisfying (1) in the definition of stability. If S is a descending sequence in L then a similar argument provides a suborder satisfying (2) in the definition of stability.

Thus we drop the notation CCAC. We can now use our previous results to split CAC into SCAC and various other principles. The strongest version is the splitting into SCAC and CADS, but COH itself works as well.

Proposition 3.8. RCA_{0} ⊢ CAC ↔ SCAC + ADS ↔ SCAC + COH ↔ SCAC + CADS.

Proof. CAC trivially implies SCAC. It implies ADS by Proposition 3.1. ADS implies COH by Proposition 2.10 and COH implies CADS by Proposition 2.9. SCAC implies SADS by Proposition 3.3 and this plus CADS implies ADS by Propositions 2.7. Finally, SCAC plus ADS implies CAC by Proposition 3.7.

Our final result of this section is the analog of Proposition 2.26 and its corollaries leading up to the result that even CAC does not imply DNR and so, by the results of Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta], it implies neither SRT_{2}^{2} nor RT_{2}^{2}.

Proposition 3.9. Let P be a stable partial order computable in a set X such that there is no diagonally noncomputable function computable in X. There is then a chain or antichain G in P such that no diagonally noncomputable function is computable in G⊕X.

Proof. As usual we assume X is computable. If there is a computable antichain in P we are done, so assume not. Let F be the forcing relation defined in the proof of Theorem 3.4 from P (again assuming P satisfies (1) in the definition of stability). Let G be any 2-generic for F. Then G is obviously an ascending chain in P so suppose for the sake of a contradiction that some Φ_{e}^{G} is a diagonally noncomputable function. Now argue as in Proposition 2.26 that we can computably produce infinitely many elements ⟨b_{i}⟩ of \overline{U} = \{i | (∃s)(∀j > s)(i |_{P} j)\}. We can now thin out this set as in the proof of Theorem 3.4 to get a computable antichain in P as required.

Corollary 3.10. SCAC ⊬ DNR and hence SCAC ⊬ WKL_{0}.

Proof. By the usual iteration and dovetail argument we can use Proposition 3.9 to build an ω-model of SADS in which there is no diagonally noncomputable function, and which is therefore not a model of DNR.

Corollary 3.11. CAC ⊬ DNR and hence CAC ⊬ WKL_{0}.

Proof. We can combine the forcing of Proposition 3.9 with those used to prove Corollary 2.28 to get an ω-model in which both SCAC and ADS hold but in which there is no diagonally noncomputable function, and which is therefore not a model of DNR. By Proposition 3.8 this model is also a model of CAC.

Corollary 3.12. CAC ⊬ SRT_{2}^{2} and so CAC ⊬ RT_{2}^{2}.

Proof. Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta] show that SRT_{2}^{2} ⊢ DNR and so neither SRT_{2}^{2} nor RT_{2}^{2} can be a consequence of CAC.

This result answers Question 3.18 of CJS.

We can now add to Diagram 2 as follows:

[figure: RT_{2}^{2}; (1,2); _{SRT2 2}; (3); (1); DNR; CAC; |; (2); (4); (5); _{WKL_{0}}; |; (12); COH; SCAC; |; (6); (7); ADS; (8); (9); COH; (11); COH + WKL_{0}; |; (10); SADS; (13); CADS; (13); _{RCA_{0}}]

Diagram 3 The references for these results are as follows: (1) Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta]; (2) Corollary 3.11; (3) Proposition 3.3 and Corollary 3.6; (4) Proposition 3.8 and Corollary 3.6; (5) Proposition 3.1; (6) Corollary 3.6; (7) Proposition 3.3; (8) Proposition 2.7 and Corollary 2.16; (9) Proposition 2.10 and Corollary 2.22; (10) Corollary 2.25; (11) Proposition 2.9; (12) Corollary 2.16; (13) Corollary 2.6.

4 BΣ_{2}

As we mentioned in §1, CJS show that SRT_{2}^{2} ⊢ BΣ_{2} and so SRT_{2}^{2} is not conservative over RCA_{0} (even for Σ_{3}^{0} sentences). This shows that COH does not imply SRT_{2}^{2} as COH is conservative over RCA_{0} for even more than Π_{1}^{1} sentences (CJS and Corollary 2.21). In this section we show that both SCAC and ADS imply BΣ_{2} and that there are alternate versions StCOH and StCADS of COH and CADS, respectively, which imply BΣ_{2} and are equivalent to each other. Each is also equivalent to the original version plus BΣ_{2}. We also show that SADS is not Π_{1}^{1}-conservative over RCA_{0}. It is convenient to work with the following Ramsey type principle, which by Hirst [1987, Theorem 6.4] (or see CJS Theorem 2.10) is equivalent to BΣ_{2} over RCA_{0}.

(RT_{<∞}^{1}) For every n ∈ ℕ and every map f : ℕ → n there is an infinite set H such that |f“H| = 1.

Proposition 4.1. RCA_{0} ⊢ SCAC → BΣ_{2}.

Proof. We prove RT_{<∞}^{1} using SCAC. Suppose f : ℕ → n. Define a partial order P by x <_{P} y if and only if x < y and f(x) = f(y). If there is an i such that f^{−1}“{i} is infinite, we are done. If each such set is finite, then for every x almost every y is P-incomparable with x, as for any x, y ∈ ℕ, if f(x) ≠ f(y) then x |_{P} y. Thus P is stable. A chain in P would be a subset of a single f^{−1}“{i} and so homogeneous for f. An antichain A would be an infinite set every element of which has a different color, and so restricting f to A would yield a one-to-one map from an infinite set into n, which is not possible in RCA_{0}.

We now introduce alternative versions of COH and CADS that might have been equally plausible principles to consider instead of the original versions.

Definition 4.2. If R⃗ = ⟨R_{i} | i ∈ ℕ⟩ is a sequence of sets, an infinite set S is strongly R⃗-cohesive if (∀n)(∃s)(∀i ⩽ n)[(∀j > s)(j ∈ S → j ∈ R_{i}) ∨ (∀j > s)(j ∈ S → j ∉ R_{i})].

(StCOH) For every sequence R⃗ of sets there is a strongly R⃗-cohesive set.

Definition 4.3. An infinite linear order L with first and last elements (0 and 1, respectively) in which all nonfirst elements have immediate predecessors and all nonlast ones have immediate successors is strongly of type ω +ω^{∗} if, for every finite ascending sequence 0 = x_{0} <_{L} x_{1} <_{L} ⋯ <_{L} x_{n} = 1, there is exactly one infinite subinterval [x_{i}, x_{i+1}), and both [x_{0}, x_{i}] and [x_{i}, x_{n}] are finite.

(StCADS) Every infinite linear order has a suborder that is either of type ω or ω^{∗}, or strongly of type ω + ω^{∗}.

Each of these strong principles clearly implies the usual version. In the presence of BΣ_{2} the notions of strongly cohesive and strongly of type ω + ω^{∗} coincide with those of cohesive and of type ω + ω^{∗}, respectively, so the converses also hold in this context. Furthermore, using the strong versions of our principles makes them actually imply BΣ_{2}.

Proposition 4.4. RCA_{0} ⊢ COH + BΣ_{2} ↔ CADS + BΣ_{2} ↔ StCADS ↔ StCOH.

Proof. COH + BΣ_{2} implies CADS + BΣ_{2} by Proposition 2.9.

To see that CADS + BΣ_{2} implies StCADS we just have to show that the two notions of being of type ω + ω^{∗} are equivalent given BΣ_{2}. Let L be of type ω + ω^{∗}, with first element 0 and last element 1. If 0 = x_{0} <_{L} x_{1} <_{L} ⋯ <_{L} x_{n} = 1 is a finite sequence then define f : ℕ → n by f(x) = i where i is least such that x ⩽_{L} x_{i}. (Such an i exists for every x by IΣ_{1} and f then exists by Δ_{1}^{0}-CA.) By BΣ_{2} in the form of RT_{<∞}^{1}, there is an i such that f(x) = i for infinitely many x. Thus [x_{i−1}, x_{i}) is infinite. Now x_{i} has infinitely many predecessors and so only finitely many successors, while x_{i−1} has infinitely many successors and so only finitely many predecessors. Thus L is strongly of type ω + ω^{∗}.

Next we assume StCADS and prove StCOH. Consider the proof in Proposition 2.10 that ADS → COH. Given a sequence R⃗ of sets, it defines a linear order L and actually shows that any ascending or descending sequence in L is a strongly R⃗-cohesive set. All that remains is to show that we can also get such a set from a suborder S of L that is strongly of order type ω + ω^{∗}. Given n ∈ ℕ, we define an ascending sequence in S with at most 2^{n+1} + 1 many elements. We first get the set F of σ ∈ 2^{n+1} such that there is an x ∈ S with σ = ⟨R_{i}(x) | i ⩽ n⟩. For each σ ∈ F we let x_{σ} be the ℕ-least x ∈ S witnessing that σ ∈ F. Our ascending sequence in S is given by listing {x_{σ} | σ ∈ F } in increasing L-order (i.e. increasing lexicographic order on the σ ∈ F) adding on if necessary the last element of S. Thus, by the assumption that S is strongly of type ω+ω^{∗}, there is a unique infinite interval [x_{σ}, x_{τ}) and there are only finitely many elements of S that are L-below x_{σ} or L-above x_{τ}. Thus ⟨R_{i}(x) | i ⩽ n⟩ = σ for all but finitely many x ∈ S, and so S is strongly R⃗-cohesive.

Finally, we assume StCOH and prove RT_{<∞}^{1}. (StCOH obviously implies COH.) Let f : ℕ → n and define a sequence of sets R_{i} for i < n by R_{i} = {x | f(x) = i}. Let S be strongly cohesive for this sequence. Thus there is an s such that (∀i < n)[(∀j > s)(j ∈ S → j ∈ R_{i}) ∨ (∀j > s)(j ∈ S → j ∉ R_{i})]. As f is total, there is no j for which the second disjunct can hold for every i < n. Thus there must be an i < n for which the first disjunct holds. This R_{i} is cofinite in S and so infinite as required.

Proposition 4.5. RCA_{0} ⊢ ADS → StCOH and so RCA_{0} ⊢ ADS → BΣ_{2}.

Proof. The proof of Proposition 2.10 that (in RCA_{0}) ADS → COH actually shows that ADS → StCOH.

Finally, although we do not know whether SADS implies BΣ_{2}, we do know that it is not Π_{1}^{1}-conservative over RCA_{0}. To prove this, we introduce the following principle, which follows from BΣ_{2} by the proof of Proposition 4.4.

(PART) Every linear order of type ω + ω^{∗} is strongly of type ω + ω^{∗}.

Proposition 4.6. RCA_{0} ⊢ SADS → PART.

Proof. Let L be a linear order of type ω + ω^{∗} with first element 0 and last element 1. Let 0 = x_{0} <_{L} x_{1} <_{L} ⋯ <_{L} x_{n} = 1 for some n ∈ ℕ be a finite sequence. By SADS there is an ascending or descending sequence S in L. Suppose it is ascending. By IΠ_{1} (which is equivalent to IΣ_{1}) there is a least i ⩽ n such that all elements of S are below x_{i}. The interval [x_{i−1}, x_{i}) then contains infinitely many elements (a final segment, actually) of S. As in the proof of Proposition 4.4, we see that there are only finitely many elements below x_{i−1} or above x_{i} as required in the definition of L being strongly of type ω + ω^{∗}. The argument for a descending sequence S is symmetric.

Corollary 4.7. RCA_{0} ⊬ PART and so SADS is not Π_{1}^{1}-conservative over RCA_{0}.

Proof. PART is a Π_{1}^{1} consequence of SADS by Proposition 4.6. If it were a theorem of RCA_{0} then in RCA_{0} we would have that CADS implies StCADS, which implies BΣ_{2} by Proposition 4.4. This would contradict the fact that, as it is a consequence of COH, CADS is Π_{1}^{1}-conservative over RCA_{0}.

We conclude this section by considering the principle CRT_{2}^{2}, introduced in §1, which states that every 2-coloring of pairs has a set on which it is stable, and the following stronger version analogous to those considered above.

(StCRT_{2}^{2}) Strongly Cohesive Ramsey’s Theorem for pairs: For every coloring f of [ℕ]^{2} there is an infinite set S on which f is strongly stable, i.e. such that (∀n)(∃y)(∀x ∈ S)(x < n → (∀z ∈ S)[z > y → f(x, y) = f(x, z)]).

Proposition 4.8. RCA_{0} ⊢ StCRT_{2}^{2} ↔ CRT_{2}^{2} + BΣ_{2} ↔ StCOH.

Proof. To see that StCRT_{2}^{2} → BΣ_{2} first note that StCRT_{2}^{2} clearly implies StCRT_{3}^{2} (the same principle for 3-colorings) by the usual argument considering first the 2-coloring gotten by taking as the first color the union of the first two of the given three colors and then if necessary applying StCRT_{2}^{2} again to a set homogeneous to this union. Next, consider any counterexample f : ℕ → n to RT_{<∞}^{1}. As usual, define a coloring by letting C(x, y) be 0 if f(x) = f(y), letting it be 1 if f(x) < f(y), and letting it be 2 if f(x) > f(y). Let S be a set on which C is strongly stable. No x can be stable within S to 0 as each f^{−1}[i] is finite. Let F = {i < n | (∃s ∈ S)(f(s) = i)}. This set is finite by IΣ_{1}. Let A = {a_{i} | i ∈ F and a_{i} is the least a ∈ S such that f(a) = i}. Again A is finite and so by assumption there is a y ∈ S such that (∀z ∈ S)[z > y → C(a_{i}, y) = C(a_{i}, z)] for every i ∈ F. If C(a_{i}, y) = 1 or 2 then f(y) = j ≠ i for some j ∈ F and so C(a_{j}, y) = 0 for the desired contradiction.

Next we assume CRT_{2}^{2} + BΣ_{2} and consider any sequence of sets R_{0}, R_{1}, … (with the aim of constructing a cohesive set for the sequence). We appeal to the proof that RCA_{0} ⊢ RT_{2}^{2} → COH in Mileti [2004]. Let d(a, b) be the least i such that R_{i}(a) ≠ R_{i}(b). Since we can always add more sets to the R_{i}, without loss of generality the function d is total, and we define a coloring C by C(a, b) = R_{d(a,b)}(a). Mileti [2004] shows in RCA_{0} that any set homogenous for C is cohesive for the R_{i}. Let S be such that C is stable on S. If S is not cohesive for the R_{i} then there is a k for which there are infinitely many s ∈ S such that s ∈ R_{k} and infinitely many t ∈ S such that t ∉ R_{k}. By BΣ_{2} there are finite strings ρ_{0} and ρ_{1} of length k + 1 with ρ_{i}(k) = i for i = 0, 1 such that there are infinitely many t ∈ S for which t ∈ R_{j} ⇔ ρ_{0}(j) = 1 for j ⩽ k and infinitely many s ∈ S for which s ∈ R_{j} ⇔ ρ_{1}(j) = 1 for j ⩽ k. Let l ⩽ k be least such that ρ_{0}(j) ≠ ρ_{1}(j). Consider now the sets A = {t ∈ S | (∀j ⩽ k)(t ∈ R_{j} ⇔ ρ_{0}(j) = 1)} and B = {s ∈ S | (∀j ⩽ k)(s ∈ R_{j} ⇔ ρ_{1}(j) = 1)}. Both sets are infinite and if a ∈ A and b ∈ B with a < b then C(a, b) = R_{l}(a) = ρ_{0}(l). Thus every a ∈ A is stable within S to ρ_{0}(l). The usual construction of a homogeneous set H for C from a set whose elements are all stable to the same color can now be carried out using BΣ_{2}. (Define a sequence a_{i} by recursion where a_{i+1} is the least element a of A such that C(a_{j}, a) = ρ_{0}(l) for j < i. There is such an a by BΣ_{2} and the recursion is then Δ_{1}^{0}.) As mentioned above, H is cohesive for the R_{i}.

Finally, note that StCOH → CRT_{2}^{2} + BΣ_{2} by Propositions 1.4 and 4.4, while these two together clearly imply StCRT_{2}^{2}.

We summarize our results in the following diagram. We list here only those references not given after Diagram 3: (1) Proposition 4.1; (2) Proposition 4.5; (3) proof of Proposition 4.4; (4) Proposition 4.6; (5) Proposition 4.4; (6) Corollary 4.7; (7) Proposition 4.4;

(8) Proposition 4.4 and Corollary 2.21; (9) Corollary 2.21; (10) Corollary 2.6 (since the proof of that corollary shows that COMP is not a model of CADS); (11) Proposition 4.8;

(12) Proposition 1.4; (13) Proposition 2.9.

[figure: RT_{2}^{2}; _{SRT2 2}; DNR; CAC; |; COH; SCAC; |; (1); ADS; (2); BΣ_{2}; (3); COH + WKL_{0}; |; (9); SADS; (4); _{StCRT2 2}; StCOH; (5); (11); StCADS; (8); (7); BΣ_{2}; |; (10); PART; (6); COH; (12); |; (9); _{CRT2 2}; (13); CADS; _{WKL_{0}}; |; _{RCA_{0}}]

Diagram 4

5 Transitive and Semitransitive Colorings

In this section we will try to isolate the properties of colorings that allow us to prove that ADS or CAC is weak in some way that RT_{2}^{2} is not or is not known to be. In particular, each of ADS and CAC can be split into a stable version that has low solutions and the cohesive principle COH that does not, but is conservative over RCA_{0}. Moreover, neither implies WKL_{0} nor even DNR. If we examine the proofs of these results the primary issue is seen to be one of some transitivity of the coloring. We isolate the required properties in the definitions of transitive and semitransitive colorings below. The existence of homogeneous sets for such colorings clearly implies ADS and CAC, respectively. We will prove that the implications can be reversed and so provide classes of colorings corresponding to ADS and CAC. We also examine the relation between the stable versions of the coloring principles and SCAC and SADS.

Definition 5.1. An n-coloring of [ℕ]^{2} (as in Definition 1.1) is transitive if each f^{−1}[i] (i.e. the set C_{i} of pairs in the natural ordering of ℕ with color i) is a transitive relation, i.e. C_{i}(x, y) ∧ C_{i}(y, z) → C_{i}(x, z). (With this view we identify the coloring with the sequence C⃗.) An n-coloring is semitransitive if each C_{i} is a transitive relation, except possibly for one i. Homogeneity and stability for such colorings is as usual.

Thus, for example, if L is a linear order (on ℕ) then C_{0}(x, y) ↔ x <_{ℕ} y ∧ x <_{L} y and C_{1}(x, y) ↔ x <_{ℕ} y ∧ x >_{L} y define a transitive 2-coloring. Moreover, any H homogeneous for this coloring is an ascending or descending sequence in L (depending on whether H is homogeneous to C_{0} or C_{1}, respectively). Similarly, if P is a partial order (on ℕ), let C_{0}(x, y) ↔ x <_{ℕ} y ∧ x |_{P} y, let C_{1}(x, y) ↔ x <_{ℕ} y ∧ x <_{P} y, and let C_{2}(x, y) ↔ x <_{ℕ} y ∧ x >_{P} y; this defines a semitransitive 3-coloring. If H is homogeneous, then H is an antichain in P (if homogeneous to C_{0}), an ascending sequence (if homogeneous to C_{1}), or a descending sequence (if homogeneous to C_{2}). Thus the assumptions that there are always homogeneous sets for transitive 2-colorings and for semitransitive 3-colorings imply ADS and CAC, respectively.

Now for semitransitive n-colorings an inductive argument shows that the principle of existence of homogeneous sets for n-colorings is equivalent to that for 2-colorings: Given an n-coloring C⃗ with n > 2 and C_{0} not transitive define a semitransitive 2-coloring D⃗ by setting D_{0} = C_{0} ∪ ⋯ ∪ C_{n−2} and D_{1} = C_{n−1}. A homogeneous set for D⃗ is either homogeneous to D_{1} = C_{n−1}, and so is a homogeneous set for C⃗, or to D_{0}. In the latter case we define a new 2-coloring E⃗ with E_{0} = C_{0} ∪ ⋯ ∪ C_{n−3} and E_{1} = C_{n−2} and consider a homogeneous set for E⃗. Iterating at most n − 1 times we arrive at a set homogeneous for the original n-coloring C⃗. The same argument works for the principles limited to stable colorings, as the union operation preserves stability. Such considerations lead to the usual situation that, in a context with limited induction, we have a difference between the assertions of the instances of some principle for each standard n and the assertion that the principle holds for every n. We leave these issues aside and turn to the proofs that CAC and ADS imply the existence of homogeneous sets for the appropriate types of colorings.

Theorem 5.2. For each n ∈ ω, we can prove in RCA_{0} that CAC implies the principle that every semitransitive n-coloring has a homogeneous set, and so for n ⩾ 2, each such principle is equivalent to CAC.

Proof. Consider first the case that n = 2 and assume that C_{0} is not necessarily transitive, but C_{1} is transitive. Define a relation P on ℕ by x <_{P} y ↔ x < y ∧ C_{1}(x, y). As C_{1} is transitive, P is a partial order. A chain in P is homogeneous to C_{1}. An antichain is homogeneous to C_{0}. We now proceed by induction (on ω) as above to deduce the principle for n > 2.

Theorem 5.3. In RCA_{0}, we can prove that ADS implies that every transitive 2-coloring has a homogeneous set, and so this principle is equivalent to ADS.

Proof. Suppose that C_{0}, C_{1} define a transitive 2-coloring of ℕ. We define a linear order L on ℕ by recursion. Begin by putting 0 into the domain of L. Suppose at stage n we have ordered the numbers less than n in L. Find the L-largest k <_{ℕ} n such that C_{0}(k, n). If there is no such k, declare n to be L-below every number less than n. Otherwise, insert n into the L order L-above k and L-below the L-immediate successor of k among the numbers less than n. This defines the linear order L on ℕ. Let H be an ascending or descending sequence in L.

If H is a descending sequence in L, we may take it to also be ascending in natural order as it is infinite. We then claim that H is homogeneous to C_{1}. If not then there are s <_{ℕ} t in H such that C_{0}(s, t). By the definition of L, when t is put into the order, it is put in L-above s, which contradicts the fact that H is a descending sequence.

If H is ascending, we may again take it to be ascending in natural order. We claim H is then homogeneous to C_{0}. In fact, we claim that if s <_{ℕ} t and s <_{L} t then C_{0}(s, t). If not, let s be ℕ-least such that there is a t greater than s in both natural and L order such that C_{1}(s, t) and then let t be the ℕ-least such number for this s. (This pair exists by Σ_{1} induction.) Consider the situation when t is added to L. As s <_{L} t, there must be some t_{0} <_{ℕ} t that is greater than or equal to s in the L order such that C_{0}(t_{0}, t). We cannot have s = t_{0} by our assumption that C_{1}(s, t). If t_{0} <_{ℕ} s then, by the definition of the order construction at s, we have C_{1}(t_{0}, s), as otherwise we would have put s in L-above t_{0}. As we also have by assumption that C_{1}(s, t), transitivity of C_{1} gives C_{1}(t_{0}, t) for a contradiction. Finally we cannot have s <_{ℕ} t_{0} by our leastness assumption on t.

We next consider the stable versions of these principles. Our first result provides the final evidence that SCAC is the correct stable version of CAC. The others deal with SADS and stable transitive partitions.

Proposition 5.4. RCA_{0} ⊢ SCAC ↔ every stable semitransitive 2-coloring has a homogeneous set.

Proof. Suppose C is a stable semitransitive 2-coloring. Let P be as defined in the proof of Theorem 5.2. If x is stable to C_{1} then for almost every y, we have C_{1}(x, y) and so x <_{P} y. On the other hand, if x is stable to C_{0} then for almost every y, we have x |_{P} y. So P is stable. Thus the proof of Theorem 5.2 provides our desired homogeneous set. For the other direction, suppose that P is stable. The standard 3-coloring as defined above to show that this implication works for arbitrary partial orders and colorings is stable and the same proof as in the general case shows that a homogeneous set gives the desired chain or antichain.

Proposition 5.5. RCA_{0} ⊢ every stable transitive 2-coloring has a homogeneous set → SADS.

Proof. The proof of Proposition 2.8 works here as well, as the coloring used there is transitive.

Proposition 5.6. RCA_{0} + BΣ_{2} ⊢ SADS → every stable transitive 2-coloring has a homogeneous set.

Proof. Consider the proof of Theorem 5.3. We only have to show that the linear order L defined there is of type ω + ω^{∗} if the coloring is stable. Consider any n. If there is an m >_{L} n that is stable to C_{0} then by definition x >_{L} n for almost every x. Otherwise, consider the construction of L at stage n. There are some numbers x_{1}, …, x_{k} ⩽_{ℕ} n that are L-above or equal to n. We claim by Σ_{1} induction that, for m >_{ℕ} n, we have m >_{L} n if and only if the following condition holds: there is a finite chain m = y_{0} >_{L} ⋯ >_{L} y_{j} = x_{i} for some i ⩽ k such that the y_{l} are also descending in natural order, and for each l < j, we have C_{0}(y_{l+1}, y_{l}). To establish this claim, we argue as follows. When m is put into the ordering and is placed above n it must be placed above some z ⩾_{L} n with z <_{ℕ} m and C_{0}(z, m). The claim now follows by the transitivity of the coloring (and Σ_{1} induction). Now, by BΣ_{2} and our case assumption there is an s after which all the x_{i} are stable to 1 and so there are only finitely many m >_{L} n as required.

Note that we can run through the versions of these principles and their connections with BΣ_{2} as in §4. As an example, we note that an examination of the preceding two proofs shows that, in RCA_{0}, SADS for orders strongly of type ω + ω^{∗} is equivalent to the principle stating that every strongly stable transitive 2-coloring has a homogeneous set.

6 Questions

From our point of view, the main combinational/reverse mathematics questions left open in CJS are whether SRT_{2}^{2} implies COH and so RT_{2}^{2}, whether CAC implies RT_{2}^{2} and whether RT_{2}^{2} implies WKL_{0} (all over RCA_{0}). We have answered the analogous questions for CAC and ADS negatively (and on the positive side have shown that CAC and ADS do imply COH and BΣ_{2}). In addition, we have shown (in conjunction with Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman [ta]) that CAC does not imply RT_{2}^{2}. The other questions for RT_{2}^{2} remain open. To these we add the following:

Question 6.1. Does ADS imply CAC?

Question 6.2. Does SADS imply SCAC?

Of course a positive answer to Question 6.2 would imply a positive one to Question 6.1.

One obvious question is raised by our results on (semi)transitive colorings:

Question 6.3. Are there m > n ⩾ 2 such that the existence of homogeneous sets for all transitive n-colorings implies the same for m-colorings?

If, for example, there are no such m and n then we would have a whole hierarchy of Ramsey type principles intermediate between ADS and CAC as, by Theorem 5.2, CAC implies that every transitive m-coloring has a homogeneous set for every m.

There are also two obvious combinatorial/reverse mathematics questions raised by our analysis of the relationships between BΣ_{2}, StCADS, and StCOH.

Question 6.4. Does CRT_{2}^{2} or even CADS imply COH?

Question 6.5. Does SADS or even PART imply BΣ_{2}?

Next, we see the primary proof theoretic question left open in CJS as whether SRT_{2}^{2} or even RT_{2}^{2} is conservative over BΣ_{2}. The problem of proving conservativity over BΣ_{2} seems difficult. External forcing arguments of the sort used in CJS and in our proof of Theorem 2.20 and Corollary 2.21 can at times be used to get conservation results over IΣ_{2} (or more) when the forcing relation for Σ_{2} (or Π_{2}) sentences is Σ_{2}^{0} (Π_{2}^{0}, respectively). This is done in CJS to prove that even RT_{2}^{2} is Π_{1}^{1}-conservative over RCA_{0} + IΣ_{2}. The problem at the level of BΣ_{2} is that what one would want to do is consider each sentence of the form (∀i < n)(∃s)(∀t)φ(i, s, t) that is true in the forcing extension and so forced by a condition p. Of course, for each i < n there is an s and a condition q ⊩ ∀t φ(i, s, t) with q ⩽ p. As long as this assertion about i is Σ_{2}^{0} in the ground model one might hope to apply BΣ_{2} in the ground model to get a single condition forcing everything and so the desired bound in the extension. The problem is that producing such a condition seems to require a recursive construction of n many successive conditions rather than a bounding argument. Unfortunately, the existence of n many recursive iterations of even Π_{1}^{0} functions for each n ∈ ℕ implies IΣ_{2} over RCA_{0} (indeed, over just IΔ_{1}^{0}, which follows from P_{0} + Δ_{1}^{0}-CA) and so cannot be applied in arbitrary models of BΣ_{2} to get such a conservation result. We can make this statement more precise by considering the following family of principles:

(PREC_{n}) If φ(x, y) ∈ Π_{n−1} defines a total function then (∀z)(∀m)(∃σ)[|σ| = m ∧ σ(0) = z ∧ (∀i < m)φ(σ(i), σ(i + 1))].

In the presence of Δ_{1}^{0}-CA (even without IΣ_{1}), this principle for n = 1 is easily seen to be equivalent to the following:

(PREC) ∀z ∀f ∃g [g(0) = z ∧ ∀n (g(n + 1) = f(g(n))] where we use f and g to range over functions (with the understanding that this is an abbreviation for the translation into formulas with variables over sets).

Proposition 6.6. For each n ⩾ 1, we have P_{0} + IΔ_{1}^{0} ⊢ PREC_{n} ↔ IΣ_{n}.

Proof. To see that IΣ_{n} implies PREC_{n}, fix z and prove the assertion of PREC_{n} by Σ_{n}- induction on m.

For the other direction, we proceed by induction on n. We begin with PREC_{1}. Consider a Σ_{1}^{0} formula ∃x ψ(i, x) such that ∃x ψ(0, x) ∧ ∀k (∃x ψ(k, x) → ∃x ψ(k + 1, x)).

We must show that ∀k ∃x ψ(k, x). Define the formula φ(⟨i, x⟩, ⟨n, z⟩) by

[¬ψ(i, x) ∧ n = z = 0] ∨ [ψ(i, x) ∧ n = i + 1 ∧ ψ(i + 1, z) ∧ (∀z′ < z)¬ψ(i + 1, z′)].

This formula is Π_{0}^{0} and defines a total function by IΔ_{1}^{0} and our assumptions on ψ. To prove ∀k ∃x ψ(k, x), consider any k. By PREC_{1} there is a σ of length k + 2 such that σ(0) is a witness that ∃x ψ(0, x) and φ(σ(i), σ(i + 1)) holds for i < k. Using IΔ_{1}^{0}, we can now prove that ψ(i, σ(i)) holds for every i ⩽ k and so ∃x ψ(k, x) as required.

Next, assume PREC_{n−1} for n > 1, which by induction implies IΣ_{n−1}. Consider any Σ_{n}^{0} formula ρ = ∃x ∀y θ(k, x, y) and assume that ρ(0) ∧ ∀k (ρ(k) → ρ(k + 1)). We wish to prove ∀k ρ(k). The proof is like that in the n = 1 case with one added layer of uniformization. Let φ(⟨i, x_{0}, x_{1}⟩, ⟨m, z_{0}, z_{1}⟩) be

[¬θ(i, x_{0}, z_{0}) ∧ (∀w < z_{0})θ(i, x_{0}, w) ∧ m = z_{1} = 0] ∨ [ ∀y θ(i, x_{0}, y) ∧ m = i + 1 ∧ ∀y θ(i + 1, z_{0}, y) ∧ z_{1} is a sequence of length z_{0} ∧ (∀w < z_{0})¬θ(i + 1, w, z_{1}(w)) ∧ (∀z′ < z_{1})(if z′ is a sequence of length z_{0} then

¬(∀w < z_{0})¬θ(i + 1, w, z′(w)) ].

This formula is Π_{n−1} and, by our assumptions (including IΠ_{n−1}, which is equivalent to IΣ_{n−1}), defines a total function. Iterating it for n many steps starting at ⟨0, x_{0}, 0⟩ for an x_{0} such that ∀y θ(0, x_{0}, y) produces the sequence of witnesses needed to show that (∀i ⩽ n)ρ(i). Thus PREC_{n} proves ∀n ρ(n) by reducing the induction needed one quantifier level as in the n = 1 case.

We note that PREC or PREC_{1} give a comprehension axiom that could be adopted in place of IΣ_{1} in the definition of RCA_{0} (given by Simpson [1999]). These axioms assert only the existence of (even just finite) iterations of given functions and make no additional induction assumptions. This is the route followed by Friedman [1976] to define his EFT (elementary theory of functions) as the base theory to which Δ_{1}^{0}-CA is added to get RCA_{0}.

Returning now to BΣ_{2}, we note that the only conservation results at this level of which we are aware are by Hájek [1993] and Avigad [2002] for WKL_{0}.^{2} Hájek uses a priority argument in RCA_{0} (and so one that is carried out internally in each model of BΣ_{2}) to produce a definable universal solution G to all instances of WKL_{0} computable in a fixed set X such that the verification of BΣ_{2} for sentences involving G can be reduced to ones for sentences with X but without G. (Computability theoretically, what he proves is that the construction of the Jockusch-Soare Low Basis Theorem can be used to produce a path P such that P′ ⩽_{tt} 0′ and that this suffices.) Following this outline one might hope to prove that SADS, for example, is conservative over BΣ_{2}. The idea would be to use the priority argument in the proof of Theorem 2.11 to produce low solutions for SADS in an arbitrary models of BΣ_{2}. As G is low, Σ_{2}^{0}(G) ∈ Σ_{2}^{0} and so BΣ_{2} would hold in the extension generated by G. One would then iterate as in Hájek [1993] to get a model of SADS + BΣ_{2} with the same first order part as the original model. (This could then be extended to get Π_{1}^{1}-conservativity by relativizing.)

2Chong, Slaman, and Yang have recently announced a proof that COH is Π_{1}^{1}-conservative over BΣ_{2}.

Unfortunately, it does not seem as if the priority argument of Theorem 2.11 can be carried out in BΣ_{2} as it is a Sacks type argument with unbounded injuries rather than a Friedberg-Muchnik one where the number of injuries is computably bounded. Also, the iteration used in Hájek [1993] is done through a cut (a (typically) proper initial segment of the first order part or the given model). Unfortunately, this means that the proof that all instances of the problem at hand get solutions added on during the iteration relies on the generic G being a universal solution, i.e. on there being a solution computable in G for every computable instance of the problem. (In the case of WKL_{0} an instance of the problem is an infinite binary tree and the solution an infinite path in the tree. In the case of SADS an instance of the problem is a linear order of type ω + ω^{∗} and the solution a suborder of type ω or ω^{∗}.) Theorem 2.18, however, shows that there is no such universal instance of SADS. (If there were one then it would have a low solution S by Theorem 2.11, but by Theorem 2.18 there would be another instance of SADS that has no solution computable in S.)

On the other path in our diagrams of implications and nonimplications the weakest principle is CADS, which, in the presence of BΣ_{2}, is equivalent to COH. Here we seem to have a sufficiently universal instance of the problem given by the sequence of primitive recursive sets. Our problem for COH is that no internal argument in BΣ_{2} produces even a low_{2} solution. It is true that CJS prove that there always is a low_{2} solution (and so, in particular, a low_{2} p-cohesive set) but the proof does not work in BΣ_{2}. Indeed, it seems likely that by using and extending the ideas of Mourad [1988, Ch. II] as well as some further computability theoretic information about solutions to COH one could show that it is not possible to produce low_{2} solutions for COH in BΣ_{2} in the desired way. Indeed, it seems that if, provably in BΣ_{2}, there is a formula that for every sequence R⃗ uniformly defines an R⃗-cohesive set S such that the complete Σ_{1}^{0} set in S is Δ_{3}^{0} in R⃗, then IΣ_{2} holds.^{3} Nonetheless, as mentioned above Chong, Slaman, and Yang have recently announced a proof that COH is Π_{1}^{1}-conservative over BΣ_{2}. Perhaps their methods can be extended to other principles considered here.

Thus we close with an open-ended question about conservativity over BΣ_{2}.

Question 6.7. Are any of the principles weaker than ACA_{0} that we have considered (other than those following from WKL_{0} or COH) Π_{1}^{1}- or even just arithmetically conservative over BΣ_{2}? ^{4}

3We thank Carl Jockusch for some useful conversations and Chi Tat Chong for some useful correspondence about this point.

4As mentioned above, Hirschfeldt, Shore, and Slaman have recently studied another principle, AMT.

It asserts that every complete atomic theory has an atomic model. This principle lies strictly between SADS and RCA_{0} but is Π_{1}^{1}-conservative over BΣ_{2} as well as RCA_{0}.

References

[1] Ambos-Spies, K.; Kjos-Hanssen, B.; Lempp, S.; Slaman, T. A. [2004], Comparing DNR and WWKL. J. Symbolic Logic 69, 1089–1104.

[2] Arslanov, M.; Cooper, S. B.; Li, A. [2004], There is no low maximal d.c.e. degree — corrigendum. Math. Log. Quart. 50, 628–636.

[3] Avigad, J. [2002], Notes on Π_{1}^{1}-conservativity, ω-submodels, and the collection schema. Carnegie Mellon Technical Report CMU-PHIL-125 (updated version avail-

able at http://www.andrew.cmu.edu/user/avigad/papers.html).

[4] Cholak, P. A.; Jockusch, Jr., C. G.; Slaman, T. A. [2001], On the strength of Ramsey’s Theorem for pairs. J. Symbolic Logic 66, 1–55.

[5] Cooper, S. B. [1972], Jump equivalence of the Δ_{2}^{0} hyperhyperimune sets. J. Symbolic Logic 37, 598–600.

[6] Downey, R. G. [1998], Computability theory and linear orderings. Handbook of Recursive Mathematics (Ershov, Goncharov, Nerode, Remmel, eds.), Stud. Logic Found. Math. 138–139, Elsevier, Amsterdam, 823–976.

[7] Downey, R.; Hirschfeldt, D. R.; Lempp, S.; Solomon, R. [2001], A Δ_{2}^{0} set with no infinite low subset in either it or its complement. J. Symbolic Logic 66, 1371–1381.

[8] Friedman, H. [1976], Systems of second order arithmetic with restricted induction I (abstract). J. Symbolic Logic 41, 557–558.

[9] Giusto, M.; Simpson, S. G. [2000], Located sets and reverse mathematics. J. Symbolic Logic 65, 1451–1480.

[10] Goncharov, S. S; Nurtazin, A. T. [1973], Constructive models of complete decidable theories. Algebra and Logic 12, 67–77.

[11] Hájek, P. [1993], Interpretability and fragments of arithmetic. Arithmetic, Proof Theory, and Computational Complexity (Prague, 1991), Oxford Logic Guides 23, Oxford Univ. Press, New York, 185–196.

[12] Hájek, P.; Pudlák, P. [1998], Metamathematics of First-Order Arithmetic, second printing. Perspect. Math. Logic, Springer-Verlag, Berlin.

[13] Harizanov, V. [1998], Turing degrees of certain isomorphic images of computable relations, Ann. Pure and Applied Logic, 93, 103-113.

[14] Herrmann, E. [2001], Infinite chains and antichains in computable partial orderings. J. Symbolic Logic 66, 923–934.

[15] Hirschfeldt D. R.; Jockusch, Jr., C. G.; Kjos-Hanssen, B.; Lempp, S.; Slaman, T. A. [ta], Some Remarks on the Proof-theoretic Strength of Some Combinatorial Principles. To appear in the proceedings of the Program on Computational Prospects of Infinity, Singapore 2005.

[16] Hirst, J. [1987], Combinatorics in Subsystems of Second Order Arithmetic, Ph.D. Dissertation, Pennsylvania State University.

[17] Jockusch, Jr., C. G. [1972], Ramsey’s Theorem and recursion theory. J. Symbolic Logic 37, 268–280.

[18] Jockusch, Jr., C. G.; Soare, R. I. [1972], Π_{1}^{0} classes and degrees of theories. Trans. Amer. Math. Soc. 173, 33–56.

[19] Jockusch, Jr., C. G.; Stephan, F. [1993], A cohesive set which is not high. Math. Log. Quart. 39, 515–530 (correction in Math. Log. Quart. 43, 569).

[20] Lerman, M. [1981], On recursive linear orderings. Logic Year 1979–1980 (Lerman, Schmerl, Soare, eds.), Lecture Notes in Math. 859, Springer-Verlag, Berlin, 132–142.

[21] Mileti, J. R. [2004], Partition Theorems and Computability Theory. Ph.D. Dissertation, University of Illinois at Urbana-Champaign.

[22] Mourad, J. [1988], Fragments of Arithmetic and the Foundations of the Priority Method. Ph.D. Dissertation, University of Chicago.

[23] Paris, J. B. [1980], A hierarchy of cuts in models of arithmetic. Model Theory of Algebra and Arithmetic, Lecture Notes in Math. 834, Springer, Berlin-New York, 312–337.

[24] Paris, J. B.; Kirby, L. A. S. [1978], Σ_{n}-collection schemas in arithmetic. Logic Colloquium ’77, Stud. Logic Foundations Math. 96, North-Holland, Amsterdam-New York, 199–209.

[25] Rosenstein, J. G. [1982], Linear Orderings. Pure Appl. Math. 98, Academic Press, New York etc.

[26] Seetapun, D.; Slaman, T. A. [1995], On the strength of Ramsey’s Theorem. Notre Dame J. Formal Logic 36, 570–582.

[27] Simpson, S. G. [1977], Degrees of unsolvability: a survey of results. Handbook of Mathematical Logic (Barwise, ed.), North-Holland, Amsterdam, 631–652.

[28] Simpson, S. G. [1999], Subsystems of Second Order Arithmetic. Perspect. Math. Logic, Springer-Verlag, Berlin.

[29] Simpson, S. G. and Yu, X. [1990], Measure theory and Weak König’s Lemma. Arch. Math. Logic 30, 171–180.

[30] Specker, E. [1971], Ramsey’s Theorem does not hold in recursive set theory. Logic Colloquium ’69, Stud. Logic Found. Math., North-Holland, Amsterdam.

[31] Szpilrajn, E. [1930], Sur l’extension de l’ordre partiel. Fund. Math. 16, 386–389.