2 Free sets, thin sets and rainbows

The main goal of this section is to recall the definitions of the usual finite-dimensional Free Set, Thin Set, and Rainbow Ramsey Theorem and motivate their generalizations to colorings of exactly $\omega $ -large sets in analogy to the case of Ramsey’s theorem.

Let us first fix some notation and recall the definition of these principles for colorings of finite subsets of fixed size. We denote by $\mathbb {N}$ the set of natural numbers and by $\mathbb {N}^+$ the set of positive natural numbers. For $X\subseteq \mathbb {N}$ and $n \in \mathbb {N}$ we denote by $[X]^{n}$ the set of all n-subsets of X. We denote by $[X]^{<\omega }$ the set of all finite subsets of X. We always assume that sets are presented in increasing order and make no distinction between a set and the sequence of its elements in increasing order. We write $x \cdot y$ for the concatenation of two sequences x and y. We identify a natural number with the set of its predecessors, so that, if $k\geq 1$ we can write $f: X \to k$ to declare a function from X to $\{0, 1, \dots , k-1\}$ . A function of this type is often called a coloring of X in k colors.

We start by recalling the classical Ramsey’s theorem for finite colorings of the n-subsets of a countable set.

Ramsey’s theorem was first studied in Computability Theory by Jockusch [Reference Jockusch18], who proved that every computable instance admits an arithmetical solution, and constructed a computable instance of $\mathsf {RT}^3_2$ such that every solution computes the halting set. The formalization of Jockusch’s proofs in Reverse Mathematics by Simpson [Reference Simpson33] yields that $\mathsf {RT}^1_k$ is provable over $\mathsf {RCA}_0$ for any standard $k \in \mathbb {N}^+$ , and $\mathsf {RT}^n_k$ is equivalent to $\mathsf {ACA}_0$ over $\mathsf {RCA}_0$ for $n \geq 3$ and any $k\geq 2$ . The case $n = 2$ was a long-standing open question, until Seetapun [Reference Seetapun and Slaman32] proved that no computable instance of $\mathsf {RT}^2_k$ codes the halting set, hence that $\mathsf {RT}^2_k$ is strictly weaker than $\mathsf {ACA}_0$ over $\mathsf {RCA}_0$ .

The following Free Set Theorem, and its weakening the Thin Set theorem, have been introduced by Harvey Friedman [Reference Friedman and Simpson13] and first studied in [Reference Cholak, Giusto, Hirst and Jockusch5].

The notion of free set in Friedman’s Free Set Theorem is the same as the one used in a combinatorial characterization theorem for the $\aleph _n$ cardinals by Kuratowski [Reference Kuratowski19]. Here, the following property of an $n+1$ -subset U of a set X with respect to a function $f:[X]^n \to [X]^{<\omega }$ is considered: for all $x\in U$ we have $x \notin f(U\setminus \{x\})$ . For the particular case of a function mapping in (singletons from) X this means that for all $x\in U$ we have $f(U\setminus \{x\}) \neq x$ . This is the same as asking that for any n-subset s of U, if $f(s) \in U$ then $f(s) \in s$ , which means that U is free for f. Interestingly, in §6 we are lead to consider extensions of the Free Set Theorem with colors in $[\mathbb {N}]^{<\omega }$ .

The next theorem is a weakening of the Free Set Theorem.

The notion of free set might seem ad-hoc at first sight, but can be better understood in the light of the Thin Set Theorem. Indeed, an infinite set $H \subseteq \mathbb {N}$ is f-free if and only if, for every $x \in H$ , the set $H \setminus \{x\}$ is f-thin with witness color x (in the sense that f never takes value x on $[H\setminus \{x\}]^n$ ). Thus, the Free Set Theorem is a natural generalization of the Thin Set Theorem. The next principle is sometimes called an anti-Ramsey theorem or the Rainbow Ramsey Theorem. We first need the following definition.

The principles $\mathsf {TS}^n, \mathsf {FS}^n,$ and $\mathsf {RRT}^n_k$ have been thoroughly investigated from the point of view of Computability Theory and Reverse Mathematics by a number of authors [Reference Cholak and Patey4, Reference Cholak, Giusto, Hirst and Jockusch5, Reference Liu and Patey22, Reference Patey28]. The general picture that emerged is that these principles are computationally and combinatorially very weak consequences of Ramsey’s theorem ( $\mathsf {RT}^n \to \mathsf {FS}^n \to \mathsf {TS}^n \wedge \mathsf {RRT}^n$ ): while $\mathsf {RT}^3$ codes the jump and implies $\mathsf {ACA}_0$ , Wang [Reference Wang35] showed that the Free Set, Thin Set, and Rainbow Ramsey theorems do not code the halting set and satisfy the so-called strong cone avoidance property, which entails that they do not imply $\mathsf {ACA}_0$ .

In the remainder of this section we observe that, similarly to the case of Ramsey’s theorem, the natural generalizations of the Free Set, Thin Set, and Rainbow Ramsey theorems to colorings of all finite subsets of $\mathbb {N}$ fail.

Let $\mathsf {FS}^{<\omega }$ be the following principle: For every coloring $f:[\mathbb {N}]^{<\omega } \to \mathbb {N}$ there exists an infinite free set. Analogously, let $\mathsf {TS}^{<\omega }$ be the following principle: for every coloring $f:[\mathbb {N}]^{<\omega } \to \mathbb {N}$ there exists an infinite thin set. Finally, let $\mathsf {RRT}^{<\omega }_k$ be the following statement: For all k-bounded coloring $f:[\mathbb {N}]^{<\omega } \to \mathbb {N}$ there exists an infinite set $H\subseteq \mathbb {N}$ such that f is injective on $[H]^{<\omega }$ (i.e., H is a rainbow for f).

Similarly to the finite dimensions case [Reference Cholak, Giusto, Hirst and Jockusch5], the Free Set Theorem for all finite sets implies the Thin Set Theorem for all finite sets. We formulate this fact in terms of reductions since the exact same argument applies to other principles of interest in this article. The observation that the proof of the next proposition (see proof Theorem 3.2 in [Reference Cholak, Giusto, Hirst and Jockusch5]) applies to barriers was one of the starting points of the present work.

As a corollary we obtain the following proposition.

We next show that the natural generalization of the Rainbow Ramsey Theorem to colorings of all finite subsets of the natural numbers fails. The proof features the notion of exactly $\omega $ -large set, which is central for the present article.

The $\omega $ -large sets are also known as relatively large sets in the literature. For an infinite $X\subseteq \mathbb {N}$ we denote by $[X]^{!\omega }$ the family of all exactly $\omega $ -large subsets of X. The family $[\mathbb {N}]^{!\omega }$ coincides with the famous Schreier barrier used in better quasi ordering theory and Banach Space Theory [Reference Todorcevic34].

3 Colorings of exactly $\omega $ -large sets

In this section, we introduce and prove the generalizations of the Free Set, Thin Set, and Rainbow Ramsey theorems to colorings of exactly $\omega $ -large sets. We also establish some basic implications and relations among those principles.

As mentioned, Ramsey’s theorem fails when generalized to the family of all finite sets. On the other hand, there exists a natural generalization of Ramsey’s theorem to some families of finite sets of unbounded size that is central for our investigation. The following is the generalization of Ramsey’s theorem to colorings of exactly $\omega $ -large sets, as a particular case of more general theorems by Pudlák and Rödl [Reference Pudlák and Rödl31] and by Farmaki and Negrepontis [Reference Farmaki and Negrepontis12]. Besides, it is a particular case of Nash-Williams’ generalization of Ramsey’s theorem to barriers, which in turn is a consequence of the Clopen Ramsey Theorem (see [Reference Simpson33]).

