Benoit Monin

Ludovic Patey

PIGEONS DO NOT JUMP HIGH

Introduction

The infinite pigeonhole principle asserts the existence, for any k-partition of the integers, of an infinite subset of one of the parts. In particular, the pigeonhole principle for 2-partitions asserts that, for every set A, there is an infinite subset of A or of A. The pigeonhole principle can be seen as a mathematical problem, with instances and solutions. An instance is a kpartition of the integers, and a solution to an instance is an infinite subset of one of the parts. In this paper, we conduct a computability-theoretic study of the pigeonhole principle seen as a problem. More precisely, given an arbitrary instance of the pigeonhole principle, we show the existence of a "weak" solution, for various computability-theoretic notions of weakness. Our main motivation is reverse mathematics.

Reverse mathematics and Ramsey's theorem

Reverse mathematics is a foundational program which seeks to determine the optimal axioms to prove ordinary theorems. It uses the framework of second-order arithmetics, with a base theory, RCA 0 , capturing "computable mathematics". The early study of reverse mathematics revealed the existence of four linearly ordered big systems WKL, ACA, ATR, and Π 1 1 CA (in increasing order), such that, given an ordinary theorem, it is very likely either to be provable in RCA 0 , or provably equivalent to one of the four systems in RCA 0 . These systems together with RCA 0 are known as the "Big Five". Among them, WKL stands for "weak König's lemma", and asserts that every infinite binary tree admits an infinite path, while ACA is the comprehension axiom restricted to arithmetical formulas. WKL can be thought of as capturing compactness arguments, and ACA is equivalent to the existence, for every set X, of the halting set relative to X. See Simpson [START_REF] Stephen | Subsystems of Second Order Arithmetic[END_REF] for an introduction to reverse mathematics.

Among the theorems studied in reverse mathematics, Ramsey's theorem received a special attention from the community, since Ramsey's theorem for pairs historically was the first theorem known to escape the Big Five phenomenon. Given a set of integers X, [X] n denotes the set of all n-tuples over X. For a coloring f :

[ω] n → k, a set of integers H is homogeneous if f is constant over [H] n .
Statement (Ramsey's theorem). RT n k : "Every k-coloring of [ω] n admits an infinite homogeneous set".

In particular, RT 1 k is the infinite pigeonhole principle for k-partitions. Ramsey's theorem and its consequences are notoriously hard to analyse from a computability-theoretic viewpoint. Jockusch [START_REF] Carl | Ramsey's theorem and recursion theory[END_REF] proved that RT n k is equivalent to ACA whenever n ≥ 3, thereby showing that RT n k satisfies the Big Five phenomenon. The question whether RT 2 k implies ACA was a longstanding open question, until Seetapun [START_REF] Seetapun | On the strength of Ramsey's theorem[END_REF] proved that RT 2 k is strictly weaker than ACA. Later, Jockusch [START_REF] Carl | Ramsey's theorem and recursion theory[END_REF][START_REF] Jockusch | Π 0 1 classes and degrees of theories[END_REF] and Liu [START_REF] Liu | RT 2 2 does not imply WKL0[END_REF] showed that RT 2 k is incomparable with WKL, and therefore that Question 1.1. Is every ω-model of D 2 2 a model of RT 2 2 ? This question is equivalent to asking whether every ω-model of D 2 2 is a model of COH. A particular way to prove such an implication would be, given a sequence of sets R 0 , R 1 , . . . , to construct a ∆ 0, R 2 set A such that every infinite subset of A or A computes relative to R a cohesive set for R. Among the instances of COH, the sequence of primitive recursive sets R is maximally difficult, in that for every computable sequence of sets S, every cohesive set for R computes a cohesive set for S. The sets cohesive for the sequence of primitive recursive sets are called p-cohesive. Jockusch and Stephan [START_REF] Jockusch | A cohesive set which is not high[END_REF] studied the p-cohesive degrees, and proved that these are the precisely the degrees whose Turing jump is PA over ∅ . The following question is therefore of particular interest. Question 1.2. Is there a ∆ 0 2 set A such that for every infinite set H ⊆ A or H ⊆ A, the jump of H is PA over ∅ ? A degree d is high if d ≥ 0 . A particular way to answer positively the previous question would be by proving that there is a ∆ 0 2 set A whose solutions are of high degrees. However, Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF] proved that given a non-∆ 0 2 set C, every ∆ 0 2 set admits an infinite subset H of it or its complement such that C is not ∆ 0,H 2 . In particular, we can always obtain a solution H of non-high degree.

By an empirical observation, many proofs of the existence of "weak" solutions for ∆ 0 2 instances of the pigeonhole principle are actually proofs of such an existence for arbitrary (even non-∆ 0 2 ) instances of the pigeonhole principle. For instance, Dzhafarov and Jockusch [START_REF] Damir | Ramsey's theorem and cone avoidance[END_REF] proved the existence, for every set A and every non-computable set C, of a solution to A, that is, an infinite subset of A, which does not compute C. Liu [START_REF] Liu | RT 2 2 does not imply WKL0[END_REF] proved the existence of a solution of non-PA degree, and more generally of solutions computing no enumeration of a closed set in the Cantor space [START_REF] Liu | Cone avoiding closed sets[END_REF]. The second author [START_REF] Patey | The reverse mathematics of Ramsey-type theorems[END_REF] proved the existence, for every set A and every hyperimmune function f , of a solution H to A such that f is H-hyperimmune, where a function f is H-hyperimmune if it is not dominated by any H-computable function. This observation could provide a partial answer to the difficulty of answering Question 1.2. Maybe there exists a (non-necessarily ∆ 0 2 ) set A such that every solution has a jump of PA degree over ∅ , or even of high degree. Then, any answer to Question 1.2 would necessarily rely on ∆ 0 2 approximations of the set A. This motivates our first main theorem:

Theorem 1.3 Every set A has an infinite subset H ⊆ A or H ⊆ A of non-high degree.
This theorem can be taken as a further evidence towards the intuition that Question 1.2 does not depend on the ∆ 0 2 definability of the set A. Note that by an observation of the second author [START_REF] Patey | Open questions about Ramsey-type statements in reverse mathematics[END_REF], a negative answer to Question 1.2 for non-∆ 0 2 sets would have consequences on other statements studied in reverse mathematics, notably the increasing polarized Ramsey theorem for pairs (IPT 2 2 ) introduced by Dzhafarov and Hirst [START_REF] Damir | The polarized Ramsey's theorem[END_REF].

The hierarchies in reverse mathematics

The computability-theoretic study of the pigeonhole principle is also motivated by questions on the strictness of hierarchies in reverse mathematics. Many consequences of Ramsey's theorem form hierarchies of statements, parameterized by the size of the colored tuples. A first example is Ramsey's theorem itself. Indeed, RT n+1 k implies RT n k for every n, k ≥ 1. By the work of Jockusch [START_REF] Carl | Ramsey's theorem and recursion theory[END_REF], this hierarchy collapses starting from the triples, and by Seetapun [START_REF] Seetapun | On the strength of Ramsey's theorem[END_REF], Ramsey's theorem for pairs is strictly weaker than Ramsey's theorem for triples. We therefore have

RT 1 k < RT 2 k < RT 3 k = RT 4 k = .
. . Friedman [START_REF] Harvey | Fom:53:free sets and reverse math and fom:54:recursion theory and dynamics[END_REF] introduced the free set and thin set theorems in reverse mathematics, while Csima and Mileti [START_REF] Csima | The strength of the rainbow Ramsey theorem[END_REF] introduced and studied the rainbow Ramsey theorem. A coloring f :

[ω] n → ω is k-bounded if each color occurs at most k times. An infinite set of integers H is thin for f if f omits at least one color over [H] n . We say that H is free for f if for every x ∈ H, H {x} is thin for f . Last, H is a rainbow for f if each color occurs at most once on [H] n .

Statement (Free set theorem). FS n : "Every coloring of [ω] n admits an infinite free set".

Statement (Thin set theorem). TS n : "Every coloring of [ω] n admits an infinite thin set".

Statement (Rainbow Ramsey theorem). RRT n k : "Every k-bounded coloring of [ω] n admits an infinite rainbow".

The reverse mathematics of these statements were extensively studied in the literature [START_REF] Cholak | Free sets and reverse mathematics[END_REF][START_REF] Csima | The strength of the rainbow Ramsey theorem[END_REF][START_REF] Kang | Combinatorial principles between RRT 2 2 and RT 2 2[END_REF][START_REF] Patey | Combinatorial weaknesses of Ramseyan principles[END_REF][START_REF] Patey | Somewhere over the rainbow Ramsey theorem for pairs[END_REF][START_REF] Patey | The weakness of being cohesive, thin or free in reverse mathematics[END_REF][START_REF] Rice | Thin set for pairs implies DNR[END_REF][START_REF] Wang | Some reverse mathematics of rainbow Ramsey theorems[END_REF][START_REF] Wang | Rainbow Ramsey theorem for triples is strictly weaker than the arithmetical comprehension axiom[END_REF][START_REF] Wang | Cohesive sets and rainbows[END_REF][START_REF] Wang | The definability strength of combinatorial principles[END_REF][START_REF] Wang | Some logically weak Ramseyan theorems[END_REF]. In particular, these theorems form hierarchies which are not known to be strictly increasing over RCA 0 . Question 1.4. Are the hierarchies of the free set, thin set, and rainbow Ramsey theorem strictly increasing? Partial results were however obtained. All these statements admit lower bounds of the form "For every n ≥ 2, there is a computable instance of P n with no Σ 0 n solution", where P n denotes any of RT n k (Jocksuch [START_REF] Carl | Ramsey's theorem and recursion theory[END_REF]), RRT n k (Csima and Mileti [6]), FS n , or TS n (Cholak, Giusto, Hirst and Jockusch [START_REF] Cholak | Free sets and reverse mathematics[END_REF]). From the upper bound viewpoint, all these statements follow from Ramsey's theorem. Therefore, by Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF], every computable instance of P 1 admits a computable solution, and every computable instance of P 2 admits a low 2 solution. These results are sufficient to show that P 1 < P 2 < P 3 in reverse mathematics. This upper bound becomes too coarse at triples, since RT 3 2 is equivalent to ACA, while Wang [START_REF] Wang | Some logically weak Ramseyan theorems[END_REF] surprisingly proved that P n is strictly weaker than ACA for every n and P n among FS n , TS n , and RRT n k . In particular, Wang [START_REF] Wang | Cohesive sets and rainbows[END_REF] proved that every computable instance of RRT 3 k admits a low 3 solution. The following question is still open. A positive answer would also answer positively Question 1.4. Question 1.5. Does every computable instance of FS n , TS n , and RRT n k admit a low n solution?