The classical Ramsey Theorem is a statement about cardinality, in the precise sense that $\mathsf {RT}^n_k$ proves over $\mathsf {RCA}_0$ the following stronger statement “For every infinite set $X \subseteq \mathbb {N}$ and every coloring $f : [X]^n \to k$ , there is an infinite f-homogeneous set $H \subseteq X$ .” Proposition 8.3.4 of [Reference Dzhafarov and Mummert11] gives the equivalence of this general version of Ramsey’s Theorem—denoted $\mathsf {General}$ - $\mathsf {RT}^n_k$ in [Reference Dzhafarov and Mummert11]—with $\mathsf {RT}^n_k$ both in terms of Weihrauch reductions and in terms of provability over $\mathsf {RCA}_0$ . The situation is more complex in the case of Large Ramsey Theorem, as there is no clear direct equivalence between $\mathsf {RT}^{!\omega }_k$ and its general version ensuring homogeneous sets in any countable subset of $\mathbb {N}$ . Nevertheless, the classical proof and the computability-theoretic bounds of Large Ramsey Theorem as defined in Definition 3.1 hold for the general version of the statement. Because of this, Large Ramsey Theorem can arguably be considered as a non-robust statement. A first solution, adopted by Carlucci and Zdanowski [Reference Carlucci and Zdanowski3], consisted in directly studying the theorem in its general formulation, where an instance is a pair $(X, f)$ with X an infinite subset of $\mathbb {N}$ and f a k-coloring of the exactly large subsets of X. However, making the domain part of the instance raises some issues when considering strong cone avoidance as we do in §6 for the Large Ramsey Theorem, since the domain can be chosen to be sparse enough to compute any hyperarithmetic set. We shall therefore adopt a different approach, and prove our lower bounds in terms of the weaker versions of our statements, while proving the cone avoidance results on a generalized version formulated in terms of barriers, that will be presented in §6. All these versions are equivalent over $\mathsf {RCA}_0$ to $\mathsf {ACA}_0^+$ , so either formulation can be chosen. The following theorem summarizes the known bounds on $\mathsf {RT}^{!\omega }_k$ .

It is quite natural to ask if the natural generalizations of the Free Set, Thin Set, and Rainbow Ramsey theorems to colorings of exactly $\omega $ -large sets hold. The following is the natural generalization of the Free Set Theorem to colorings of exactly $\omega $ -large sets.

There exists a direct combinatorial proof of $\mathsf {FS}^{!\omega }$ , as for the proof of $\mathsf {RT}^{!\omega }_k$ , involving countable applications of $\mathsf {RT}^n_k$ and $\mathsf {FS}^n$ for $n \in \mathbb {N}^+$ and a final application of $\mathsf {FS}^1$ . A computability-theoretic analysis of this proof yields a solution computable in the $\omega $ -jump of the instance. We rather establish $\mathsf {FS}^{!\omega }$ by reduction to $\mathsf {RT}^{!\omega }$ . The proof combines ideas from the proof of $\mathsf {FS}^n$ from $\mathsf {RT}^n_{2n+2}$ [Reference Cholak, Giusto, Hirst and Jockusch5, Theorem 5.2 and Corollary 5.3] and from the proof of Theorem 4.1 in [Reference Carlucci and Zdanowski3].

Proof. For $s = \{s_0, \dots , s_{s_0}\}$ an exactly $\omega $ -large set with $s_0> 0$ , and $s_0 < \dots < s_{s_0}$ define $s \ominus 1$ to be the following exactly $\omega $ -large set: $\{s_0 - 1,s_1 - 1, \dots , s_{s_0 - 1} - 1\}$ . The idea is to keep one degree of freedom: $s_{s_0}$ , as in the proof of Carlucci and Zdanowski [Reference Carlucci and Zdanowski3, Proposition 4.1].

Let $f : [\mathbb {N}]^{!\omega } \to \mathbb {N}$ be an instance of $\mathsf {FS}^{!\omega }$ . Consider the following function $g : [\mathbb {N}]^{!\omega } \to 2$ defined by induction. Note that the function g is called recursively on lexicographically smaller parameters, so the induction is well-defined since the lexicographic order is a well-order. For $s = \{s_0, \dots , s_{s_0}\}$ an exactly $\omega $ -large set:

$$ \begin{align*} g(s) = \begin{cases} 0 \hspace{1.5cm} \text{if } f(s \ominus 1) = s_i - 1\ \textit{for some } i < s_0 & \\ 1 - g(f(s \ominus 1) + 1, s_1, \dots, s_{f(s \ominus 1) + 1}) & \\ \hspace{1.7cm} \text{if } f(s \ominus 1) < s_0 - 1 \\ 1 - g(s_0, \dots, s_i, f(s \ominus 1) + 1, s_{i+2}, \dots, s_{s_0}) & \\ \hspace{1.7cm} \text{if } f(s \ominus 1) \in (s_i - 1, s_{i+1} - 1)\ \textit{for some } i < s_0 - 1 \\ 0 \hspace{1.5cm} \text{if } f(s \ominus 1) \in (s_{s_0 - 1} - 1, s_{s_0} - 1) \\ 1 \hspace{1.5cm} \text{otherwise } (\textit{if } f(s \ominus 1) \geq s_{s_0} ). \\ \end{cases} \end{align*} $$

Let $H = \{x_0, x_1, \dots \}\subseteq \mathbb {N}^+$ be an infinite g-homogeneous set as given by $\mathsf {RT}^{!\omega }_2$ . We claim that $H' = \{x_0 - 1, x_1 - 1, \dots \}$ is f-free. Consider some exactly $\omega $ -large set $\{s_0 - 1, \dots , s_{s_0 - 1} - 1\} \subseteq H'$ . Then $\{s_0, \dots , s_{s_0 - 1}\} \subseteq H$ . There are two cases:

Case 1. H is homogeneous for the color $0$ . Then, take $s_{s_0}$ to be the next element of H after $s_{s_0 - 1}$ and write $s = \{s_0, \dots , s_{s_0}\}$ , then $g(s) = 0$ . There are four subcases:

Subcase 1.1. $f(s \ominus 1) = s_i - 1$ for some $i < s_0$ . In that case we are done.

Subcase 1.2. $f(s \ominus 1) \in (s_{s_0 - 1} - 1, s_{s_0} - 1)$ . In that case, by definition of $s_{s_0}$ , $f(s \ominus 1)$ is not in $H'$ .

Subcase 1.3. $f(s \ominus 1) < s_0 - 1$ and $g(f(s \ominus 1) + 1, s_1, \dots , s_{f(s \ominus 1) + 1}) = 1$ . If $f(s \ominus 1) \in H'$ this contradicts the fact that H is g-homogeneous for the color  $0$ .

Subcase 1.4. $f(s \ominus 1) \in (s_i - 1, s_{i+1} - 1)$ for some $i < s_0 - 1$ and $g(s_0, \dots , s_i, f(s \ominus 1) + 1 ,s_{i+2}, \dots , s_{s_0}) = 1$ . If $f(s \ominus 1) \in H'$ this contradicts the fact that H is g-homogeneous for the color $0$ .

Case 2. H is homogeneous for the color $1$ . Take $s_{s_0} \in H$ bigger than $s_{s_0 - 1}$ and write $s = \{s_0, \dots , s_{s_0}\}$ , then $g(s) = 1$ . There are three subcases:

Subcase 2.1. $f(s \ominus 1) \geq s_{s_0}$ . This case is impossible, indeed, as H is infinite, there exists some element $x \in H$ such that $x> f(s \ominus 1) + 1$ and therefore $f(s \ominus 1) \in (s_{s_0} - 1, x - 1)$ , which leads to $g(s_0, \dots , s_{s_0 - 1}, x) = 0$ contradicting the fact that H is g-homogeneous for the color $1$ .

Subcase 2.2. $f(s \ominus 1) < s_0 - 1$ and $g(f(s \ominus 1) + 1, s_1, \dots , s_{f(s \ominus 1) + 1}) = 0$ . If $f(s \ominus 1) \in H'$ this contradicts the fact that H is g-homogeneous for the color $1$ .

Subcase 2.3. $f(s \ominus 1) \in (s_i - 1, s_{i+1} - 1)$ for some $i < s_0 - 1$ and $g(s_0, \dots , s_i, f(s \ominus 1) + 1 ,s_{i+2}, \dots , s_{s_0}) = 0$ . If $f(s \ominus 1) \in H'$ this contradicts the fact that H is g-homogeneous for the color $1$ .

Notice that g is uniformly computable in f and that $H'$ is uniformly computable in H. Therefore, $\mathsf {FS}^{!\omega } \leq _{\mathrm {sW}} \mathsf {RT}^{!\omega }_2$ .

The above proof uses the fact that the exactly $\omega $ -large sets are well-ordered under lexicographic ordering. Since the order type of this ordering is $\omega ^\omega $ and the statement “ $\omega ^\omega $ is well-ordered” implies the consistency of $\mathsf {RCA}_0$ (see [Reference Gentzen15, Reference Hájek and Pudlák16]), the above proof is not formalizable in $\mathsf {RCA}_0$ . Yet, since $\mathsf {RT}^{!\omega }_2$ implies $\mathsf {ACA}_0$ and the latter proves that $\omega ^\omega $ is well-ordered we obtain the following corollary.

We next introduce the generalization of the Thin Set Theorem to colorings of exactly $\omega $ -large sets. For the fixed-dimension case, Cholak et al. [Reference Cholak, Giusto, Hirst and Jockusch5] have proved in $\mathsf {RCA}_0$ that for all $k\geq 2$ , $\mathsf {FS}^k$ implies $\mathsf {TS}^k$ (see Theorem 3.2 in [Reference Cholak, Giusto, Hirst and Jockusch5]; the proof yields a strong Weihrauch reduction). A completely analogous argument establishes that the Thin Set Theorem follows from (and is reducible to) the Free Set Theorem for colorings of exactly $\omega $ -large sets.

The following proposition states that requiring that one color is omitted is equivalent to requiring that infinitely many colors are omitted. The result is the analogue of Theorem 3.5 in [Reference Cholak, Giusto, Hirst and Jockusch5] and can be proved by exactly the same proof.

We now turn to the generalization of the Rainbow Ramsey Theorem.

For the fixed dimension case, Galvin gave a reduction to Ramsey’s theorem. His argument is formalizable in $\mathsf {RCA}_0$ and yields that for each $n, k\in \mathbb {N}$ , $\mathsf {RRT}^n_k \leq _{\mathrm {sW}} \mathsf {RT}^n_k$ (see [Reference Csima and Mileti8, Theorem 5.2]). Csima and Mileti also showed that for each $n,k\in \mathbb {N}^+$ , $\mathsf {RRT}^n_k$ follows from $\mathsf {RRT}^{n+1}_k$ over $\mathsf {RCA}_0$ (the proof of Theorem 5.3 in [Reference Csima and Mileti8] yields a strong Weihrauch reduction).

We first observe that Galvin’s argument adapts to the case of colorings of exactly $\omega $ -large sets and establishes a strong Weihrauch reduction.

Proof. Let $f:[\mathbb {N}]^{!\omega } \to \mathbb {N}$ be k-bounded and fix a computable bijection $b(\cdot ): [\mathbb {N}]^{!\omega } \to \mathbb {N}$ . Define $g:[\mathbb {N}]^{!\omega } \to k$ as follows:

$$ \begin{align*}g(s) = |\{ t \in [\mathbb{N}]^{!\omega} \,:\, b(t) < b(s) \text{ and } f(s) = f(t)\}|.\end{align*} $$

The fact that g is a k-coloring depends on the hypothesis that f is k-bounded. Let H be an infinite set such that g is constant on $[H]^{!\omega }$ , as given by $\mathsf {RT}^{!\omega }_k$ . Let $s, t \in [H]^{!\omega }$ . Since $g(s) = g(t)$ and either $b(s) < b(t)$ or $b(t) < b(s)$ we have that $f(s) \neq f(t)$ . Thus, H is rainbow for f.

The following is an adaptation of a result by Wang [Reference Wang35], who showed that for every n, $\mathsf {RRT}^n_2 \leq _{\mathrm {sW}} \mathsf {FS}^n$ .

Proof. Fix a computable bijection $b: [\mathbb {N}]^{!\omega } \to \mathbb {N}$ . Let $f:[\mathbb {N}]^{!\omega }\to \mathbb {N}$ be $2$ -bounded. Define $g:[\mathbb {N}]^{!\omega } \to \mathbb {N}$ as follows:

$$ \begin{align*}g(s)= \begin{cases} \min(t\setminus s) & \mbox{ if there is a } t\in [\mathbb{N}]^{!\omega} \text{ such that } b(t)<b(s) \text{ and } f(s)=f(t),\\ 0 & \mbox{ otherwise.} \end{cases} \end{align*} $$

Since f is $2$ -bounded, if t exists in the definition of g then it is unique. If t and s are distinct exactly $\omega $ -large sets then $(t\setminus s)\neq \emptyset $ , since $t\subseteq s$ is impossible. Let A be an infinite g-free set. We claim that A is a rainbow for f. Suppose otherwise, by way of contradiction, as witnessed by $s, t \in [A]^{!\omega }$ such that $f(s) = f(t)$ . Without loss of generality we can assume $b(t) < b(s)$ . Then $g(s) = \min (t\setminus s) \in A \setminus s$ , contradicting that A is g-free.

Wang [Reference Wang35] proved that the Free Set, Thin Set, and Rainbow Ramsey theorems for fixed-sized sets satisfy cone-avoidance. This entails that none of these principles codes the halting set or implies $\mathsf {ACA}_0$ . A natural question is whether the same is true of their versions for exactly $\omega $ -large sets. We will show that $\mathsf {FS}^{!\omega }$ and $\mathsf {TS}^{!\omega }$ code $\emptyset ^{(\omega )}$ and imply the much stronger system $\mathsf {ACA}_0^+$ , while $\mathsf {RRT}^{!\omega }$ admits cone avoidance.

Some first lower bounds on our principles can be obtained by adapting results from the finite-dimensional case. For example, the Rainbow Ramsey Theorem with internal quantification over all fixed finite dimensions $\forall n \mathsf {RRT}^n_2$ follows from the Rainbow Ramsey Theorem for exactly $\omega $ -large sets.

Analogous results can be obtained for the Large Free Set and the Large Thin Set Theorem, so that $\mathsf {P}^{!\omega }$ implies $\forall n \mathsf {P}^n$ over $\mathsf {RCA}_0$ for $\mathsf {P}\in \{\mathsf {FS},\mathsf {TS}\}$ . Both implications are also witnessed by strong Weihrauch reductions. We omit the proofs since these results are superseded by the results of the next section where we prove that $\mathsf {FS}^{!\omega }$ and $\mathsf {TS}^{!\omega }$ imply $\mathsf {ACA}_0^+$ .

4 Large thin and free set theorems code $\emptyset ^{(\omega )}$

In this section we establish strong lower bounds on $\mathsf {FS}^{!\omega }$ and $\mathsf {TS}^{!\omega }$ showing that both these principles code $\emptyset ^{(\omega )}$ and imply $\mathsf {ACA}_0^+$ . This should be contrasted with the fact that neither $\forall n \mathsf {FS}^n$ nor $\forall n \mathsf {TS}^n$ imply $\mathsf {ACA}_0$ .

The first goal is to prove the existence of a computable instance of $\mathsf {TS}^{!\omega }$ such that every solution uniformly computes $\emptyset ^{(\omega )}$ . In particular, $\mathsf {TS}^{!\omega }$ admits the same lower bound as $\mathsf {RT}^{!\omega }_2$ . Since $\mathsf {TS}^{!\omega }$ is strongly Weihrauch reducible to $\mathsf {FS}^{!\omega }$ by Theorem 3.7, it follows that there is a computable instance of $\mathsf {FS}^{!\omega }$ such that every solution computes $\emptyset ^{(\omega )}$ . By results in the previous section, this bound is optimal, since every computable instance of $\mathsf {FS}^{!\omega }$ admits a solution computable in $\emptyset ^{(\omega )}$ by Theorem 3.4 and Theorem 3.2. The following definition of thinness is technically convenient.