The known techniques to prove upper bounds to FS n , TS n , and RRT n k , are done by forcing with an inductive argument. This is in particular the case to prove that FS n , TS n and RRT n k does not imply ACA (Wang [START_REF] Wang | Some logically weak Ramseyan theorems[END_REF]), WKL (Patey [START_REF] Patey | Combinatorial weaknesses of Ramseyan principles[END_REF]), and preserve multiple hyperimmunities (Patey [START_REF] Patey | Iterative forcing and hyperimmunity in reverse mathematics[END_REF]) for every n. The techniques are all obtained by proving the result for arbitrary instances of the pigeonhole principle, and then generalizing to other hierarchies by an inductive argument. In this paper, we therefore prove the following theorem, which introduces the machinery that hopefully will serve to answer positively Question 1.5. This gives a partial answer to a question of Wang [33, Questions 6.1 and 6.2] and the second author [START_REF] Patey | Open questions about Ramsey-type statements in reverse mathematics[END_REF]Question 5.4] for the case n = 3.

Definitions and notation

A binary string is an ordered tuple of bits a 0 , . . . , a n-1 ∈ {0, 1}. The empty string is written . A binary sequence (or real) is an infinite listing of bits a 0 , a 1 , . . . . Given s ∈ ω, 2 s is the set of binary strings of length s and 2 <s is the set of binary strings of length < s. As well, 2 <ω is the set of binary strings and 2 ω is the set of binary sequences. Given a string σ ∈ 2 <ω , we use |σ| to denote its length. Given two strings σ, τ ∈ 2 <ω , σ is a prefix of τ (written σ τ ) if there exists a string ρ ∈ 2 <ω such that σρ = τ . Given a sequence X, we write σ ≺ X if σ = X n for some n ∈ ω. A binary string σ can be interpreted as a finite set F σ = {x < |σ| : σ(x) = 1}. We write σ ⊆ τ for F σ ⊆ F τ . We write #σ for the size of F σ .

A binary tree is a set of binary strings T ⊆ 2 <ω which is closed downward under the prefix relation. A path through T is an binary sequence P ∈ 2 ω such that every initial segment belongs to T .

A Turing ideal I is a collection of sets which is closed downward under the Turing reduction and closed under the effective join, that is, (∀X ∈ I)(∀Y ≤ T X)Y ∈ I and (∀X, Y ∈ I)X ⊕ T ∈ I, where X ⊕ Y = {2n : n ∈ X} ∪ {2n + 1 : n ∈ Y }. A Scott set is a Turing ideal I such that every infinite binary tree T ∈ I has a path in I. In other words, a Scott set is the secondorder part of an ω-model of RCA 0 + WKL. A Turing ideal M is countable coded by a set

X if M = {X n : n ∈ ω} with X = n X n . A formula is Σ 0 1 (M) (resp. Π 0 1 (M)) if it is Σ 0 1 (X) (resp. Π 0 1 (X)) for some X ∈ M.
Given two sets A and B, we denote by A < B the formula (∀x

∈ A)(∀y ∈ B)[x < y]. We write A ⊆ * B to mean that A -B is finite, that is, (∃n)(∀a ∈ A)(a ∈ B → a < n). A k-cover of a set X is a sequence of sets Y 0 , . . . , Y k-1 such that X ⊆ Y 0 ∪ • • • ∪ Y k-1 .

Main concepts

The main contribution of this paper is a new notion of forcing enabling a finer analysis of the computability-theoretic aspects of the infinite pigeonhole principle. All the theorems obtained in Section 4 are direct applications of this notion of forcing by taking a sufficiently generic filter, or by an effectivization of the construction of a filter. In order to give a better grasp on the notion of forcing, we focus in this section on some essential features of its design.

Forcing question

In computability theory, forcing is often specified by a partial order (P, ≤) of conditions. Each condition c ∈ P is given an interpretation

[c] ⊆ 2 ω , such that [d] ⊆ [c] whenever d ≤ c.
Informally, c can be seen as a partial approximation of the object we construct, and [c] denotes the set of all possible objects which satisfy this partial approximation. Then, every filter F induces a collection of sets [F] = c∈F [c]. Any set G ∈ [F] is called a generic set. Whenever the filter F is sufficiently generic, [F] is often a singleton {G}, in which case the generic set is uniquely determined.

Such notions of forcing induce a forcing relation c ϕ(G) defined over conditions c ∈ P and arithmetical formulas with one formal set parameter ϕ(G). In particular, c ϕ(G) for a ∆ 0 formula if ϕ(G) holds for every set G ∈ [c]. The relation is defined inductively for more complex formulas, so that it satisfies the following main lemma: Lemma 2.1 For every sufficiently generic filter F, every set G ∈ [F] and every arithmetical formula ϕ(G), ϕ(G) holds if and only if c ϕ(G) for some condition c ∈ F.

The computability-theoretic properties of the generic sets are strongly related to the existence, for every condition c ∈ P, of a Σ 0 n -definable relation c ? ϕ(G) over Σ 0 n formulas ϕ(G) which satisfies the following properties:

(∃d ≤ c)d ϕ(G).
In the case of Cohen forcing, that is, forcing over binary strings with the suffix relation, the default forcing question has the good definitional properties, that is, deciding a Σ 0 n formula is Σ 0 n . However, for many other notions of forcing, this forcing question is definitionally too complex, and one has to define custom forcing relations and forcing questions, to have the desired complexity.

For instance, consider the notion of forcing (P, ≤) whose conditions are infinite computable binary trees, and such that S ≤ T if S ⊆ T . The interpretation of T is the collection [T ] of its paths. We can define a forcing relation for Σ 0 1 and Π 0 1 formulas as follows. Definition 2.3. Let ψ(G, x) be a ∆ 0 0 formula, and

T ∈ P. (a) T (∃x)ψ(G, x) if there is some ∈ ω such that for every σ ∈ T with |σ| = , ψ(σ, w)
holds for some w < . (b) T (∀x)ψ(G, x) if for every σ ∈ T and every w < |σ|, ψ(σ, w) holds.

First, note that if T ϕ(G) where ϕ(G) is Σ 0 1 or Π 0 1 , then ϕ(G) will hold for every filter F containing T , and every generic set G for this filter. Then, define T ? (∃x)ψ(G, x) to hold if and only if T (∃x)ψ(G, x). Let's assume that the formula ψ(G, x) is continuous, that is, if ψ(σ, w) holds and σ ≺ τ , then ψ(τ, w) holds. If T ? (∃x)ψ(G, x), then T (∃x)ψ(G, x) by definition. If T ? (∃x)ψ(G, x), then the set S = {σ ∈ T : (∀w < |σ|)¬ψ(σ, w)} is an infinite subtree of T such that S (∀x)¬ψ(G, x). Note that T ? (∃x)ψ(G, x) is a Σ 0 1 formula, which satisfies Lemma 2.2.

Having a forcing question whose definition has the same complexity as the formula it decides, yields a few preservation properties for free. Let (P, ≤) be a notion of forcing such that the relation c ? ϕ(G) is uniformly Σ 0 n whenever ϕ(G) is Σ 0 n , and satisfies Lemma 2.1 and Lemma 2.2. The following lemma holds. Lemma 2.4 For every non-Σ 0 n set C, and every Σ 0 n formula ϕ(G, x), the following set is dense in (P, ≤).

D = {c ∈ P : (∃w ∈ C)c ϕ(G, w) ∨ (∃w ∈ C)c ¬ϕ(G, w)} Proof. Fix a condition c ∈ P. Let W = {w ∈ ω : c ? ϕ(G, w)}. By assumption, the set W is Σ 0 n , while C is not. Let w ∈ W ∆C = (W C) ∪ (C W ). If w ∈ W C, then c ? ϕ(G, w), so by Lemma 2.2(a), there is some d ≤ c such that d ϕ(G, w). If w ∈ C W , then c ? ϕ(G, w), so by Lemma 2.2(b), there is some d ≤ c such that d ¬ϕ(G, w). In both cases, d belongs to D.
Then, for every sufficiently generic set G, C will not be Σ 0,G n . This is the notion of preservation of non-Σ 0 n definitions, introduced by Wang [START_REF] Wang | The definability strength of combinatorial principles[END_REF]. In particular, if some set C is not ∆ 0 n , then either C or C is not Σ 0 n , so by the same reasoning, C will not be ∆ 0,G n for every sufficiently generic set G.

In many cases, the forcing question is compact in the following sense:

Definition 2.5. A forcing question ? is compact if for every c ∈ P and every formula ψ(G, x), c ? (∃x)ψ(G, x) if and only if there is a finite set U such that c ? (∃x ∈ U )ψ(G, x).