The definition of f-thin set depends on the choice of codomain of the function. It will always be clear from the context.

The following version of the Thin Set Theorem for finite colorings was introduced in [Reference Dorais, Dzhafarov, Hirst, Mileti and Shafer9] and is useful for our purposes.

Dorais et al. [Reference Dorais, Dzhafarov, Hirst, Mileti and Shafer9, Proposition 5.5] proved the existence, for every $n \in \mathbb {N}^+$ , of a computable coloring $f : [\mathbb {N}]^{n+2} \to 2^n$ such that every infinite f-thin set computes $\emptyset '$ . However, their proof is not uniform, which is a required feature for our construction to code $\emptyset ^{(\omega )}$ . We prove the existence, for every $n \geq 2$ , of a computable coloring $f : [\mathbb {N}]^{n+1} \to n$ such that every infinite f-thin set uniformly computes $\emptyset '$ .

Combining these two lemmas, we get the following, where the array $(d_{n,k})_{n,k\in \mathbb {N}}$ is as in Theorem 4.3.

The following theorem states that $\mathsf {TS}^{!\omega }$ does not admit cone avoidance in a strong sense: there exists a single computable instance of $\mathsf {TS}^{!\omega }$ that computes $\emptyset ^{(\omega )}$ .

Since the proof of Theorem 4.6 relativizes and is formalizable in $\mathsf {RCA}_0$ we obtain the following Reverse Mathematics corollary.

The above corollary coupled with Theorem 3.2 and Corollary 3.5 implies the equivalence over $\mathsf {RCA}_0$ of $\mathsf {RT}^{!\omega }_2$ , $\mathsf {TS}^{!\omega }$ , and $\mathsf {FS}^{!\omega }$ . However, we do not know whether $\mathsf {RT}^{!\omega }_2$ is strongly Weihrauch-reducible to $\mathsf {TS}^{!\omega }$ or $\mathsf {FS}^{!\omega }$ .

The remaining question is whether $\mathsf {RRT}^{!\omega }$ codes $\emptyset ^{(\omega )}$ . In the next section, we shall answer this question negatively in a strong sense: $\mathsf {RRT}^{!\omega }$ does not code any non-computable set. Some computability-theoretic weak anti-basis results for $\mathsf {RRT}^{!\omega }$ can be obtained by streamlining results from the finite dimensional case. For instance, Csima and Mileti [Reference Csima and Mileti8] proved the following theorem:

The proof of Theorem 4.9 is uniform in n. Using this uniformity we obtain the following.

Proof. For each $n\geq 2$ let $f_n : [\mathbb {N}]^n \to \mathbb {N}$ be the $2$ -bounded instance of $\mathsf {RRT}^n_2$ with no infinite $\Sigma ^0_n$ rainbow given by Theorem 4.9. Let $g:[\mathbb {N}]^{!\omega } \to \mathbb {N}$ be defined as follows:

$$ \begin{align*}g(n, x_0, \dots, x_{n-1}) = \langle n, f_n(x_0, \dots, x_{n-1}) \rangle.\end{align*} $$

The function g is clearly $2$ -bounded since each $f_n$ is $2$ -bounded. Then for every g-rainbow H and every n in H, the set $H \setminus [0,n]$ is an $f_n$ -rainbow, so H is not $\Sigma ^0_n$ by Theorem 4.9.

Patey [Reference Patey27] proved that $\mathsf {RCA}_0 \vdash (\forall n)[\mathsf {RRT}^{n+1}_2 \to \mathsf {TS}^n]$ and for every $n \in \mathbb {N}^+$ , $\mathsf {RCA}_0 \vdash \mathsf {RRT}^{2n+1}_2 \to \mathsf {FS}^n$ . The argument almost translates in the exactly $\omega $ -largeness setting as follows. A set $s\subseteq \mathbb {N}$ is exactly $(\omega +1)$ -large if $s \setminus \{\min s\}$ is exactly $\omega $ -large. Let $\mathsf {RRT}^{!(\omega +1)}_2$ be the Rainbow Ramsey Theorem for $2$ -bounded colorings of the exactly $(\omega +1)$ -large sets.

5 Coloring barriers of order type $\omega ^\omega $

In the previous sections we established lower bounds showing that the Free Set Theorem and the Thin Set Theorem for the Schreier barrier code $\emptyset ^{(\omega )}$ . In this section we develop a more robust generalization of the principles of interest, based on the notion of barrier. The main motivation is to prove upper bounds on a generalization of the Large Rainbow Ramsey theorem.

Ramsey’s theorem for exactly $\omega $ -large sets ( $\mathsf {RT}^{!\omega }_k$ ) is arguably the simplest generalization of Ramsey’s theorem to collections of finite sets of arbitrary size, which is combinatorially true. However, the restriction $|s| = 1+\min s$ is somewhat arbitrary, and could be replaced by any restriction of the form $|s| = h(\min s)$ for a computable function $h : \mathbb {N} \to \mathbb {N}$ , while leaving the computational lower bounds and upper bounds of the statement unchanged. In this section, we therefore generalize the previous statements about exactly $\omega $ -large sets to a family of statements satisfying better closure properties.

There exist two possible approaches to relate $\mathsf {RT}^{!\omega }_k$ to existing theorems. The bottom-up approach, already explained, consists in considering $\mathsf {RT}^{!\omega }_k$ as a generalization of Ramsey’s theorem to larger families of finite sets. The top-down approach, which we explore now, consists in seeing $\mathsf {RT}^{!\omega }_k$ as a particular case of the clopen Ramsey Theorem by Galvin and Prikry [Reference Galvin and Prikry14]. In what follows, we write $[X]^\omega $ for the class of all infinite subsets of X. This notation should not be confused with the set $[X]^{!\omega }$ of all exactly $\omega $ -large subsets of X.

Every coloring $f : [\mathbb {N}]^{!\omega } \to k$ can be considered as a continuous coloring ${g : [\mathbb {N}]^\omega \to k}$ defined by $g(X) = f(X \upharpoonright _{1+\min X})$ , and every g-homogeneous set is f-homogeneous. On the other hand, given a continuous coloring $g : [\mathbb {N}]^\omega \to k$ , there exists a prefix-free set $B \subseteq [\mathbb {N}]^{<\omega }$ and a coloring $f : B \to k$ such that

1. (1) for every infinite set $X \in [\mathbb {N}]^\omega $ , there exists a (unique) $s_X \in B$ such that ${s_X \prec X}$ (where $\prec $ denotes proper initial segment);

2. (2) for every $X \in [\mathbb {N}]^\omega $ , $g(X) = f(s_X)$ .

Any set B satisfying the above properties is called a block. Marcone [Reference Marcone23] proved over $\mathsf {RCA}_0$ that such a set B can always be assumed to satisfy slightly stronger structural properties, making it something called a barrier. Given a set $B \subseteq [\mathbb {N}]^{<\omega }$ , we write $\operatorname {base}(B)$ for the set $\{ n \in \mathbb {N} : (\exists s \in B)(n \in s) \}$ . In the following definition $\preceq $ denotes the initial segment relation and $\subset $ denotes the proper subset relation.

Note that the last item is stronger than asking for B to be prefix-free. The simplest notions of barriers are the families $[\mathbb {N}]^n$ for $n \in \mathbb {N}$ . Barriers were introduced by Nash-Williams [Reference Nash-Williams25] in order to study better quasi-orders (bqo), a strengthening of well-quasi-orders (wqo) with better closure properties. Barriers were studied by Marcone [Reference Marcone23] in the context of Reverse Mathematics.

Marcone [Reference Marcone23] proved over $\mathsf {RCA}_0$ that the Barrier Ramsey Theorem is equivalent to $\mathsf {ATR}_0$ . Thus, the Barrier Ramsey Theorem is much stronger than Ramsey’s theorem for exactly $\omega $ -large sets, which stands at the level of $\mathsf {ACA}_0^+$ .

Barriers can be classified based on the order type of their lexicographic order. Given a barrier $B \subseteq [\mathbb {N}]^{<\omega }$ and $s, t \in B$ , let $s <_{\mathrm {lex}} t$ if $s(x) < t(x)$ for the least x such that $s(x) \neq t(x)$ , if it exists. Here, we identify s and t with finite increasing sequences over $\mathbb {N}$ . Note that since B is prefix-free, $<_{\mathrm {lex}}$ is total on B. The lexicographic orders are not in general well-orders, but Pouzet [Reference Pouzet30] proved that they are on barriers. Assous [Reference Assous1] characterized the order types of lexicographic orders on barriers, and proved that they are either of the form $\omega ^n$ for some $n \in \mathbb {N}^+$ , or $\omega ^\alpha \cdot k$ for some $\alpha \geq \omega $ and $k \in \mathbb {N}^+$ .

Clote [Reference Clote6] proved that the order type of barriers is relevant to the computability-theoretic analysis of the Barrier Ramsey Theorem, by conducting a level-wise analysis of its solutions in the hyperarithmetic hierarchy based on the order type of the barrier. He proved in particular the following theorem:

The Schreier barrier is a simple example of barrier of order type $\omega ^\omega $ . Carlucci and Zdanowski [Reference Carlucci and Zdanowski3] showed that the lower bound of Clote is witnessed by the Schreier barrier. Based on Clote’s analysis, it is natural to conjecture that the Free set, Thin set, and Rainbow Ramsey theorems for barriers of order type $\omega ^\omega $ are the robust counterpart of their versions for exactly $\omega $ -large sets. Actually, we shall see that, arguably, the right notion is the restriction of the statements to a sub-class of barriers of order type $\omega ^\omega $ .

Given a set X and $n \in \mathbb {N}$ , we write $[X]^{\leq n}$ for the set of all subsets $s \subseteq X$ such that $|s| \leq n$ , and $[X]^{\leq !\omega }$ for the set of all subsets $s \subseteq X$ such that $|s| \leq 1+\min s$ . By convention, for $n = 0$ , $[X]^{\leq n}$ is the singleton $\{\emptyset \}$ . Given a function $h : \mathbb {N} \to \mathbb {N}$ , we write $[X]^{\leq h(\cdot )}$ for the set of all finite $s \subseteq X$ such that $|s| \leq h(\min s)$ .

A function $h : \mathbb {N} \to \mathbb {N}$ is left-c.e. if there is a uniformly computable sequence of functions $h_0, h_1, \dots $ such that for every $x, i \in \mathbb {N}$ , $h_i(x) \leq h_{i+1}(x)$ and $\lim _i h_i(x) = h(x)$ . The sequence $(h_i)_{i\in \mathbb {N}}$ is then called a left-c.e. approximation of h. If B is a computable barrier of order type at most $\omega ^\omega $ , then it is $\omega $ -bounded by a left-c.e. function. This bound is tight, as there exist computable barriers of order type $\omega ^{\omega }$ which are not computably $\omega $ -bounded.

Let us first define a generalized version of Rainbow Ramsey Theorem for subsets of $[\mathbb {N}]^{<\omega }$ , and show that its restriction to computable barriers of order type $\omega ^\omega $ codes the jump.

In this article, we shall consider only sets $B\subseteq [\mathbb {N}]^{<\omega }$ , such that $\operatorname {base}(B) = \mathbb {N}$ .

As seen in Proposition 2.10, the statement $\mathsf {RRT}^B_k$ is not mathematically true for $B = [\mathbb {N}]^{<\omega }$ and $k\in \mathbb {N}$ . However, its restriction to barriers follows from Ramsey’s theorem for barriers (the proof is completely analogous to the proof of Theorem 3.10 above). Moreover, we shall see in §6 that $\mathsf {RRT}^B_k$ holds for every $\omega $ -bounded barrier $B \subseteq [\mathbb {N}]^{<\omega }$ .

The following proposition shows that $\mathsf {RRT}^B_2$ restricted to computable barriers of order type $\omega ^\omega $ codes the halting set.

We shall however see that for every computably $\omega $ -bounded barrier $B \subseteq [\mathbb {N}]^{<\omega }$ and every $k \in \mathbb {N}^+$ , $\mathsf {RRT}^B_k$ admits strong cone avoidance (see below). Note that the Schreier barrier is an example of a computable, computably $\omega $ -bounded barrier.

Because of this, Proposition 5.10 cannot be improved to code more than $\emptyset '$ . Indeed, every computable barrier of order type $\omega ^\omega $ is $\emptyset '$ -computably $\omega $ -bounded, so for any non- $\emptyset '$ -computable set D, every computable barrier of order type $\omega ^\omega $ , and every computable k-bounded function $f : B \to \mathbb {N}$ , there exists an infinite f-rainbow which does not compute D.

6 Large Rainbow Ramsey Theorem avoids cones

In this section, we prove that the Rainbow Ramsey theorem for computably $\omega $ -bounded barriers admits strong cone avoidance. In particular, this is the case for the Large Rainbow Ramsey theorem since the Schreier barrier is $\omega $ -bounded by the computable function $x \mapsto x + 1$ .

Note that in the previous definition, no computability constraint is given on the $\mathsf {P}$ -instance X. Thus, strong cone avoidance reflects the combinatorial weakness of $\mathsf {P}$ , in the sense that no matter how complex the instance is, it cannot code in its solutions an infinite binary sequence. We shall use the following two theorems:

Wang [Reference Wang35] introduced and studied the following formal theorem, which is strictly related to the Thin Set theorem.

Note that $\mathsf {RT}^n_{k,k-1}$ is the same as $\mathsf {TS}^n_k$ from Theorem 4.2.

The following sequence of numbers, known as Catalan numbers, is omnipresent in Combinatorics. It is inductively defined as follows:

$$ \begin{align*}C_0 = 1 \hspace{1cm} C_{n+1} = \sum_{i = 0}^n C_i C_{n-i}. \end{align*} $$

This sequence starts with $1, 1, 2, 5, 14, 42, \dots $ (see sequence A000108 in the OEIS). The number $C_n$ admits many characterizations, such as the number of ways of associating n applications of a binary operator. In computability theory, the nth Catalan number $C_n$ surprisingly arose as the exact threshold $\ell $ at which $\mathsf {RT}^n_{<\infty , \ell }$ admits strong cone avoidance.

In the remaining part of this section we show that the Rainbow Ramsey Theorem for computable, computably $\omega $ -bounded barriers admits strong cone avoidance and therefore does not code the jump. To obtain this result, we introduce some variants of the Free Set Theorem for large sets which are of interest in their own right. We first introduce the needed terminology.

For example, given a coloring $f : [\mathbb {N}]^n \to \mathbb {N}$ , one can let $B = [\mathbb {N}]^n$ and ${g : [\mathbb {N}]^n \to [\mathbb {N}]^{<\omega }}$ be defined by $g(s) = \{f(s)\}$ . Then a set is f-free if and only if it is g-free. Of course, even with $B = [\mathbb {N}]^n$ , infinite free sets do not necessarily exist for arbitrary colorings. We need to impose some constraints on the size of the sets in the image of f.