In particular, the forcing question for Cohen forcing and for the notion of forcing with computable binary trees is compact (see Wang [START_REF] Wang | The definability strength of combinatorial principles[END_REF]Section 3.2] for a definition of the forcing with computable binary trees). This yields other preservation properties for free. A function g dominates a function f if g(x) ≥ f (x) for every x ∈ ω. Given a set X, a function f is X-hyperimmune if is not dominated by any X-computable function. Let (P, ≤) be a notion of forcing with a compact forcing question satisfying the previous properties. The following lemma holds. Lemma 2.6 For every n, every ∅ (n) -hyperimmune function f and every Turing functional Φ e , the following set is dense in (P, ≤).

D = {c ∈ P : (∃w)c Φ G (n) e (w) ↑ ∨(∃w)c Φ G (n) e (w) < f (w)}
Proof. Fix a condition c ∈ P. Let g be the partial ∅ (n) -computable function which on input w, searches for a finite set U such that c ? (∃x ∈ U )Φ G (n) e (w)↓ = x. It it finds such a set, then g(w) = max U . Otherwise, g(w) ↑. We have two cases. In the first case, g is total. Then, by ∅ (n) -hyperimmunity of f , there is some w such that g(w) < f (w). Let U be the finite set witnessing that g(w)↓. In other words, c ? (∃x

∈ U )Φ G (n) e (w)↓ = x. By Lemma 2.2(a), there is some d ≤ c such that d (∃x ∈ U )Φ G (n) e (w)↓ = x, hence d Φ G (n) e (w)↓ < f (w). If g is partial, say g(w)
↑ for some w. Then by compactness of the forcing question, c ? (∃x

)Φ G (n) e (w)↓ = x. By Lemma 2.2(a), there is some d ≤ c such that d Φ G (n) e (w) ↑.
Then, for every sufficiently generic set G, f will be G (n) -hyperimmune. This is the notion of preservation of hyperimmunity, introduced by the second author [START_REF] Patey | Iterative forcing and hyperimmunity in reverse mathematics[END_REF].

Whenever the extension d of Lemma 2.2 is obtained ∅ (n) -uniformly in c, one can effectivize the construction to obtain a ∅ (n) -computable filter while controlling the nth jump of the generic set G, and therefore obtain a set of low n degree. In the case of Cohen forcing, this yields the existence of a low 1-generic set, and in the case of the forcing with computable binary trees, this yields the low basis theorem (Jockusch [15]).

Mathias forcing and the pigeonhole principle

In this paper, given a set A, we want to build a "weak" infinite subset H of A or of A. We actually construct two sets G 0 ⊆ A and G 1 ⊆ A by a variant of Mathias forcing, and ensure that at least one of them is infinite and satisfies the desired weakness property. In order to obtain a forcing question with the good definitional complexity, we shall use a different notion of forcing depending on the complexity of the formulas we want to control.

In the case of Σ 0 1 and Π 0 1 formulas, we fix a countable Scott set M, and use a notion of forcing whose conditions are tuples (F 0 , F 1 , X), where F 0 ⊆ A and F 1 ⊆ A are finite sets, and X ∈ M is an infinite set such that max(F 0 , F 1 ) < min X. Let A 0 = A and A 1 = A. Our setting is slightly different from Section 2.1 since each filter F induces two generic sets G 0 and G 1 , defined by

G i = {F i : (F 0 , F 1 , X) ∈ F } for each i < 2. A condition c = (F 0 , F 1 , X) has therefore two interpretations [c] 0 and [c] 1 , defined by [c] i = {H : F i ⊆ H ⊆ (F i ∪ X) ∩ A i } for each i < 2.
We also need to define two forcing relations depending on which of the generic sets G 0 and G 1 we control. The natural forcing relations are again too complex from a definitional point of view, and we need to define custom ones.

Definition 2.7. Let ψ(G, x) be a ∆ 0 0 formula, c = (F 0 , F 1 , X) and i < 2. (a) c i (∃x)ψ(G, x) if there is some w ∈ ω such that ψ(F i , w) holds. (b) c i (∀x)ψ(G, x) if for every w ∈ ω and every E ⊆ X, ψ(F i ∪ E, w) holds.
Note that the definition of the forcing relation for Π 0 1 formulas is stronger than the canonical one, since it would suffice to require that ψ(F i ∪ E, w) holds for every w ∈ ω and every E ⊆ X ∩ A i . Because of this, it is not in general the case that, given a Σ 0 1 formula ϕ(G) and a side i < 2, the set of conditions c such that c i ϕ(G) or c i ¬ϕ(G) is dense. However, Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF] designed a disjunctive forcing question ensuring this property on at least one side. We now detail it. Definition 2.8. Given a condition c = (F 0 , F 1 , X) and two Σ 0 1 formulas ϕ 0 (G) and ϕ 1 (G), define c ? ϕ 0 (G 0 ) ∨ ϕ 1 (G 1 ) to hold if for every 2-cover Z 0 ∪ Z 1 = X, there is some side i < 2 and some finite set E ⊆ Z i such that ϕ i (F i ∪ E) holds. This forcing relation satisfies the following disjunctive property. Lemma 2.9 (Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF]) Let c ∈ P be a condition, and ϕ 0 (G) and ϕ 1 (G) be Σ 0 1 formulas. (a) If c ? ϕ 0 (G 0 ) ∨ ϕ 1 (G 1 ), then there is some d ≤ c and some i < 2 such that

d i ϕ i (G). (b) If c ? ϕ 0 (G 0 ) ∨ ϕ 1 (G 1
), then there is some d ≤ c and some i < 2 such that d i ¬ϕ i (G).

Proof. Suppose c ? ϕ 0 (G 0 ) ∨ ϕ 1 (G 1 ) holds. Then letting Z 0 = X ∩ A 0 and Z 1 = X ∩ A 1 , there is some side i < 2 and some finite set E ⊆ X ∩ A i such that ϕ i (F i ∪ E) holds. The condition d = (F i ∪ E, F 1-i , X ∩ (max E, ∞)) is an extension of c such that d i ϕ i (G).
Suppose now that c ? ϕ 0 (G 0 )∨ϕ 1 (G 1 ). Let P be the collection of all the 2-covers Z 0 ∪Z 1 = X such that for every i < 2 and every finite set

E ⊆ Z i , ϕ i (F i ∪ E) does not hold. P is a non- empty Π 0,X 1 class, so since X ∈ M |= WKL, there is some 2-cover Z 0 ∪ Z 1 ∈ P ∩ M. Let i < 2 be such that Z i is infinite. Then the condition d = (F 0 , F 1 , Z i ) is an extension of c such that d i ¬ϕ i (G).
By a pairing argument (if for every pair m, n ∈ ω, m ∈ A or n ∈ B, then A = ω or B = ω), if a filter F is sufficiently generic, there is some side i such that for every Σ 0 1 formula ϕ(G), there is some c ∈ F such that c i ϕ(G) or c i ¬ϕ(G). We therefore get the following lemma.

Lemma 2.10 For every sufficiently generic filter F and every set G i ∈ [F] i , there is a side i < 2 such that for every Σ 0 1 formula ϕ(G), ϕ(G i ) holds if and only if c i ϕ(G) for some condition c ∈ F.

In this paper, we generalize the combinatorics of Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF] to design a notion of forcing with a forcing question having the right definitional complexity for upper formulas. This generalization involves the development of some new forcing machineries.

Acceptability classes

The combinatorics of Cholak, Jockusch and Slaman enable one to decide a Σ 0 1 formula relative to the generic set G independently of the set A, by asking whether the Σ 0 1 formula holds over "sufficiently many" finite sets. We make this largeness criterion precise through the notion of acceptability class.

Definition 2.11. An acceptability class is a collection of sets

A ⊆ 2 ω such that (a) If X ∈ A and Y ⊇ X, then Y ∈ A (b) For every k-cover Y 0 , . . . , Y k-1 of ω, there is some j < k such that Y j ∈ A.
For example, the collection of all the infinite sets is an acceptability class. Moreover, any superclass of an acceptability class is again an acceptability class. We shall exclusively consider acceptability classes which are countable intersections of Σ 0 1 classes, and which contain only infinite sets. Fix a ∆ 0 formula Φ a (G, n, m). Suppose that C is a set of integers such that e∈C U e is an acceptability class that contains only infinite sets, and such that for every finite sequence σ and every n, ζ(a, σ, n) ∈ C.

Fix a set A, and let A 0 = A and A 1 = A. Since e∈C U e is an acceptability class, there is some i < 2 such that A i ∈ e∈C U e . We can then build an infinite subset H of A i such that (∀n)(∃m)¬Φ a (H, n, m) holds by the finite extension method σ 0 ⊆ σ 1 ⊆ • • • ⊆ A i , letting H = s σ s . First, note that A i must be infinite since e∈C U e contains only infinite sets. Therefore, given an initial segment σ s ⊆ A i , one can find an extension σ s+1 σ s such that #σ s+1 > #σ s . Then, given some n ∈ ω and an initial segment

σ s ⊆ A i , since ζ(a, σ s , n) ∈ C, A i ∈ U ζ(a,σs,n) ,
so there is some ρ ⊆ A i -{0, . . . , |σ s |} and some m ∈ ω such that ¬Φ a (σ s ∪ρ, n, m) holds. Letting σ s+1 = σ s ρ, we made some progress to satisfy the Π 0 2 fact (∀n)(∃m)¬Φ a (H, n, m). Before moving to the design of the notions of forcing, we prove two technical lemmas about acceptability classes. Lemma 2.13 Suppose A 0 ⊇ A 1 ⊇ . . . is a decreasing sequence of acceptability classes. Then s A s is an acceptability class.