Given $n \in \mathbb {N}$ and a function $h : \mathbb {N} \to \mathbb {N}$ , we write $\mathsf {FS}^{\leq n}_k$ , $\mathsf {FS}^{\leq !\omega }_k$ , and $\mathsf {FS}^{\leq h(\cdot )}_k$ for $\mathsf {FS}^B_k$ when B is $[\mathbb {N}]^{\leq n}$ , $[\mathbb {N}]^{\leq !\omega }$ and $[\mathbb {N}]^{\leq h(\cdot )}$ , respectively. In the extreme case where $B = \{\emptyset \}$ , $\mathsf {FS}^B_k$ is nothing but the statement “For every finite set $F \in [\mathbb {N}]^{\leq k}$ , there is an infinite set $H \subseteq \mathbb {N}$ such that $H \cap F = \emptyset $ ”. We have seen in Corollary 4.7 that there exists a computable instance f of $\mathsf {FS}^{\leq !\omega }_1$ such that every infinite f-free set computes $\emptyset ^{(\omega )}$ . The case $n < \omega $ is different.

Note that the k-constraint cannot be released, even in the case of colorings of singletons, as it would yield a combinatorially false statement:

One can however replace the constant constraint by a function when considering a natural sub-class of instances.

An easy combinatorial argument shows that the following statement is classically true.

Here again, given $n \in \mathbb {N}$ and a function $h : \mathbb {N} \to \mathbb {N}$ , we write $\mathsf {PFS}^{\leq n}_b$ , $\mathsf {PFS}^{\leq !\omega }_b$ , and $\mathsf {PFS}^{\leq h(\cdot )}_b$ for $\mathsf {PFS}^B_b$ when B is $[\mathbb {N}]^{\leq n}$ , $[\mathbb {N}]^{\leq !\omega }$ , and $[\mathbb {N}]^{\leq h(\cdot )}$ , respectively. We now show how the above principle relates to the Generalized Rainbow Ramsey Theorem $\mathsf {RRT}^B$ .

The following proposition shows the existence of a computable barrier of order type $\omega ^\omega $ for which the Progressive Free Set theorem does not admit cone avoidance. In particular, this barrier is not computably $\omega $ -bounded, as we shall prove that the Progressive Free Set theorem for computable barriers which are computably $\omega $ -bounded admits strong cone avoidance.

We now proceed to establish that the $\mathsf {PFS}^{\leq h(\cdot )}_h$ admits strong cone avoidance for every computable function $h : \mathbb {N} \to \mathbb {N}$ . Note that h needs to be computable since by Proposition 6.13, letting h be the function such that $B \subseteq [\mathbb {N}]^{\leq h(\cdot )}$ , $\mathsf {PFS}^{\leq h(\cdot )}_1$ does not admit cone avoidance.

Proof. For simplicity, we prove the theorem in a non-relativized form. Relativization is straightforward. Fix a non-computable set D. Let $\mathcal {P}$ be the collection of all progressive colorings of type $[\mathbb {N}]^{\leq h(\cdot )} \to [\mathbb {N}]^{<\omega }$ . For a function $b:\mathbb {N}\to \mathbb {N}$ we write $\mathcal {P}_b$ for the class of all b-constrained colorings in $\mathcal {P}$ .

Given two colorings $f, g \in \mathcal {P}$ , we write $g \leq f$ if for every $s \in [\mathbb {N}]^{\leq h(\cdot )}$ , ${g(s) \supseteq f(s)}$ . Note that if H is g-free and $g \leq f$ , then H is f-free. Given two colorings $f, g \in \mathcal {P}$ , let $f \cup g$ be the coloring defined by $(f \cup g)(s) = f(s) \cup g(s)$ . The coloring $f \cup g$ is the greatest lower bound of f and g with respect to $\leq $ .

Consider the following notion of forcing:

Definition 6.15. A condition is a triple $(f, \sigma , X)$ such that $f \in \mathcal {P}$ is $b_f$ -constrained, for some computable function $b_f : \mathbb {N} \to \mathbb {N}$ , $\sigma \in [\mathbb {N}]^{<\omega }$ , $X \subseteq \mathbb {N}$ is an infinite set such that $\max \sigma < \min X$ , and

1. (a) for every $s \in [\sigma \cup X]^{\leq h(\cdot )}$ with $\min s \in \sigma $ , $f(s) \cap X \subseteq s$ ;

2. (b) for every $s \in [\sigma \cup X]^{\leq h(\cdot )}$ , $f(s) \cap \sigma \subseteq s$ ;

3. (c) $D \not \leq _T X$ .

A condition $d = (g, \tau , Y)$ extends $c = (f, \sigma , X)$ (written $d \leq c$ ) if $g \leq f$ , $\tau \succeq \sigma $ , $Y \subseteq X,$ and $\tau \setminus \sigma \subseteq X$ .

The following lemma states that property (a) can be obtained “for free”, that is, by restricting the reservoir, and therefore does not impose any constraint on the stem. In what follows, fix a coloring $f \in \mathcal {P}$ which is $b_f$ -constrained, for some computable function $b_f : \mathbb {N} \to \mathbb {N}$ .

Lemma 6.16. For every $\sigma \in [\mathbb {N}]^{<\omega }$ and every infinite set X such that $\max \sigma < \min X$ and $D \not \leq _T X$ , there is an infinite set $Y \subseteq X$ such that $D \not \leq _T Y$ and for every $s \in [\sigma \cup Y]^{\leq h(\cdot )}$ with $\min s \in \sigma $ , $f(s) \cap Y \subseteq s$ .

Proof. For every $t \in [\sigma ]^{\leq h(\cdot )}$ with $t \neq \emptyset $ , let $f_t : [X]^{\leq h(\min t) - |t|} \to [\mathbb {N}]^{\leq b_f(\min t)}$ be defined for every u by $f_t(u) = f(t \cdot u)$ . By finitely many successive applications of Proposition 6.8, there exists an infinite subset $Y \subseteq X$ such that $D \not \leq _T Y$ and such that Y is simultaneously $f_t$ -free for every $t \in [\sigma ]^{\leq h(\cdot )}$ with $t \neq \emptyset $ .

We claim that Y is our desired set. Indeed, for every $s \in [\sigma \cup Y]^{\leq h(\cdot )}$ with ${\min s \in \sigma} $ , letting $t = s \cap \sigma $ and $u = s \cap Y$ , we have $f(s) = f_t(u)$ , so by $f_t$ -freeness of Y, $f(s) = f_t(u) \cap Y \subseteq u \subseteq s$ .

In what follows, recall that $C_n$ stands for the nth Catalan number.

Definition 6.17. A set X stabilizes $\sigma $ if for every $t \in [\sigma ]^{\leq h(\cdot )}$ with $t \neq \emptyset $ and every $n \leq h(\min t) - |t|$ , there is a set $I_{t,n} \subseteq [\sigma ]^{\leq b_f(\min t) \times C_n}$ such that for every $u \in [X]^n$ , $f(t, u) \cap \sigma \subseteq I_{t, n}$ .

Lemma 6.18. For every $\sigma \in [\mathbb {N}]^{<\omega }$ and every infinite set X such that $\max \sigma < \min X$ and $D \not \leq _T X$ , there is an infinite set $Y \subseteq X$ stabilizing $\sigma $ such that $D \not \leq _T Y$ .

Proof. For every $t \in [\sigma ]^{\leq h(\cdot )}$ with $t \neq \emptyset $ and every $n \leq h(\min t) - |t|$ , let ${g_{t, n} : [X]^n \to [\sigma ]^{\leq b_f(\min t)}}$ be defined by $g_{t, n}(u) = f(t \cdot u) \cap \sigma $ . By finitely many successive applications of strong cone avoidance of $\mathsf {RT}^n_{<\infty , C_n}$ (see Cholak and Patey [Reference Cholak and Patey4]), there is an infinite subset $Y \subseteq X$ such that $D \not \leq _T Y$ and for every $t \in [\sigma ]^{\leq h(\cdot )}$ with $t \neq \emptyset $ and every $n \leq h(\min t) - |t|$ , $|g_{t, n}([Y]^n)| \leq C_n$ . Note that here, a color is an element of $[\sigma ]^{\leq b_f(\min t)}$ instead of a natural number. Let $I_{t, n} = \bigcup g_{t, n}([Y]^n)$ . Then $|I_{t, n}| \leq b_f(\min t) \times C_n$ . By definition, for every $u \in [Y]^n$ , $f(t \cdot u) \cap \sigma = g_{t, n}(u) \subseteq I_{t, n}$ .

Given a computable function $b : \mathbb {N} \to \mathbb {N}$ , let $b ^{+} : \mathbb {N} \to \mathbb {N}$ be the computable function defined by $b^{+}(m) = \sum _{n \leq h(m)} b(m) \times C_n$ .

Definition 6.19. Let X be a reservoir stabilizing $[0, k]$ . The limit coloring is the function $g_{k,X} : [k]^{\leq h(\cdot )} \to [k]^{<\omega }$ defined by $g_{k,X}(\emptyset ) = \emptyset $ and $g_{k,X}(t) = \bigcup _{n \leq h(t) - |t|} I_{t, n}$ otherwise.

The limit function $g_{k,X}$ is $b_f^{+}$ -constrained. Note that if $\rho \subseteq [0, k]$ is $g_{k,X}$ -free, then it is f-free. Indeed, for every $t \in [0, k]^{\leq h(\cdot )}$ , $g_{k,X}(t) = I_{t, 0}$ and by definition of stability for $n = 0$ , $f(t) \cap [0, k] \subseteq I_{t, 0}$ .

The following lemma is the core combinatorial lemma which specifies the conditions under which a block of elements $\rho $ can be added to the stem while preserving the property (b).

Lemma 6.20. Let $(f, \sigma , X)$ be a condition and $Y \subseteq X$ be an infinite set stabilizing $[0, k]$ for some $k \in \mathbb {N}$ and let $g_{k,Y} : [k]^{\leq h(\cdot )} \to [k]^{<\omega }$ be the limit coloring. Let $\rho \subseteq X \upharpoonright _k$ be a finite $g_{k,Y}$ -free set. Then $(f, \sigma \cup \rho , Y)$ satisfies property (b).

Proof. Fix some $s \in [\sigma \cup \rho \cup Y]^{\leq h(\cdot )}$ . We have multiple cases.

• • Case 1. $s \cap \sigma \neq \emptyset $ . Then by properties (a) and (b) of $(f, \sigma , X)$ , $f(s) \cap (\sigma \cup X) \subseteq s$ . Since $(\sigma \cup \rho ) \subseteq (\sigma \cup X)$ , then $f(s) \cap (\sigma \cup \rho ) \subseteq s$ .

• • Case 2. $s \cap \sigma = \emptyset $ but $s \cap \rho \neq \emptyset $ . By property (b) of $(f, \sigma , X)$ , $f(s) \cap \sigma \subseteq s$ . Let $t = s \cap \rho $ and $u = s \cap Y$ . Since $\rho $ is $g_{k,Y}$ -free, $g_{k,Y}(t) \cap \rho \subseteq t$ . By definition of $g_{k,Y}(t)$ , $I_{t, |u|} \subseteq g_{k,Y}(t)$ , so $I_{t, |u|} \cap \rho \subseteq t$ . In particular, $f(s) = f(t, u) \in I_{t, |u|}$ , so $f(s) \cap \rho \subseteq t \subseteq s$ . Thus, $f(s) \cap (\sigma \cup \rho ) \subseteq s$ .

• • Case 3. $s \cap (\sigma \cup \rho ) = \emptyset $ . Then $s \subseteq Y$ . Since $\min Y> \max (\sigma \cup \rho )$ , then by progressiveness of f, $f(s) \cap (\sigma \cup \rho ) = \emptyset $ .

One can combine Lemmas 6.16, 6.18, and 6.20 to obtain an extensibility lemma, saying that every sufficiently generic filter induces an infinite set.

Lemma 6.21. Let $(f, \sigma , X)$ be a condition. There is an extension $(f, \tau , Y) \leq (f, \sigma , X)$ such that $|\tau |> |\sigma |$ .

Proof. Let $x = \min X$ . By Lemma 6.18, there is an infinite subset $Y_0 \subseteq X$ stabilizing $[0, x]$ such that $D \not \leq _T Y_0$ . Let g be the limit function. By Lemma 6.16, there is an infinite subset $Y \subseteq Y_0$ such that $(f, \sigma \cup \{x\}, Y)$ satisfies property (a). By Lemma 6.20, $\{x\}$ being vacuously g-free, $(f, \sigma \cup \{x\}, Y)$ satisfies property (b). Thus, $(f, \sigma \cup \{x\}, Y)$ is a valid extension.

Given a computable function $b : \mathbb {N} \to \mathbb {N}$ , the space $\mathcal {P}_b$ is not compact. However, $\mathcal {P}_b$ is in one-to-one correspondence with the effectively compact space $\mathcal {R}_b$ of all relations $R \subseteq [\mathbb {N}]^{\leq h(\cdot )} \times \mathbb {N}$ such that for every $s \in [\mathbb {N}]^{\leq h(\cdot )}$ , $|\{ y : (s, y) \in R \}| \leq b(\min s)$ and for every $(s, y) \in R$ , $y \geq \min s$ . Indeed, given a function $g \in \mathcal {P}_b$ , one can define the relation $R_g \in \mathcal {R}_b$ defined by $R_g = \{ (s, y) : y \in g(s) \}$ and given a relation $R \in \mathcal {R}_b$ , the function $g_R \in \mathcal {P}_b$ is defined by $g_R(s) = \{ y : (s, y) \in R \}$ .

Note that the map $g \mapsto R_g$ is computable, but the map $R \mapsto g_R$ is not even continuous. Thankfully, there is a Turing functional which, given R and a finite set $\rho $ , decides whether $\rho $ is $g_R$ -free or not. Indeed, to decide whether $\rho $ is $g_R$ -free, one does not need to know $g_R$ restricted to $[\rho ]^{\leq h(\cdot )}$ , only to know R restricted to $[\rho ]^{\leq h(\cdot )} \times \rho $ .

We are now ready to define the forcing question:

Definition 6.22. Let $(f, \sigma , X)$ be a condition and $\varphi (G)$ be a $\Sigma ^0_1$ -formula. Let $(f, \sigma , X) \operatorname {{?}{\vdash }} \varphi (G)$ hold if and only if for every relation $R \in \mathcal {R}_{b_f^{+}}$ , there is a finite $g_R$ -free set $\rho \subseteq X$ such that $\varphi (\sigma \cup \rho )$ holds.

The previous formulation of the forcing question is $\Pi ^1_1(X)$ as it starts with a second-order universal quantification. However, thanks to the effective compactness of the space $\mathcal {R}_{b_f^{+}}$ , it is equivalent to a $\Sigma ^0_1(X)$ -formula:

Lemma 6.23. Let $(f, \sigma , X)$ be a condition and $\varphi (G)$ be a $\Sigma ^0_1$ -formula. Then $(f, \sigma , X) \operatorname {{?}{\vdash }} \varphi (G)$ if and only if there is some $k \in \omega $ such that for every $b_f^{+}$ -constrained progressive function $g : [0, k]^{\leq h(\cdot )} \to [0, k]^{<\omega }$ , there is a finite g-free set $\rho \subseteq X \upharpoonright _k$ such that $\varphi (\sigma \cup \rho )$ holds.