Proof. If X ∈ s A s and Y ⊇ X, then for every s, since A s is an acceptability class, Y ∈ A s , so Y ∈ s A s . Let Y 0 , . . . , Y k-1 be a k-cover of ω. For every s ∈ ω, there is some j < k such that Y j ∈ A s . By the infinite pigeonhole principle, there is some j < k such that Y j ∈ A s for infinitely many s.

Since A 0 ⊇ A 1 ⊇ is a decreasing sequence, Y j ∈ s A s .
Lemma 2.14 Let A be a Σ 0 1 class. The sentence "A is an acceptability class" is Π 0 2 .

Proof. Say A = {X : (∃σ X)ϕ(σ)} where ϕ is a Σ 0 1 formula. By compactness, A is an acceptability class iff for every σ and τ such that σ ⊆ τ and ϕ(σ) holds, ϕ(τ ) holds, and for every k, there is some n ∈ ω such that for every σ 0 ∪ • • • ∪ σ k-1 = {0, . . . , n}, there is some j < k such that ϕ(σ j ) holds.

From Mathias forcing to a second jump control

The notion of forcing used to control the first jump of solutions to the infinite pigeonhole principle is a variant of Mathias forcing, a purely combinatorial notion with no effectiveness restriction on the reservoirs. This notion is essential in the study of Ramsey's theory. We now review the basic definitions of Mathias forcing, and then describe how to enrich this notion of forcing to have a better second jump control. Definition 2.15. Let Q 0 be the set of ordered pairs (σ, X) such that X is infinite and X ∩ {0, . . . , |σ|} = ∅.

Mathias forcing builds a single object G by approximations (conditions) which consist in an initial segment σ of G, and an infinite reservoir of integers. The purpose of the reservoir is to restrict the set of elements we are allowed to add to the initial segment. The reservoir therefore enriches the standard Cohen forcing by adding an infinitary negative restrain. The denotation of a condition is therefore naturally defined as follows.

Given a condition p = (σ, X)

∈ Q 0 , let [σ, X] = {Y ∈ [ω] ω : σ Y ∧ Y -{0, . . . , |σ|} ⊆ X} Definition 2.16. The partial order on Q 0 is defined by (τ, Y ) ≤ (σ, X) if σ τ , Y ⊆ X and τ -σ ⊆ X.
The following lemma is standard, and expresses that whenever the approximation becomes more precise, then the set of "candidates" decreases.

Lemma 2.17 Suppose (τ, Y ) ≤ (σ, X) ∈ Q 0 . Then [τ, Y ] ⊆ [σ, X].
The forcing relation for Σ 0 1 and Π 0 1 formulas can be defined in a natural way, and has the right definitional complexity (relative to the reservoir), that is, forcing a Σ 0 1 and a Π 0 1 fact is Σ 0 1 and Π 0 1 relative to the reservoir, respectively. The relation can be extended to arbitrary arithmetical formulas by an inductive definition, but then forcing a Π 0 n formula becomes Π 0 n+1 relative to the reservoir. This makes the forcing question for higher formula fail to have a good definitional complexity, even when the reservoir is required to be computable. We refer the reader to Cholak, Dzhafarov, Hirst and Slaman [START_REF] Cholak | Generics for computable Mathias forcing[END_REF] for the study a computable Mathias forcing.

Definition 2.18. Let Φ e (G, n) be a ∆ 0 formula with free variable m. Let p = (σ, X) fact usually requires to take an extension, we cannot force all the Σ 0 1 facts simultaneously. A Π 0 2 fact is then forced if, whatever the further stage of the construction, it will always be possible to make some progress by forcing one more Σ 0 1 fact. In the case of Mathias forcing, the notion of reservoir is too permissive, and it is not possible to talk about the extensions of a condition with a definitionally simple formula. We will therefore enrich the notion of Mathias condition to add some restrictions on the reservoir, so that the extensions can be described in a simpler way. One can think of a condition (σ, X, C, U ) as a Mathias condition (σ, U ) with a set C denoting an acceptability class e∈C U e which will impose some constraints on the nature of the reservoirs. This view is reflected through the denotation of a condition. Given a condition p

∈ Q 0 . (a) p (∃n)Φ e (G, n) if (∃n)Φ e (σ, n) (b) p (∀n)Φ e (G, n) if (∀τ ⊆ X)(∀n)Φ e (σ ∪ τ, n) Lemma 2.
= (σ, X, C, U ) ∈ Q 1 , let [σ, X, C, U ] = [σ, U ]
From a purely combinatorial viewpoint, the reservoir X of a condition (σ, X, C, U ) could have been dropped, yielding a notion of forcing with 3-tuples (σ, C, U ). The reservoir X is kept for effectiveness restrictions reasons, which will become clear in section 3. Indeed, the reservoir X is responsible for forcing Π 0 1 facts, while the reservoir U will force (together with C) Π 0 2 facts. When considering effective forcing, we shall see that U will be "one jump up" of X. For example, X can be taken to be of low degree, while U will be low over ∅ . Since X will solely be responsible for forcing Π 0 1 fact, we shall relate a condition (σ, X, C, U ) with the Mathias condition (σ, X).

Lemma 2.21 Suppose (σ, X, C, U ) ∈ Q 1 . Then (a) (σ, X) ∈ Q 0 (b) [σ, X, C, U ] ⊆ [σ, X]
Proof. (a) Since U ∈ e U e and e U e contains only infinite sets, then U is infinite. In particular, X is infinite since X ⊇ U . Moreover, X ∩ {0, . . . , |σ|} = ∅. Therefore (σ, X)

∈ Q 0 . (b) Since (σ, U ) ≤ (σ, X) as a Mathias condition, by Lemma 2.17, [σ, X, C, U ] ⊆ [σ, X].
In particular, if (σ, X)

(∃n)Φ e (G, n) (resp. (σ, X) (∀n)Φ e (G, n)), then (∃n)Φ e (Y, n) (resp. (∀n)Φ e (Y, n)) holds for every Y ∈ [σ, X, C, U ]. Definition 2.22. The partial order on Q 1 is defined by (τ, Y, D, V ) ≤ (σ, X, C, U ) if σ τ , Y ⊆ X, V ⊆ U , C ⊆ D and τ -σ ⊆ U .
From the definition of a forcing condition (σ, X, C, U ), and especially from the constraint that U ∈ e∈C U e , it is not clear at all that there exists infinite decreasing sequences of conditions with non-trivial reservoirs, that is, with U being coinfinite. In general, being a valid condition is not even closed under removing finitely elements from the reservoirs. Indeed, if U ∈ e∈C U e and Y ⊆ X is cofinite in X, then it might be that Y ∩ U ∈ e∈C U e . Thankfully, since e∈C U e is an acceptability class, we shall see in section 3 that by carefully choosing our reservoirs, we will be able to apply some basic operations on them and keep having valid conditions.

Lemma 2.23 Suppose (τ, Y, D, V ) ≤ (σ, X, C, U ) ∈ Q 1 . Then (a) [τ, Y, D, V ] ⊆ [σ, X, C, U ] (b) (τ, Y ) ≤ (σ, X) Proof. (a) Since σ τ , V ⊆ U and τ -σ ⊆ U , then (τ, V ) ≤ (σ, U ). Therefore [τ, Y, D, V ] ⊆ [σ, X, C, U ]. (b) Immediate since (τ, V ) ≤ (σ, U ), Y ⊆ X and and τ -σ ⊆ U ⊆ X.
We now define the forcing relation for Σ 0 2 formulas and Π 0 2 formulas. In the case of Σ 0 2 formulas, this coincides with the forcing relation for Σ 0 2 formulas over Mathias forcing. The the case of Π 0 2 formulas is new, and is justified by our explanations about the combinatorics of acceptability classes. Recall the function ζ of Definition 2.12. Definition 2.24. Let Φ e (G, n, m) be a ∆ 0 formula with free variables m and n.

Let p = (σ, X, C, U ) ∈ Q 1 . (a) p (∃n)(∀m)Φ e (G, n, m) if (∃n)(∀τ ⊆ X)(∀m)Φ e (σ ∪ τ, n, m) (b) p (∀n)(∃m)¬Φ e (G, n, m) if (∀ρ ⊆ U )(∀n)ζ(e, σ ∪ ρ, n) ∈ C Lemma 2.25
Let Φ e (G, n, m) be a ∆ 0 formula with free variables m and n. Let p, q ∈ Q 1 be such that q ≤ p. We now define the notion of genericity which will be sufficient to prove the main property of the forcing relation, that is, whenever a formula is forced, then it will hold over the generic set.

Definition 2.26. A Q 1 -filter F is 2-generic if for every Σ 0 2 formula ϕ(G), there is some p ∈ F such that p ϕ(G) or p ¬ϕ(G).
As explained above, it is not clear at all that 2-generic Q 1 -filters exist. Their existence will be proven in section 3.

Lemma 2.27 Let F be a 2-generic Q 1 -filter, and Φ e (G, n, m) be a ∆ 0 formula with free variables m and n. If p (∀n)(∃m)¬Φ e (G, n, m) for some p ∈ F, then for every n ∈ ω, there is some q = (τ, Y, D, V ) ∈ F such that (τ, Y ) (∃m)¬Φ e (G, n, m).

Proof. Fix n ∈ ω, and let Φ u (G, a, b) = ¬Φ e (G, n, a). Since F is a 2-generic filter, there is some

q = (τ, Y, D, V ) ∈ F such that q (∃a)(∀b)Φ u (G, a, b) or q (∀a)(∃b)¬Φ u (G, a, b)
Suppose first q (∃a)(∀b)Φ u (G, a, b). Then in particular (τ, Y ) (∃a)¬Φ e (G, n, a) and we are done. Suppose now q (∀a)(∃b)¬Φ u (G, a, b). Since F is a filter, we can assume that q ≤ p. In particular, by the lemma's hypothesis, q (∀n)(∃m)¬Φ e (G, n, m), so ζ(e, τ, n) ∈ D. Since V ∈ e∈D U e , then V ∈ U ζ(e,τ,n) . Therefore, there is some ρ ⊆ V -{0, . . . , |τ |} and some m ∈ ω such that ¬Φ e (τ ∪ ρ, n, m) holds. Since q (∀a)(∃b

)¬Φ u (G, a, b), ζ(u, τ ∪ ρ, m) ∈ D, so V ∈ U ζ(u,τ ∪ρ,m)
. Therefore, there is some µ ⊆ V -{0, . . . , |τ ∪ ρ|} such that Φ e (τ ∪ ρ ∪ µ, n, m) holds. This contradicts ¬Φ e (τ ∪ ρ, n, m).

Lemma 2.28 Let F be a 2-generic Q 1 -filter. Then there is some p ∈ F such that p (∀n

)(∃m)[m > n ∧ m ∈ G]. Proof. Let Φ e (G, n, m) ≡ [m ≤ n ∨ m ∈ G]. Since F is a 2-generic filter, there is some p = (σ, X, C, U ) ∈ F such that p (∃n)(∀m)Φ e (G, n, m) or p (∀n)(∃m)¬Φ e (G, n, m)
Suppose for the sake of contradiction that the first case holds. Then (∃n

)(∀ρ ⊆ X)(∀m)[m ≤ n ∨ m ∈ σ ∪ ρ]. This is impossible since X is infinite. Given a collection F ⊆ Q 1 , we let G F = {σ : (σ, X, C, U ) ∈ F}.
Lemma 2.29 Let F be a 2-generic Q 1 -filter. Let Φ e (G, n, m) be a ∆ 0 formula with free variables m and n, and let p ∈ F.

(a) If p (∃n)(∀m)Φ e (G, n, m), then (∃n)(∀m)Φ e (G F , n, m) holds. (b) If p (∀n)(∃m)¬Φ e (G, n, m), then (∀n)(∃m)¬Φ e (G F , n, m) holds.
Proof. Say p = (σ, X, C, U ). We first prove (b). Fix some n. By Lemma 2.27, there is some q = (τ, Y, D, V ) ∈ F such that (τ, Y ) (∃m)¬Φ e (G, n, m). By Lemma 2.19(a) (∃m)¬Φ e (G F , n, m) holds. We now prove (a). For this, we claim that G F ∈ [p]. Indeed, by (b) of this lemma (which we already proved) and Lemma 2.28, G F is infinite. Moreover, σ G F , and for every ρ ⊆ G F -σ, there is some q = (τ, Y, D, V ) ∈ F with q ≤ p such that ρ ⊆ τ . In particular, ρ ⊆ U , so G F ∈ [p]. By Lemma 2.21(b), G F ∈ [σ, X]. Since p (∃n)(∀m)Φ e (G, n, m), there is some n ∈ ω such that (σ, X) (∀m)Φ e (G, n, m). By Lemma 2.19(b), (∀m)Φ e (G F , n, m) holds.

Lemma 2.30 Let F be a 2-generic Q 1 -filter. Then G F is infinite.

Proof. Immediate by Lemma 2.28 and Lemma 2.29.

Pigeonhole forcing

We now design the actual notion of forcing used to construct solutions to the infinite pigeonhole principle. It can be seen as a tree version of the Q 1 -forcing, with some effectiveness restrictions on the conditions. Let M |= WKL be a countable Turing ideal, and let

A 0 ∪ A 1 = ω. Definition 3.1. Let P 1 denote the set of conditions (σ 0 s , σ 1 s , X s , C, U s : s < k) such that (a) σ i s ⊆ A i for every s < k (b) X s ∩ {0, . . . , max i |σ i s |} = ∅ ; X s ⊇ U s for every s < k (c) U 0 , . . . , U k-1 is a k-cover of ω -{0, . . . , max i,s |σ i s |} (d) e∈C U e is an acceptability class containing only infinite sets (e) X , U , C ∈ M A Turing ideal M = {X 0 , X 1 , . . . } is countable coded by a set B if B = i X i . An index of some Z ∈ M is then some i ∈ ω such that Z = X i .
Thanks to the notion of index, any P 1condition can be finitely presented as follows. An index of a P 1 -condition c = (σ 0 s , σ 1 s , X s , C, U s : s < k) is a tuple (σ 0 s , σ 1 s , a s , b, e s : s < k) where a s is an index for X s , b an index for C and e s is an index for U s . Note that the existence of these indices is ensured by property (e) of Definition 3.1. Definition 3.2. The partial order on P 1 is defined by

(τ 0 s , τ 1 s , Y s , D, V s : s < ) ≤ (σ 0 s , σ 1 s , X s , C, U s : s < k) if there is a function f : → k such that for every i < 2 and s < , σ i f (s) τ i s , Y s ⊆ X f (s) , V s ⊆ U f (s) , C ⊆ D and τ i s -σ i f (s) ⊆ U f (s)
. We can think of the P 1 -forcing as a tree version of the Q 1 -forcing. Given a P 1 -condition c = (σ 0 s , σ 1 s , X s , C, U s : s < k), each s < k will be referred to as a branch of c. Each branch s represents two candidate Q 1 -conditions c [0,s] = (σ 0 s , X s , C, U s ) and c [1,s] = (σ 1 s , X s , C, U s ). Actually, they will not be true Q 1 -conditions in general, since there is no reason why U s would belong to e∈C U e . For example, U s might be finite. We shall however see in Lemma 3.4 that there must be at least one branch s such that c [0,s] , c [1,s]

∈ Q 1 .
The notion of condition extension enables to fork branches, according to the function f witnessing the extension. We write d ≤ f c if d ≤ c is witnessed by the function f . We say that the branch t of d refines the branch s of c if f (t) = s. We are interested in two particular kinds of extensions: the ones which do not fork any branch, and the ones which fork exactly one branch. Given a condition c = (σ 0 s , σ 1 s , X s , C, U s : s < k) ∈ P 1 , a simple extension of c is a condition d ≤ f c such that f is the identity function. An s-extension of c is a condition d ≤ f c such that f -1 (t) is a singleton for every t = s.

Validity and projections

We now develop the framework which relates P 1 -forcing to Q 1 -forcing. Informally, a branch

s of a condition c = (σ 0 s , σ 1 s , X s , C, U s : s < k) ∈ P 1 is a good candidate if either c [0,s] , c [1,s] ∈ Q 1 is a valid Q 1 -condition. Definition 3.3. Let c = (σ 0 s , σ 1 s , X s , C, U s : s < k) be a P 1 -condition. A branch s is valid in c if U s ∈ e∈C U e .
From the discussion above, it should be clear that if a branch s is valid in c, then c [0,s] , c [1,s] ∈ Q 1 . We first prove that valid branches exist. Lemma 3.4 Every P 1 -condition has a valid branch.

Proof. Let c = (σ 0 s , σ 1 s , X s , C, U s : s < k) ∈ P 1 . Suppose for the sake of contradiction that for every s < k, U s ∈ e∈C U e . Let u ∈ ω be large enough to that {U s : s < k} ∪ {{0, . . . , u}} is a cover of ω. This cover contradicts the fact that e∈C U e is an acceptability class containing only infinite sets.

Thanks to compactness, being a valid branch is not definitionally too complex. In particular, if we work within a Turing ideal countable coded by a set B such that B ≤ ∅ , then being a valid branch is Π 0 3 .

Lemma 3.5 Let c be a P 1 -condition. The sentence "The branch s is valid in c" is Π 0 2 (M).

Proof. Say c = (σ 0 s , σ 1 s , X s , C, U s : s < k). Then s is valid in c if for every n ∈ C, there is a finite set E ⊆ U s such that E ∈ e∈C,e<n U e . The sentence is Π 0 2 (C ⊕ X s ⊕ U s ), hence Π 0 2 (M).
By upward-closure of the notion of acceptability class, if a branch t of a P 1 -condition d is valid, and d ≤ f c, then the branch f (t) of c is also valid. Therefore, given an infinite decreasing sequence of conditions, the valid branches form an infinite subtree.

Lemma 3.6 Suppose d ≤ f c ∈ P 1 and d [i,s] ∈ Q 1 . Then (a) c [i,f (s)] ∈ Q 1 (b) d [i,s] ≤ c [i,f (s)] .
Proof. Say c = (σ 0 s , σ 1 s , X s , C, U s : s < k) and d = (τ 0 s , τ 1 s , Y s , D, V s : s < ).

(a) X s ∩ {0, . . . , |σ i s |} = ∅ and e∈C U e is an acceptability class containing only infinite sets. We need to check that U f (s) ∈ e∈C U e . By assumption, V s ∈ e∈D U e . Since V s ⊆ U f (s) , then U f (s) ∈ e∈D U e . Moreover, C ⊆ D, so e∈D U e ⊆ e∈C U e , and we are done.

(b) This is immediate by definition of the extension relation of P 1 .

We now define the notion of projector, which in the context of an infinite decreasing sequence of P 1 -conditions, corresponds to an infinite path through the tree of valid branches. According to our notation, we write F [i,P ] = {c [i,P (c)] : c ∈ F}. An F-projection is a collection F [i,P ] = {c [i,P (c)] : c ∈ F} for some F-projector P .

The forcing question

We now design a disjunctive forcing question to control the second jump, in the same spirit as the one designed by Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF] to control the first jump. Given a branch s of a condition c and two Σ 0 2 formulas ϕ 0 (G) and ϕ 1 (G), we define a Σ 0 1 (M) relation c ? s ϕ 0 (G) ∨ ϕ 1 (G), such that -If c ? s ϕ 0 (G)∨ϕ 1 (G), then there is an extension d such that for every projector P going throw the branch s of c (P (c) = s), then d [i,P (d)] ϕ i (G) for some i < 2.