Proof. Suppose first that there is some $k \in \mathbb {N}$ such that for every $b_f^{+}$ -constrained progressive function $g : [0, k]^{\leq h(\cdot )} \to [0, k]^{<\omega }$ , there is a finite g-free set $\rho \subseteq X \upharpoonright _k$ such that $\varphi (\sigma \cup \rho )$ holds. Let $R \in \mathcal {R}_{b_f^+}$ be a relation, and let $g_R \in \mathcal {P}_{b_f^+}$ be the corresponding function. Then, letting $g : [0, k]^{\leq h(\cdot )} \to [0, k]^{<\omega }$ be defined by ${g(s) = g_R(s) \cap [0, k]}$ , the function g is $b_f^{+}$ -constrained and progressive, so there is some finite g-free set $\rho \subseteq X \upharpoonright _k$ such that $\varphi (\sigma \cup \rho )$ holds. In particular, $\rho $ is $g_R$ -free. Since there is such a $\rho $ for every $R \in \mathcal {R}_{b_f^+}$ , then $(f, \sigma , X) \operatorname {{?}{\vdash }} \varphi (G)$ holds.

Suppose now that for every $k \in \mathbb {N}$ , there is a $b_f^{+}$ -constrained progressive function $g_k : [0, k]^{\leq h(\cdot )} \to [0, k]^{<\omega }$ such that for every $g_k$ -free set $\rho \subseteq X \upharpoonright _k$ , $\varphi (\sigma \cup \rho )$ does not hold. Let $\mathcal {T}$ be the tree which, at level k, contains all such functions $g_k$ , and which is ordered by the function extension relation. The tree $\mathcal {T}$ is finitely branching, so by König’s lemma, there is an infinite path $g \in \mathcal {T}$ . This path is a function $g \in \mathcal {P}_{b_f^+}$ such that for every finite g-free set $\rho \subseteq X$ , $\varphi (\sigma \cup \rho )$ does not hold. Then the relation $R_g$ witnesses that $(f, \sigma , X) \operatorname {{?}{\vdash }} \varphi (G)$ does not hold.

Any filter $\mathcal {F}$ for this notion of forcing induces a set,

$$ \begin{align*}G_{\mathcal{F}} = \bigcup \{ \sigma : (g, \sigma, X) \in \mathcal{F} \}. \end{align*} $$

We say that a condition p forces a formula $\varphi (G)$ if $\varphi (G_{\mathcal {F}})$ holds for every sufficiently generic filter $\mathcal {F}$ containing p. The following lemma states that the forcing question meets its specification.

Lemma 6.24. Let $p = (f, \sigma , X)$ be a condition and $\varphi (G)$ be a $\Sigma ^0_1$ -formula.

1. 1. If $p \operatorname {{?}{\vdash }} \varphi (G)$ , then there is an extension of p forcing $\varphi (G)$ .

2. 2. If $p \operatorname {{?}{\nvdash }} \varphi (G)$ , then there is an extension of p forcing $\neg \varphi (G)$ .

Proof. Suppose first $p \operatorname {{?}{\vdash }} \varphi (G)$ holds. By Lemma 6.23, there is some $k \in \mathbb {N}$ such that for every $b_f^{+}$ -constrained progressive function $g : [0, k]^{\leq h(\cdot )} \to [0, k]^{<\omega }$ , there is a finite g-free set $\rho \subseteq X$ such that $\varphi (\sigma \cup \rho )$ holds. By Lemma 6.18, there is an infinite subset $Y_0 \subseteq X$ stabilizing $[0, k]$ and such that $D \not \leq _T Y_0$ . Let $g_{k,Y_0} : [0, k]^{\leq h(\cdot )} \to [0, k]^{<\omega }$ be the limit function. Note that $g_{k,Y_0}$ is $b_f^{+}$ -constrained and progressive, so there is a finite $g_{k,Y_0}$ -free set $\rho \subseteq X$ such that $\varphi (\sigma \cup \rho )$ holds. By Lemma 6.20, $(f, \sigma \cup \rho , Y_0)$ satisfies (b). By Lemma 6.16, there is an infinite subset $Y \subseteq Y_0$ such that $(f, \sigma \cup \rho , Y)$ satisfies (a) and $D \not \leq _T Y$ . Thus, $(f, \sigma \cup \rho , Y)$ is a valid extension of p. By choice of $\rho $ , it forces $\varphi (G)$ .

Suppose $p \operatorname {{?}{\nvdash }} \varphi (G)$ holds. Then there is a relation $R \in \mathcal {R}_{b_f^{+}}$ such that for every finite $g_R$ -free set $\rho \subseteq X$ , $\varphi (\sigma \cup \rho )$ does not hold. Let $g_R \in \mathcal {P}_{b_f^{+}}$ be the corresponding function. Let $\hat {f} : [\mathbb {N}]^{\leq h(\cdot )} \to [\mathbb {N}]^{<\omega }$ be defined by $\hat {f}(s) = f(s) \cup (g_R(s) \setminus \sigma )$ . Note that $\hat {f} \leq f$ , and every $\hat {f}$ -free subset $\rho \subseteq X$ is $g_R$ -free. Moreover, $\hat {f}$ is $(b_f + b_f^{+})$ -constrained and progressive. Since $(f, \sigma , X)$ satisfies (b) and for every $s \in [\sigma \cup X]^{\leq h(\cdot )}$ , $\hat {f}(s)\cap \sigma \subseteq f(s)\cap \sigma \subseteq s$ , then $(\hat {f}, \sigma , X)$ satisfies (b). By Lemma 6.16, there is an infinite subset $Y \subseteq X$ such that $D \not \leq _T Y$ and $(\hat {f}, \sigma , Y)$ satisfies (a). Thus, $q = (\hat {f}, \sigma , Y)$ is a valid extension of p.

We claim that q forces $\neg \varphi (G)$ . Indeed, suppose there is an extension $(\tilde {f}, \tau , Z) \leq q$ such that $\varphi (\tau )$ holds. Then by property (b) of $(\tilde {f}, \tau , Z)$ , $\tau $ is $\tilde {f}$ -free, and since $\tilde {f} \leq \hat {f}$ , $\tau $ is $\hat {f}$ -free. Let $\rho = \tau \setminus \sigma $ . By definition of $\hat {f}$ , $\rho $ is a $g_R$ -free subset of X, contradicting our choice of $g_R$ .

We can now prove our diagonalization lemma.

Lemma 6.25. Let $p = (f, \sigma , X)$ be a condition and $\Phi _e$ be a Turing functional. There is an extension of p forcing $\Phi _e^G \neq D$ .

Proof. Let $U = \{ (x, v) \in \mathbb {N} \times 2 : p \operatorname {{?}{\vdash }} \Phi ^G_e(x) \downarrow = v \}$ . We have three cases:

• • Case 1. $(x, 1-D(x)) \in U$ for some $x \in \mathbb {N}$ . By Lemma 6.24, there is an extension of p forcing $\Phi ^G_e(x)\downarrow = 1-D(x)$ , hence forcing $\Phi _e^G \neq D$ .

• • Case 2. $(x, D(x)) \not \in U$ for some $x \in \mathbb {N}$ . By Lemma 6.24, there is an extension of p forcing $\neg (\Phi ^G_e(x)\downarrow = D(x))$ , hence forcing $\Phi _e^G \neq D$ .

• • Case 3. U is the graph of the characteristic function of D. By Lemma 6.23, the set U is $\Sigma ^0_1(X)$ , so $D \leq _T X$ , contradiction.

We are now ready to prove Theorem 6.14. Let $f : [\mathbb {N}]^{\leq h(\cdot )} \to [\mathbb {N}]^{<\omega }$ be an h-constrained, progressive coloring, for a computable function $h : \mathbb {N} \to \mathbb {N}$ . Let $\mathcal {F}$ be a sufficiently generic filter containing $(f, \emptyset , \mathbb {N})$ , and let $G_{\mathcal {F}} = \bigcup \{ \sigma : (g, \sigma , X) \in \mathcal {F} \}$ . By definition of a forcing condition, $G_{\mathcal {F}}$ is f-free. By Lemma 6.21, $G_{\mathcal {F}}$ is infinite, and by Lemma 6.25, $D \not \leq _T G_{\mathcal {F}}$ . This completes the proof of Theorem 6.14.