-If c ? s ϕ 0 (G)∨ϕ 1 (G), then there is an extension d such that for every projector P going throw the branch s of c (P (c) = s), then d [i,P (d)] ¬ϕ i (G) for some i < 2.

Fix a sufficiently generic P 1 -filter F and an F-projector P . By a pairing argument and using the disjunctive forcing question, there must be a side i < 2 such that F [i,P ] is 2-generic. to hold if for every Z 0 ∪ Z 1 = U s , there is finite set F ⊆ C, some ρ 0 , . . . , ρ a-1 ⊆ Z 0 and n 0 , . . . , n a-1 ∈ ω, some µ 0 , . . . , µ b-1 ⊆ Z 1 and u 0 , . . . , u

b-1 ∈ ω such that e∈F U e j<a U ζ(e 0 ,σ 0 s ∪ρ j ,n j ) j<b U ζ(e 1 ,σ 1 s ∪µ j ,u j )
is not an acceptability class.

Lemma 3.9 Let s be a branch in c ∈ P 1 and let Φ e 0 (G, n, m) and Φ e 1 (G, n, m) be two ∆ 0 formulas. The relation

c ? s (∃n)(∀m)Φ e 0 (G, n, m) ∨ (∃n)(∀m)Φ e 1 (G, n, m) is Σ 0 1 (M).
Proof. By compactness, the relation holds if there is a finite set E ⊆ U s such that for every E 0 ∪ E 1 = E, there is some finite set F ⊆ C, some ρ 0 , . . . , ρ a-1 ⊆ E 0 and n 0 , . . . , n a-1 ∈ ω, some µ 0 , . . . , µ b-1 ⊆ E 1 and u

0 , . . . , u b-1 ∈ ω such that e∈F U e j<a U ζ(e 0 ,σ 0 s ∪ρ j ,n j ) j<b U ζ(e 1 ,σ 1 s ∪µ j ,u j )
is not an acceptability class. By Lemma 2.14, not being an acceptability class is Σ 0 2 . The overall relation is Σ

0 1 (C ⊕ U s ⊕ ∅ ), hence is Σ 0 1 (M).
Lemma 3.10 Let s be a branch in c ∈ P 1 and let Φ e 0 (G, n, m) and Φ e 1 (G, n, m) be two ∆ 0 formulas.

(a) If c ? s (∃n)(∀m)Φ e 0 (G, n, m)∨(∃n)(∀m)Φ e 1 (G, n, m), then there is an s-extension d ≤ f c such that for every valid branch t in d for which f (t) = s, there is some i < 2 such that d [i,t] (∃n)(∀m)Φ e i (G, n, m). (b) If c ? s (∃n)(∀m)Φ e 0 (G, n, m)∨(∃n)(∀m)Φ e 1 (G, n, m), then there is an s-extension d ≤ f c such that for every valid branch t in d for which f (t) = s, there is some i < 2 such that d [i,t] (∀n)(∃m)¬Φ e i (G, n, m).

Moreover, an index of d can be found A ⊕ M-uniformly in an index of c, s, e 0 and e 1 and the knowledge of which case holds.

Proof. Say c = (σ 0 s , σ 1 s , X s , C, U s : s < k). (a) Let Z 0 = U s ∩ A 0 and Z 1 = U s ∩ A 1 .
Unfolding the definition of the forcing question, there is finite set F ⊆ C, some ρ 0 , . . . , ρ a-1 ⊆ Z 0 and n 0 , . . . , n a-1 ∈ ω, some µ 0 , . . . , µ b-1 ⊆ Z 1 and u

0 , . . . , u b-1 ∈ ω such that e∈F U e j<a U ζ(e 0 ,σ 0 s ∪ρ j ,n j ) j<b U ζ(e 1 ,σ 1 s ∪µ j ,u j )
is not an acceptability class. Given ∈ ω, let C be the Π 0,Xs 1 class of all -covers of ω R 0 , . . . , R -1 such that for every t < , R t ∈ e∈F U e j<a U ζ(e 0 ,σ 0 s ∪ρ j ,n j ) j<b U ζ(e 1 ,σ 1 s ∪µ j ,u j ) . By assumption, C = ∅ for some ∈ ω. By the low basis theorem, pick some -cover of ω R 0 , . . . , R -1 in C which is low over X s .

Define the P 1 -condition d = (τ 0 s , τ 1 s , Y s , C, V s : s < k + -1) obtained from c by splitting the branch s into branches s 0 , . . . , s -1 , and leaving the other branches unchanged. For each t < , let

V st = U s ∩ R t , Y st = X s ∩ R t . If R t ∈ U e for some e ∈ C, then τ 0 st = σ 0 s and τ 1 st = σ 1 s . If R t ∈ U ζ(e 0 ,σ 0 s ∪ρ j ,n j ) for some j < a, let τ 1 st = σ 1 s and τ 0 st = σ 0 s ∪ ρ j . If R t ∈ U ζ(e 1 ,σ 1
s ∪µ j ,u j ) for some j < b, let τ 0 st = σ 0 s and τ 1 st = σ 1 s ∪ µ j . The P 1 -condition d is by construction an s-extension of c. We now claim that for every valid branch s t in d, there is some i < 2 such that d [i,st] (∃n)(∀m)Φ e i (G, n, m). Since s t is valid in d, R t ∩ U s ∈ e∈C U e . In particular, R t ∈ e∈C U e , so there is some i < 2 such that R t ∈ U ζ(e i ,τ i s t ,n) for some n. Unfolding the definition, (∀τ ⊆ R t )(∀m)Φ e i (τ i st ∪ τ, n, m), so d [i,st] (∃n)(∀m)Φ e i (G, n, m).

(b) Let D be the Π 0 1 (M) class of all Z 0 ⊕ Z 1 such that Z 0 ∪ Z 1 = U s such that for every finite set F ⊆ C, every ρ 0 , . . . , ρ a-1 ⊆ Z 0 and every n 0 , . . . , n a-1 ∈ ω, every µ 0 , . . . , µ b-1 ⊆ Z 1 and every u 0 , . . . , u b-1 ∈ ω, e∈F U e j<a U ζ(e 0 ,σ 0 s ∪ρ j ,n j ) j<b U ζ(e 1 ,σ 1 s ∪µ j ,u j ) is an acceptability class. Since M |= WKL, there is some

Z 0 ⊕ Z 1 ∈ D ∩ M. Let D = C ∪ {ζ(e i , σ i s ∪ ρ, n) : i < 2, ρ ⊆ X s ∩ Z i , n ∈ ω)
. By Lemma 2.13, e∈D U e is an acceptability class.

Define the P 1 -condition d = (τ 0 s , τ 1 s , Y s , D, V s : s < k + 1) obtained from c by splitting the branch s into 2 branches s 0 , s 1 , and leaving the other branches unchanged. For each ,n,m). This completes the proof of the lemma. Lemma 3.11 Let F be a sufficiently generic P 1 -filter, and let P be an F-projector. There is some i < 2 such that F [i,P ] is a 2-generic Q 1 -filter.

i < 2, let Y s i = X s , V s i = V ∩ Z i , τ 0 s 0 = σ 0 s and τ 1 s 1 = σ 1 s . For each i < 2, if s i is valid in d, then d [i,s i ] (∀n)(∃m)¬Φ e i (G
Proof. By Lemma 3.10, for every P 1 -condition c ∈ F and every pair of Σ 0 2 formulas ϕ 0 (G), ϕ 1 (G), there is a P (c)-extension d of c such that for every valid branch t in d refining the branch P (c) of c, d [i,t] ϕ i (G) or d [i,t] ¬ϕ i (G) for some i < 2. Since F is sufficiently generic, there is such an extension d ∈ F, and since P (d) is valid in d and refines the branch P (c) of c, d [i,P (d)] ϕ i (G) or d [i,P (d)] ¬ϕ i (G) for some i < 2. By a pairing argument, there is some i < 2 such that for every Σ 0 2 formula ϕ(G), there is some c ∈ F such that c [i,P (c)] ϕ(G) or c [i,P (c)] ¬ϕ(G). Therefore F [i,P ] is 2-generic. Since P is an F-projector, F [i,P ] ⊆ Q 1 . Since F is a filter, by Lemma 3.6, so is F [i,P ] . Later, Flood [START_REF] Flood | Reverse mathematics and a Ramsey-type König's lemma[END_REF] identified the amount of compactness present in Ramsey's theorem for pairs as a principle called the Ramsey-type weak König's lemma. In this section, we reprove Liu's theorem by providing an alternative (and arguably simpler) proof of his main combinatorial theorem.

Theorem 5.1 (Liu) For every set A, there is an infinite set H ⊆ A or H ⊆ A of non-PA degree.

Before proving Theorem 5.1, we deduce Liu's theorem from it. Theorem 5.2 (Liu) For every computable coloring f : [ω] 2 → 2, there is an infinite fhomogeneous set of non-PA degree.

Proof. Let R = R 0 , R 1 , . . . be the computable sequence defined by R x = {y : f (x, y) = 1}. By Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF]Lemma 9.16], there is an infinite R-cohesive set C = {x 0 < x 1 < . . . } of non-PA degree. This fact can be proven using a simple computable Mathias forcing. In particular, (∀x ∈ ω) lim y∈C f (x, y) exists. Let A = {n ∈ ω : lim m f (x n , x m ) = 1}. Note that A = {n ∈ ω : lim m f (x n , x m ) = 0}. By a relativization of Theorem 5.1, there is an infinite set H ⊆ A or H ⊆ A such that H ⊕C is of non-PA degree. Suppose that H ⊆ A, H ⊕C-computably thin out the set {x n : n ∈ H} using a greedy argument to obtain an infinite f -homogeneous set for color 1. The case H ⊆ A is similar, and yields and infinite set f -homogeneous for color 0.

We now prove Theorem 5.1 using a variant of the notion of forcing designed in this paper. Fix a set A, and let A 0 = A and A 1 = A. Definition 5.3. Let P denote the set of conditions (σ s , X s , C : s < k) such that (a) for every s < k, there is some i < 2 such that σ s ∪ X s ⊆ A i (b) X 0 , . . . , X k-1 is a k-cover of ω -{0, . . . , max s |σ s |} (c) e∈C U e is an acceptability class containing only infinite sets (d) C is computable Note that no effectiveness restriction is imposed on the reservoirs X. Their restriction is of combinatorial nature, since their union is required to be cofinite. Definition 5.4. The partial order on P is defined by (τ s , Y s , D : s < ) ≤ (σ s , X s , C : s < k) if there is a function f : → k such that for every s < , σ f (s) τ s , Y s ⊆ X f (s) , C ⊆ D and τ s -σ f (s) ⊆ X f (s) .

Again, we write d ≤ f c if d ≤ c is witnessed by the function f , and say that the branch s is valid in c = (σ s , X s , C : s < k) if X s ∈ e∈C U e . We write c [s] for (σ s , X s , C, X s ). In other words, the branch s is valid in c if c [s] ∈ Q 1 . The notion of projector is defined accordingly. Lemma 5.5 Let c ∈ P be a condition, and s be such that c [s] ∈ Q 1 . Then for every n, there is a simple extension d ≤ c such that d [s] (∃m > n)m ∈ G.

Proof. Say c = (σ s , X s , C : s < k). Since c [s] ∈ Q 1 , then X s ∈ e∈C U e . In particular, X s is infinite. Let m ∈ X s be such that m > n. Then condition d = (τ s , X s ∩ (m, ∞), C : s < k) defined by τ s = σ s ∪ {m}, and τ t = σ t otherwise, is the desired simple extension of c. Then there is an s-extension d ≤ f c such that for every valid branch t in d for which f (t) = s, d [t] (∃n)Φ e (G, n) ↓= Φ n (n) or d [t] (∃n)Φ e (G, n) ↑

Theorem 1 . 6

 16 Every ∆ 0 3 set A has an infinite subset H ⊆ A or H ⊆ A of low 3 degree.

Lemma 2 . 2

 22 Let c ∈ P be a condition, and ϕ(G) be a Σ 0 n formula. (a) If c ? ϕ(G), then there is some d ≤ c such that d ϕ(G). (b) If c ? ϕ(G), then there is some d ≤ c such that d ¬ϕ(G). Any forcing relation induces a forcing question ? defined by c ? ϕ(G) if and only if

  Fix an effective enumeration U 0 , U 1 , . . . of all the Σ 0 1 classes upward-closed under the superset relation, that is, if X ∈ U e and Y ⊇ X, then Y ∈ U e . These acceptability classes can be represented by sets of integers C, denoting the class e∈C U e , where {U e } e∈ω is a standard enumeration of the Σ 0 1 classes. Let us illustrate how one uses acceptability classes to force Π 0 2 facts. Definition 2.12. Let ζ : ω ×2 <ω ×ω → ω be the computable function that takes as a parameter a code for a ∆ 0 formula Φ e (G, n, m), a string σ and an integer n, and which gives a code for the open set {X : (∃ρ ⊆ X -{0, . . . , |σ|})(∃m)¬Φ e (σ ∪ ρ, n, m)}

Definition 2 . 20 .

 220 Let Q 1 be the set of tuples (σ, X, C, U ) such that (a) X ∩ {0, . . . , |σ|} = ∅ ; X ⊇ U with X, U ⊆ ω (b)e∈C U e is an acceptability class containing only infinite sets (c) U ∈ e∈C U e .

  (a) If p (∃n)(∀m)Φ e (G, n, m) then q (∃n)(∀m)Φ e (G, n, m) (b) If p (∀n)(∃m)¬Φ e (G, n, m) then q (∀n)(∃m)¬Φ e (G, n, m) Proof. Say p = (σ, X, C, U ) and q = (τ, Y, D, V ) (a) Since p (∃n)(∀m)Φ e (G, n, m), then there is some n such that (σ, X) (∀m)Φ e (G, n, m). By Lemma 2.23, (τ, Y ) ≤ (σ, X), so (τ, Y ) (∀m)Φ e (G, n, m), hence q (∃n)(∀m) Φ e (G, n, m). (b) Let ρ = τ -σ. By definition of q ≤ p, ρ ⊆ U . Let ρ 1 ⊆ V . In particular, ρ ∪ ρ 1 ⊆ U . By definition of p (∀n)(∃m)¬Φ e (G, n, m), for every n, ζ(e, σ ∪ ρ ∪ ρ 1 , n) ∈ C ⊆ D. So ζ(e, τ ∪ ρ 1 , n) ∈ D for every n.

Definition 3 . 7 .

 37 Let F ⊆ P 1 be a collection. An F-projector is a function P : F → ω such that (a) The branch P (c) is valid in c for every c ∈ F (b) If d ≤ f c ∈ F then P (c) = f (P (d)).

Definition 3 . 8 .

 38 Let c = (σ 0 s , σ 1 s , X s , C, U s : s < k) ∈ P 1 , s < k,and let Φ e 0 (G, n, m) and Φ e 1 (G, n, m) be two ∆ 0 formulas. Define the relation c ? s (∃n)(∀m)Φ e 0 (G, n, m) ∨ (∃n)(∀m)Φ e 1 (G, n, m)

Definition 5 . 6 .

 56 Let ξ : ω × 2 <ω → ω be the computable function that takes as an index of a Turing functional Φ e (G, n), a string σ and which gives a code for the open set {X : (∃ρ ⊆ X -{0, . . . , |σ|})(∃n)Φ e (σ ∪ ρ, n) ↓= Φ n (n)} Lemma 5.7 Let s be a branch of a condition c ∈ P, and let Φ e (G, n) be a Turing functional.

  [START_REF] Liu | Cone avoiding closed sets[END_REF] Let Φ e (G, n) be a ∆ 0 formula with free variable n, and let p ∈ Q 0 . (a) If p (∃n)Φ e (G, n), then (∃n)Φ e (Y, n) holds for every Y ∈ [p] (b) If p (∀n)¬Φ e (G, n), then (∀n)¬Φ e (Y, n) holds for every Y ∈ [p].

	The forcing relation for Σ 0 2 formulas (∃n)(∀m)Φ e (G, n, m) can be defined with Mathias forc-
	ing as p	(∃n)(∀m)Φ e (G, n, m) iff (∃n)p	(∀m)Φ e (G, n, m), and has the right definitional
	properties. The issue comes when considering Π 0 2 formulas (∀n)(∃m)¬Φ e (G, n, m). Forcing a Π 0 2 fact can be seen as a promise to satisfy a countable collection of Σ 0 1 facts. Since forcing a Σ 0 1

Applications

In this section, we apply the framework developed in section 3 to derive our main theorems. 4.1. Preservation of non-Σ 0 2 definitions Our first application shows the existence, for every instance of the pigeonhole principle, of a solution which does not collapse the definition of a non-Σ 0 2 set into a Σ 0 2 one. This corresponds to preservation of one non-Σ 0 2 definition, following the terminology of Wang [START_REF] Wang | The definability strength of combinatorial principles[END_REF].

Theorem 4.1 Fix a non-Σ 0 2 set B. For every set A, there is an infinite set H ⊆ A or H ⊆ A such that B is not Σ 0,H 2 .

Fix B and A, and let A 0 = A and A 1 = A. By Wang [START_REF] Wang | The definability strength of combinatorial principles[END_REF]Theorem 3.6.], there is a countable Turing ideal M |= WKL such that B is not Σ 0 1 (M) and ∅ ∈ M. We build our infinite set by the notion of forcing P 1 within the Turing ideal M. Fix an enumeration ϕ 0 (G, n), ϕ 1 (G, n) of all Σ 0 2 formulas with one set parameter G and one integer parameter n.

Lemma 4.2 Let F be a sufficiently generic P 1 -filter and P be an F-projector. For every pair of Σ 0 2 formulas ϕ 0 (G, n) and ϕ 1 (G, n), there is some i < 2 and some p ∈ F [i,P ] such that (∃n

Proof. Fix some c ∈ F, and let

. By Lemma 3.10(a), there is an s-extension d of c such that for every valid branch t of d refining the branch s of c, d [i,t]

. By Lemma 3.10(b), there is an s-extension d of c such that for every valid branch t of d refining the branch s of c, d [i,t] ¬ϕ i (G, n) for some i < 2.

By genericity of F, there is such an extension d ∈ F. Let P (d) = t. Since t is valid in d, then either n ∈ B and d [i,t] ϕ i (G, n), or n ∈ B and d [i,t] ¬ϕ i (G, n) for some i < 2.

We are now ready to prove Theorem 4.1.

Proof of Theorem 4.1. Let F be a sufficiently generic P 1 -filter and P be an F-projector. By Lemma 4.2, and by a pairing argument, there is some i < 2 such that for every Σ 0 2 formula ϕ(G, n), there is some p ∈ F [i,P ] such that

In particular, G = F [i,P ] is 2-generic, so by Lemma 2.30, G G is infinite, and by Lemma 2.29, B is not Σ 0 2 . By definition of

This completes the proof of Theorem 4.1. The following corollary would correspond to strong jump cone avoidance of RT 1 2 , following the terminology of Wang [START_REF] Wang | Some logically weak Ramseyan theorems[END_REF].

Proof. Given a non-∆ 0 2 set B, either B or B is not Σ 0 2 (G G ). By Theorem 4.1, for every set A, there is an infinite set H ⊆ A or H ⊆ A such that either B or B is not Σ 0,H 2 , hence such that B is not ∆ 0,H 2 . The second author asked in [24, Question 2.7] whether there is a set such that every infinite subset of it or its complement is of high degree. We answer negatively.

Corollary 4.4 For every set A, there is an infinite set H ⊆ A or H ⊆ A of non-high degree.

Proof. Apply Corollary 4.3 to B = ∅ . 4.2. Preservation of ∆ 0 2 hyperimmunities Our second application concerns the ability to prevent solutions from computing fast-growing functions. By Martin's theorem [START_REF] Martin | Classes of recursively enumerable sets and degrees of unsolvability[END_REF], a set is of high degree iff it computes a function dominating every computable function. Therefore, Corollary 4.4 already shows that an instance cannot force its solutions to compute arbitrarily fast growing functions. We shall now refine this result by proving that an instance cannot help dominating a fixed non-computably dominated function. Recall the definition of hyperimmunity. Definition 4.5. A function f dominates a function g if f (x) ≥ g(x) for every x. A function f is X-hyperimmune if it is not dominated by any X-computable function.

Theorem 4.6 Fix a ∅ -hyperimmune function f . For every set A, there is an infinite set

Fix f and A, and let A 0 = A and A 1 = A. By Jockusch and Soare [START_REF] Jockusch | Π 0 1 classes and degrees of theories[END_REF], there is a countable Turing ideal M |= WKL such that f is X-hyperimmune for every X ∈ M, and ∅ ∈ M. We build our infinite set by the notion of forcing P 1 within the Turing ideal M. Lemma 4.7 Let s be a branch in c ∈ P 1 and let ϕ 0 (G, n) and

then there is a finite set U such that

Let F be a sufficiently generic P 1 -filter and P be an F-projector. For every pair of Turing functionals Φ 0 , Φ 1 , there is some i < 2, some n and some p ∈ F [i,P ] such that

Proof. Fix some c ∈ F, and let s = P (c). Let g be the partial M-computable function which on input n searches for a finite set U such that

We have two cases. Case 1: g is total. Since f is M-hyperimmune, there is some n such that g(n) < f (n). Let U be the finite set witnessing g(n) ↓. Then c ? s Φ 0 (G , n) ↓∈ U ∨ Φ 1 (G , n) ↓∈ U . By Lemma 3.10(a), there is an s-extension d of c such that for every valid branch t of d refining the branch s of c, d [i,t]

Case 2: g is partial, say g(n) ↑ for some n. Then by Lemma 4.7, c ? s Φ 0 (G , n) ↓ ∨Φ 1 (G , n) ↓. By Lemma 3.10(b), there is an s-extension d of c such that for every valid branch t of d refining the branch s of c, d [i,t]

By genericity of F, there is such an extension d ∈ F.

Proof of Theorem 4.6. Let F be a sufficiently generic P 1 -filter and P be an F-projector. By Lemma 4.2, and by a pairing argument, there is some i < 2 such that for every Turing functional Φ, there is some p ∈ F [i,P ] such that

In particular, G = F [i,P ] is 2-generic, so by Lemma 2.30, G G is infinite, and by Lemma 2.29, f is G G -hyperimmune. By definition of P 1 , G G ⊆ A 0 or G G ⊆ A 1 . This completes the proof of Theorem 4.6.

Note that Theorem 4.6 cannot be extended to preservation of two ∅ -hyperimmune functions simultaneously, as there exists a bi-infinite set A such that, p A and p A are both ∅ -hyperimmune, where p X is the function which on input n returns the n + 1st element of X. For every infinite subset H of A, p H dominates p A , and for every infinite subset H of A dominates p A . In both cases, p A and p A cannot both be H -hyperimmune for any solution H.

Low 3 solutions

An effectivization of the forcing construction enables us to obtain lowness results for the infinite pigeonhole principle. The existence of low 2 solutions for ∆ 0 2 sets, and of low 2 cohesive sets for computable sequences of sets, was proven by Cholak, Jockusch and Slaman [3, sections 4.1 and 4.2]. The existence of low 3 cohesive sets for ∆ 0 2 sequences of sets was proven by Wang [START_REF] Wang | Cohesive sets and rainbows[END_REF]Theorem 3.4]. Wang [33, Questions 6.1 and 6.2] and the second author [START_REF] Patey | Open questions about Ramsey-type statements in reverse mathematics[END_REF]Question 5.4] asked whether such results can be generalized for every ∆ 0 n+1 instances of the pigeonhole and every ∆ 0 n instances of cohesiveness. We answer positively to both questions in the case

Theorem 4.9 For every ∆ 0 3 set A and every Q ∅ , there is an infinite set

Proof. By Simpson [30, Lemma VIII.2.9] and the relativized low basis theorem [START_REF] Jockusch | Π 0 1 classes and degrees of theories[END_REF], there is a Turing ideal M |= WKL containing ∅ , and countable coded by a set B such that B ≤ T ∅ . Let A 0 = A and A 1 = A. Consider the notion of forcing P 1 within the Turing ideal M.

Define an infinite decreasing sequence of P 1 -conditions c 0 ≥ f 0 c 1 ≥ f 1 . . . such that for every n, letting c n = (σ 0 s,n , σ 1 s,n , X s,n , C n , U s,n : s < k n ), and every s < k n , either s is not valid in c n , or there is some i < 2 such that

We claim that there is a Π 0 2 (B), hence Π 0 3 such descending sequence. Indeed, by Lemma 2.14, at a given stage n, we have a condition c n , it is Π 0 2 (B) to determine which branches are valid. Given a valid branch s, by Lemma 3.10, we can find an s-extension d such that for every valid branch t of d refining the branch s of c n , there is some side i < 2 such that the property holds. Such extension is obtained by checking whether the relation ? s holds, which is Σ 0 1 (B) by Lemma 3.9, and then finding d A ⊕ M-uniformly, hence ∅ (2) -uniformly.

The valid branches of the conditions in the sequence c 0 ≥ f 0 c 1 ≥ f 1 . . . form a Π 0 3 tree. Let F = {c 0 , c 1 , . . . }. Since Q is of PA degree above ∅ (2) , Q computes an F-projector P , that is, a function such that P (c n ) < k n is a valid branch in c n , and f n (P (c n )) = P (c n-1 ). By the pairing argument, there is a side

G ≤ T Q. This completes the proof of Theorem 4.9.

Corollary 4.10 For every ∆ 0 3 set A, there is an infinite set H ⊆ A or H ⊆ A of low 3 degree.

Proof. By the relativized low basis theorem [START_REF] Jockusch | Π 0 1 classes and degrees of theories[END_REF], there is some Q ∅ such that Q ≤ T ∅ (3) . By Theorem 4.9, there is an infinite set H ⊆ A or H ⊆ A such that H ≤ Q. In particular, H (3) ≤ T Q ≤ T ∅ (3) .

Another proof of Liu's theorem

The original computable analysis of Ramsey's theorem from Jockusch [START_REF] Carl | Ramsey's theorem and recursion theory[END_REF] produces solutions of complete degree, while the more effective proofs of Ramsey's theorem for pairs of Seetapun [START_REF] Seetapun | On the strength of Ramsey's theorem[END_REF] and Cholak, Jockusch and Slaman [START_REF] Cholak | On the strength of Ramsey's theorem for pairs[END_REF] involve a compactness argument producing solutions of PA degree. Since complete degrees are also PA, it was a long-standing open question whether Ramsey's theorem for pairs implies weak König's lemma, until answered negatively by Liu [START_REF] Liu | RT 2 2 does not imply WKL0[END_REF].

Proof. Say c = (σ s , X s , C : s < k). Define the predicate P (n, k, v) to hold if

Suppose first that the following is true for every k:

(∀n)(∃v < 2)P (n, k, v) Note that for every k, the set W k = {(n, v) : P (n, k, v)} is c.e. Therefore, there must be some n ∈ ω such that (n, Φ n (n)) ∈ W k , otherwise we would compute a {0, 1}-valued DNC function. Then in particular,

It follows that e∈C U e ∩ U ξ(e,σs) is an acceptability class. If X s ∈ e∈C U e ∩ U ξ(e,σs) , then d = (σ s , X s , C ∪ {ξ(e, σ s )}, s < k) is an s-extension of c on which the side s is not valid in d, and we are done. If X s ∈ e∈C U e ∩ U ξ(e,σs) , then there is some ρ ⊆ X s -{0, . . . , |σ|} such that Φ e (σ ∪ ρ, n) ↓= Φ n (n). The condition d = (τ s , X s {0, . . . , |ρ|}, C : s < k) defined by τ s = σ s ∪ ρ and leaving the other branches unchanged, is an s-extension of c such that d [s] (∃n)Φ e (G, n) ↓= Φ n (n).

Suppose now that there is a k such that , such that τ s j,t = σ s and Y s j,t = X s ∩ Z 0 j ∩ Z 1 t . Note that d [s j,t ] (∃n)Φ e (G, n) ↑ for every j, t < k. This completes the proof of the lemma.

Proof of Theorem 5.1. Let F be a sufficiently generic P-filter, and let P be an F-projector. Let G = {c [P (c)] : c ∈ F} and G G = {σ : (σ, X, C, ω) ∈ G}. By construction, G G ⊆ A i for some i < 2. By Lemma 5.5, G G is infinite. By Lemma 5.7, G G is of non-PA degree. This completes the proof.