Controlling iterated jumps of solutions to combinatorial problems

Abstract

Among the Ramsey-type hierarchies, namely, Ramsey’s theorem, the free set, the thin set and the rainbow Ramsey theorem, only Ramsey’s theorem is known to collapse in reverse mathematics. A promising approach to show the strictness of the hierarchies would be to prove that every computable instance at level n has a ${low}_{n}$ solution. In particular, this requires effective control of iterations of the Turing jump.

In this paper, we design some variants of Mathias forcing to construct solutions to cohesiveness, the Erdős–Moser theorem and stable Ramsey’s theorem for pairs, while controlling their iterated jumps. For this, we define forcing relations which, unlike Mathias forcing, have the same definitional complexity as the formulas they force. This analysis enables us to answer two questions of Wei Wang, namely, whether cohesiveness and the Erdős–Moser theorem admit preservation of the arithmetic hierarchy, and can be seen as a step towards the resolution of the strictness of the Ramsey-type hierarchies.

Keywords

Definability Ramsey’s theorem reverse mathematics

1. Introduction

Effective forcing is a very powerful tool in the computational analysis of mathematical statements. In this framework, lowness is achieved by deciding formulas during the forcing argument, while ensuring that the whole construction remains effective. Thus, the definitional strength of the forcing relation is very sensitive in effective forcing. We present a new forcing argument enabling one to control iterated jumps of solutions to Ramsey-type theorems. Our main motivation is reverse mathematics.

1.1. Reverse mathematics

Reverse mathematics is a vast mathematical program whose goal is to classify ordinary theorems in terms of their provability strength. It uses the framework of subsystems of second order arithmetic, which is sufficiently rich to express in a natural way many theorems. The base system, ${RCA}_{0}$ standing for Recursive Comprehension Axiom, contains the basic first order Peano arithmetic together with the $Δ_{1}^{0}$ comprehension scheme and the $Σ_{1}^{0}$ induction scheme. Thanks to the equivalence between $Δ_{1}^{0}$ -definable sets and computable sets, ${RCA}_{0}$ can be considered as capturing “computable mathematics”. The proof-theoretic analysis of the theorems in reverse mathematics is therefore closely related to their computability-theoretic content. See Simpson [19] for a formal introduction to reverse mathematics.

Early reverse mathematics results support two main empirical observations: First, many ordinary (i.e. non set-theoretic) theorems require very weak set existence axioms. Second, most of those theorems are in fact equivalent to one of four main subsystems, which together with ${RCA}_{0}$ are known as the “Big Five”. However, among the theorems studied in reverse mathematics, a notable class of theorems fails to support those observations, namely, Ramsey-type theorems. This article focuses on consequences of Ramsey’s theorem below the arithmetic comprehension axiom ( ${ACA}_{0}$ ). See Hirschfeldt [10] for a gentle introduction to the reverse mathematics below ${ACA}_{0}$ .

1.2. Controlling iterated jumps

Among the hierarchies of combinatorial principles, namely, Ramsey’s theorem [3,7,18], the rainbow Ramsey theorem [9,16,20], and the free set and thin set theorems [6,21] – only Ramsey’s theorem is known to collapse within the framework of reverse mathematics. The above mentioned hierarchies satisfy the lower bounds of Jockusch [3], that is, there exists a computable instance at every level $n ⩾ 2$ with no $Σ_{n}^{0}$ solution. Thus, a possible strategy for proving that a hierarchy is strict consists of showing the existence, for every computable instance at level n, of a ${low}_{n}$ solution.

The solutions to combinatorial principles are often built by Mathias forcing, whose forcing relation is known to be of higher definitional strength than the formula it forces [5]. Therefore there is a need for new notions of forcing with a better-behaving forcing relation. In this paper, we design three notions of forcing to construct solutions to cohesiveness, the Erdős–Moser theorem and stable Ramsey’s theorem for pairs, respectively. We define a forcing relation with the expected properties, and which formalises the first and the second jump control of Cholak, Jockusch and Slaman [7]. This can be seen as a step toward the resolution the strictness of the Ramsey-type hierarchies. We take advantage of this new analysis of Ramsey-type statements to prove two conjectures of Wang about the preservation of the arithmetic hierarchy.

1.3. Preservation of the arithmetic hierarchy

The notion of preservation of the arithmetic hierarchy has been introduced by Wang in [22], in the context of a new analysis of principles in reverse mathematics in terms of their definitional strength.

Definition 1.1 (Preservation of definitions).

A set Y preserves Ξ-definitions (relative to X) for Ξ among $Δ_{n + 1}^{0}$ , $Π_{n}^{0}$ , $Σ_{n}^{0}$ where $n > 0$ , if every properly Ξ (relative to X) set is properly Ξ relative to Y ( $X \oplus Y$ ). Y preserves the arithmetic hierarchy (relative to X) if Y preserves Ξ-definitions (relative to X) for all Ξ among $Δ_{n + 1}^{0}$ , $Π_{n}^{0}$ , $Σ_{n}^{0}$ where $n > 0$ .

Suppose that $Φ = (\forall X) (\exists Y) φ (X, Y)$ and φ is arithmetic. Φ admits preservation of Ξ-definitions if for each Z and $X ⩽_{T} Z$ there exists Y such that Y preserves Ξ-definitions relative to Z and $φ (X, Y)$ holds. Φ admits preservation of the arithmetic hierarchy if for each Z and $X ⩽_{T} Z$ there exists Y such that Y preserves the arithmetic hierarchy relative to Z and $φ (X, Y)$ holds.

The preservation of the arithmetic hierarchy seems closely related to the problem of controlling iterated jumps of solutions to combinatorial problems. Indeed, a proof of such a preservation usually consists of noticing that the forcing relation has the same strength as the formula it forces, and then deriving a diagonalization from it. See Lemma 2.16 for a case-in-point. Wang proved in [22] that weak König’s lemma ( ${WKL}_{0}$ ), the rainbow Ramsey theorem for pairs ( $RRT_{2}^{2}$ ) and the atomic model theorem ( $AMT$ ) admit preservation of the arithmetic hierarchy. He conjectured that this is also the case for cohesiveness and the Erdős–Moser theorem. We prove the two conjectures via the following concatenation of Theorems 2.2 and 3.2, where $COH$ stands for cohesiveness and $EM$ for the Erdős–Moser theorem.

Theorem 1.2.
$COH$ and $EM$ admit preservation of the arithmetic hierarchy.

1.4. Definitions and notation

Fix an integer $k \in ω$ . A string (over k) is an ordered tuple of integers $a_{0}, \dots, a_{n - 1}$ (such that $a_{i} < k$ for every $i < n$ ). The empty string is written ε. A sequence (over k) is an infinite listing of integers $a_{0}, a_{1}, \dots$ (such that $a_{i} < k$ for every $i \in ω$ ). Given $s \in ω$ , $k^{s}$ is the set of strings of length s over k and $k^{< s}$ is the set of strings of length $< s$ over k. As well, $k^{< ω}$ is the set of finite strings over k and $k^{ω}$ is the set of sequences (i.e. infinite strings) over k. Given a string $σ \in k^{< ω}$ , we use $| σ |$ to denote its length. Given two strings $σ, τ \in k^{< ω}$ , σ is a prefix of τ (written $σ ⪯ τ$ ) if there exists a string $ρ \in k^{< ω}$ such that $σ ρ = τ$ . Given a sequence X, we write $σ ≺ X$ if $σ = X ↾ n$ for some $n \in ω$ . A binary string (resp. real) is a string (resp. sequence) over 2. We may identify a real with a set of integers by considering that the real is its characteristic function.

A tree $T \subseteq k^{< ω}$ is a set downward-closed under the prefix relation. A binary tree is a set $T \subseteq 2^{< ω}$ . A set $P \subseteq ω$ is a path through T if for every $σ ≺ P$ , $σ \in T$ . A string $σ \in k^{< ω}$ is a stem of a tree T if every $τ \in T$ is comparable with σ. Given a tree T and a string $σ \in T$ , we denote by $T^{[σ]}$ the subtree ${τ \in T : τ ⪯ σ \lor τ ⪰ σ}$ .

Given two sets A and B, we denote by $A < B$ the formula $(\forall x \in A) (\forall y \in B) [x < y]$ . We write $A \subseteq^{*} B$ to mean that $A - B$ is finite, that is, $(\exists n) (\forall a \in A) (a \notin B \to a < n)$ . A Mathias condition is a pair $(F, X)$ where F is a finite set, X is an infinite set and $F < X$ . A condition $(F_{1}, X_{1})$ extends $(F, X)$ (written $(F_{1}, X_{1}) ⩽ (F, X)$ ) if $F \subseteq F_{1}$ , $X_{1} \subseteq X$ and $F_{1} ∖ F \subset X$ . A set G satisfies a Mathias condition $(F, X)$ if $F \subset G$ and $G ∖ F \subseteq X$ .

2. Cohesiveness preserves the arithmetic hierarchy

Cohesiveness plays a central role in reverse mathematics. It appears naturally in the standard proof of Ramsey’s theorem, as a preliminary step to reduce an instance of Ramsey’s theorem over $(n + 1)$ -tuples into a non-effective instance over n-tuples.

Definition 2.1 (Cohesiveness).

An infinite set C is $\vec{R}$ -cohesive for a sequence of sets $R_{0}, R_{1}, \dots$ if for each $i \in ω$ , $C \subseteq^{*} R_{i}$ or $C \subseteq^{*} \overline{R_{i}}$ . A set C is cohesive (resp. p-cohesive, r-cohesive) if it is $\vec{R}$ -cohesive where $\vec{R}$ is the sequence of all the c.e. sets (resp. primitive recursive sets, computable sets). $COH$ is the statement “Every uniform sequence of sets $\vec{R}$ admits an infinite $\vec{R}$ -cohesive set”.

Mileti [13] and Jockusch and Lempp [unpublished] proved that $COH$ is a consequence of Ramsey’s theorem for pairs over ${RCA}_{0}$ . The computational power of $COH$ is relatively well understood. A Turing degree d bounds $COH$ if every computable sequence of sets $R_{0}, R_{1}, \dots$ , has an $\vec{R}$ -cohesive set bounded by d. Jockusch and Stephan characterized in [4] the degrees bounding $COH$ as the degrees whose jump is PA relative to $\emptyset^{'}$ . The author [17] extended this characterization to an instance-wise correspondance between cohesiveness and the statement “For every $Δ_{2}^{0}$ tree T, there is a set whose jump computes a path through T”. Wang [22] conjectured that $COH$ admits preservation of the arithmetic hierarchy. We prove his conjecture by using a new forcing argument.

Theorem 2.2.
$COH$ admits preservation of the arithmetic hierarchy.

Before proving Theorem 2.2, we state an immediate corollary.
Corollary 2.3.
There exists a cohesive set preserving the arithmetic hierarchy.
Proof.
Jockusch [2] proved that every PA degree computes a sequence of sets containing, among others, all the computable sets. Wang proved in [22] that ${WKL}_{0}$ preserves the arithmetic hierarchy. Therefore there exists a uniform sequence of sets $\vec{R}$ containing all the computable sets and preserving the arithmetic hierarchy. By Theorem 2.2 relativized to $\vec{R}$ , there exists an infinite $\vec{R}$ -cohesive set C preserving the arithmetic hierarchy relative to $\vec{R}$ . In particular C is r-cohesive and preserves the arithmetic hierarchy. By [4], the degrees of r-cohesive and cohesive sets coincide. Therefore C computes a cohesive set which preserves the arithmetic hierarchy. □

Given a uniformly computable sequence of sets $R_{0}, R_{1}, \dots$ , the construction of an $\vec{R}$ -cohesive set is usually done with computable Mathias forcing, that is, using conditions $(F, X)$ in which X is computable. The construction starts with $(\emptyset, ω)$ and interleaves two kinds of steps. Given some condition $(F, X)$ :

the extension step consists of taking an element x from X and adding it to F, therefore forming the extension $(F \cup {x}, X ∖ [0, x])$ ;

the cohesiveness step consists of deciding which one of $X \cap R_{i}$ and $X \cap {\overline{R}}_{i}$ is infinite, and taking the chosen one as the new reservoir.

Cholak, Dzhafarov, Hirst and Slaman [5] studied the definitional complexity of the forcing relation for computable Mathias forcing. They proved that it has good definitional properties for the first jump, but not for iterated jumps. Indeed, given a computable Mathias condition $c = (F, X)$ and a $Σ_{1}^{0}$ formula $(\exists x) φ (G, x)$ , one can $\emptyset^{'}$ -effectively decide whether there is an extension d forcing $(\exists x) φ (G, x)$ by asking the following question:
Is there an extension $d = (E, Y) ⩽ c$ and some $n \in ω$ such that $φ (E, n)$ holds?
If there is such an extension, then we can choose it to be a finite extension, that is, such that $Y =^{*} X$ . Therefore, the question is $Σ_{1}^{0, X}$ . Consider now a $Π_{2}^{0}$ formula $(\forall x) (\exists y) φ (G, x, y)$ . The question becomes
For every extension $d ⩽ c$ and every $m \in ω$ , is there some extension $e = (E, Y) ⩽ d$ and some $n \in ω$ such that $φ (E, m, n)$ holds?
In this case, the extension d is not usually a finite extension and therefore the question cannot be presented in a $Π_{2}^{0}$ way. In particular, the formula “Y is an infinite subset of X” is definitionally complex. In general, deciding iterated jumps of a generic set requires to be able to talk about the future of a given condition, and in particular to describe by simple means the formula “d is a valid condition” and the formula “d is an extension of c”.

Thankfully, in the case of cohesiveness, we do not need the full generality of the computable Mathias forcing. Indeed, the reservoirs have a very special shape. After the first application of stage (S2), the set X is, up to finite changes, of the form $ω \cap R_{0}$ or $ω \cap \overline{R_{0}}$ . After the second application of (S2), it is in one of the following forms: $ω \cap R_{0} \cap R_{1}$ , $ω \cap R_{0} \cap {\overline{R}}_{1}$ , $ω \cap {\overline{R}}_{0} \cap R_{1}$ , $ω \cap {\overline{R}}_{0} \cap {\overline{R}}_{1}$ , and so on. More generally, after n applications of (S2), a condition $c = (F, X)$ is characterized by a pair $(F, σ)$ where σ is a string of length n representing the choices made during (S2). Given a string $σ \in 2^{< ω}$ , let $R_{σ} = ⋂_{σ (i) = 0} {\overline{R}}_{i} ⋂_{σ (i) = 1} R_{i}$ . In particular, $R_{ε} = ω$ , where ε is the empty string.

Even within this restricted partial order, the decision of the $Π_{2}^{0}$ formula remains too complicated since it requires deciding if $R_{σ}$ is infinite. However, notice that the σ’s such that $R_{σ}$ is infinite are exactly the initial segments of the $Π_{1}^{0, \emptyset^{'}}$ class $C (\vec{R})$ defined as the collection of the reals X such that $R_{σ}$ has more than $| σ |$ elements for every $σ ≺ X$ . We can therefore use a compactness argument at the second level to decrease the definitional strength of the forcing relation, as Wang [22] did for weak König’s lemma.
2.1. The forcing notion

We let $T$ denote the collection of all the infinite $\emptyset^{'}$ -primitive recursive trees T such that $[T] \subseteq C (\vec{R})$ . By $\emptyset^{'}$ -primitive recursive, we mean the class of functions obtained by adding the characteristic function of $\emptyset^{'}$ to the basic primitive recursive functions, and closing under the standard primitive recursive operations. Note that $T$ is a computable set. Given two finite sets E, F and some string $σ \in 2^{< ω}$ , we write $E ⩽_{σ} F$ to say that $F \subseteq E \subseteq F \cup (R_{σ} \cap [max F, \infty))$ . In other words, $E ⩽_{σ} F$ if and only if $(E, R_{σ})$ is a valid Mathias extension of $(F, R_{σ})$ , where $R_{σ}$ might be finite. We are now ready to defined our partial order.

Definition 2.4.
Let $P$ be the partial order whose conditions are tuples $(F, σ, T)$ where $F \subseteq ω$ is a finite set, $σ \in 2^{< ω}$ and $T \in T$ with stem σ. A condition $d = (E, τ, S)$ extends $c = (F, σ, T)$ (written $d ⩽ c$ ) if $E ⩽_{σ} F$ , $τ ⪰ σ$ and $S \subseteq T$ .

Given a condition $c = (F, σ, T)$ , the string σ imposes a finite restriction on the possible extensions of the set F. The condition c intuitively denotes the Mathias condition $(F, R_{σ} \cap (max F, \infty))$ with some additional constraints on the extensions of σ represented by the tree T. Accordingly, set G satisfies $(F, σ, T)$ if it satisfies the induced Mathias condition, that is, if $F \subseteq G \subseteq F \cup (R_{σ} \cap (max F, \infty))$ . We let $Ext (c)$ be the collection of all the extensions of c.

Note that although we did not explicitly require $R_{σ}$ to be infinite, this property holds for every condition $(F, σ, T) \in P$ . Indeed, since $[T] \subseteq C (\vec{R})$ , then $R_{τ}$ is infinite for every extensible node $τ \in T$ . Since σ is a stem of T, it is extensible and therefore $R_{σ}$ is infinite.
2.2. Preconditions and forcing $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formulas

When forcing complex formulas, we need to be able to consider all possible extensions of some condition c. Checking that some $d = (E, τ, S)$ is a valid condition extending c requires to decide whether the $\emptyset^{'}$ -p.r. tree S is infinite, which is a $Π_{2}^{0}$ question. At some point, we will need to decide a $Σ_{1}^{0}$ formula without having enough computational power to check that the tree part is infinite (see clause (ii) of Definition 2.10). As the tree part of a condition is not accurate for such formulas, we may define the corresponding forcing relation over a weaker notion of condition where the tree is not required to be infinite.

Definition 2.5 (Precondition).

A precondition is a condition $(F, σ, T)$ without the assumption that T is infinite.

In particular, $R_{σ}$ may be a finite set. The notion of condition extension can be generalized to the preconditions. The set of all preconditions is computable, contrary to the set $P$ . Given a precondition $c = (F, σ, T)$ , we denote by ${Ext}_{1} (c)$ the set of all preconditions $(E, τ, S)$ extending c such that $τ = σ$ and $T = S$ . Here, $T = S$ in a strong sense, that is, the Turing indices of T and S are the same. This fact is used in clause a) of Lemma 2.14. We let $A$ denote the collection of all the finite sets of integers. The set $A$ can be thought of as representing the set of finite approximations of the generic set G. We also fix a uniformly computable enumeration $A_{0} \subseteq A_{1} \subseteq \dots$ of finite subsets of $A$ such that $⋃_{s} A_{s} = A$ . We denote by $Apx (c)$ the set ${E \in A : (E, σ, T) \in {Ext}_{1} (c)}$ . In particular, $Apx (c)$ is collection of all finite sets E satisfying c, that is, $Apx (c) = {E \in A : E ⩽_{σ} F}$ . Last, we let ${Apx}_{s} (c) = Apx (c) \cap A_{s}$ . We start by proving a few trivial statements.

Lemma 2.6.
Fix a precondition $c = (F, σ, T)$ .
If c is a condition then ${Ext}_{1} (c) \subseteq Ext (c)$ .

If c is a condition then $Apx (c) = {E : (E, τ, S) \in Ext (c)}$ .

If d is a precondition extending c then $Apx (d) \subseteq Apx (c)$ and ${Apx}_{s} (d) \subseteq {Apx}_{s} (c)$ .

Proof.

By definition, if c is a condition, then T is infinite. If $d \in {Ext}_{1} (c)$ then $d = (E, σ, T)$ for some $E \in Apx (c)$ . As d is a precondition and T is infinite, d is a condition.

By definition, $Apx (c) = {E : (E, σ, T) \in {Ext}_{1} (c)} \subseteq {E : (E, τ, S) \in Ext (c)}$ . In the other direction, fix an extension $(E, τ, S) \in Ext (c)$ . By definition of an extension, $E ⩽_{τ} F$ , so $E ⩽_{σ} F$ . Therefore $(E, σ, T) \in {Ext}_{1} (c)$ and by definition of $Apx (c)$ , $E \in Apx (c)$ .

Fix some $(E, τ, S) \in {Ext}_{1} (d)$ . As d extends c, $τ ⪰ σ$ . By definition of an extension, $E ⩽_{τ} F$ , so $E ⩽_{σ} F$ , hence $(E, σ, T) \in {Ext}_{1} (c)$ . Therefore $Apx (d) = {E : (E, τ, S) \in {Ext}_{1} (d)} \subseteq {E : (E, σ, T) \in {Ext}_{1} (c)} = Apx (c)$ . For any $s \in ω$ , ${Apx}_{s} (d) = Apx (d) \cap A_{s} \subseteq Apx (c) \cap A_{s} = {Apx}_{s} (c)$ . □

Note that although the extension relation has been generalized to preconditions, $Ext (c)$ is defined to be the set of all the conditions extending c. In particular, if c is a precondition which is not a condition, $Ext (c) = \emptyset$ , whereas at least $c \in {Ext}_{1} (c)$ . This is why clause 1 of Lemma 2.6 gives the useful information that whenever c is a true condition, so are the members of ${Ext}_{1} (c)$ .
Definition 2.7.
Fix a precondition $c = (F, σ, T)$ and a $Σ_{0}^{0}$ formula $φ (G, x)$ .
$c ⊩ (\exists x) φ (G, x)$ iff $φ (F, w)$ holds for some $w \in ω$ ,

$c ⊩ (\forall x) φ (G, x)$ iff $φ (E, w)$ holds for every $w \in ω$ and every set $E \in Apx (c)$ .

As explained, σ restricts the possible extensions of the set F (see clause 3 of Lemma 2.6), so this forcing notion is stable by condition extension. The tree T itself restricts the possible extensions of σ, but has no effect in deciding a $Σ_{1}^{0}$ formula (Lemma 2.8).

The following trivial lemma expresses the fact that the tree part of a precondition has no effect in the forcing relation for a $Σ_{1}^{0}$ or $Π_{1}^{0}$ formula.
Lemma 2.8.
Fix two preconditions $c = (F, σ, T)$ and $d = (F, σ, S)$ , and some $Σ_{1}^{0}$ or $Π_{1}^{0}$ formula $φ (G)$ $\begin{matrix} c ⊩ φ (G) if and only if d ⊩ φ (G) . \end{matrix}$
Proof.
Simply notice that the tree part of the condition does not occur in the definition of the forcing relation, and that $Apx (c) = Apx (d)$ . □

As one may expect, the forcing relation for a precondition is closed under extension. Lemma 2.9.
Fix a precondition c and a $Σ_{1}^{0}$ or $Π_{1}^{0}$ formula $φ (G)$ . If $c ⊩ φ (G)$ then for every precondition $d ⩽ c$ , $d ⊩ φ (G)$ .
Proof.
Fix a precondition $c = (F, σ, T)$ such that $c ⊩ φ (G)$ and an extension $d = (E, τ, S) ⩽ c$ .
If $φ \in Σ_{1}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . As $c ⊩ φ (G)$ , then by clause (i) of Definition 2.7, there exists a $w \in ω$ such that $ψ (F, w)$ holds. By definition of $d ⩽ c$ , $E ⩽_{σ} F$ , so $ψ (E, w)$ holds, hence $d ⊩ φ (G)$ .

If $φ \in Π_{1}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . As $c ⊩ φ (G)$ , then by clause (ii) of Definition 2.7, for every $w \in ω$ and every $H \in Apx (c)$ , $φ (H, w)$ holds. By clause 3 of Lemma 2.6, $Apx (d) \subseteq Apx (c)$ so $d ⊩ φ (G)$ . □

2.3. Forcing higher formulas

We are now able to define the forcing relation for any arithmetic formula. The forcing relation for arbitrary arithmetic formulas is induced by the forcing relation for $Σ_{1}^{0}$ formulas. However, the definitional strength of the resulting relation is too high with respect to the formula it forces. We therefore design a custom relation with better definitional properties, and which still preserve the expected properties of a forcing relation, that is, the density of the set of conditions forcing a formula or its negation, and the preservation of the forced formulas under condition extension.

Definition 2.10.
Let $c = (F, σ, T)$ be a condition and $φ (G)$ be an arithmetic formula.
If $φ (G) = (\exists x) ψ (G, x)$ where $ψ \in Π_{n + 1}^{0}$ then $c ⊩ φ (G)$ iff there is a $w < | σ |$ such that $c ⊩ ψ (G, w)$ .

If $φ (G) = (\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ then $c ⊩ φ (G)$ iff for every $τ \in T$ , every $E \in {Apx}_{| τ |} (c)$ and every $w < | τ |$ , $(E, τ, T^{[τ]}) ⊮ \neg ψ (G, w)$ .

If $φ (G) = \neg ψ (G, x)$ where $ψ \in Σ_{n + 3}^{0}$ then $c ⊩ φ (G)$ iff $d ⊮ ψ (G)$ for every $d ⩽ c$ .

Note that in clause (ii) of Definition 2.10, there may be some $τ \in T$ such that $T^{[τ]}$ is finite, hence $(E, τ, T^{[τ]})$ is not necessarily a condition. This is where we use the generalization of forcing of $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas to preconditions. We now prove that this relation enjoys the main properties of a forcing relation.
Lemma 2.11.
Fix a condition c and an arithmetic formula $φ (G)$ . If $c ⊩ φ (G)$ then for every condition $d ⩽ c$ , $d ⊩ φ (G)$ .
Proof.
We prove by induction over the complexity of the formula $φ (G)$ that for every condition c, if $c ⊩ φ (G)$ then for every condition $d ⩽ c$ , $d ⊩ φ (G)$ . Fix a condition $c = (F, σ, T)$ such that $c ⊩ φ (G)$ and an extension $d = (E, τ, S)$ .
If $φ \in Σ_{1}^{0} \cup Π_{1}^{0}$ then it follows from Lemma 2.9.

If $φ \in Σ_{n + 2}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 1}^{0}$ . By clause (i) of Definition 2.10, there exists a $w \in ω$ such that $c ⊩ ψ (G, w)$ . By induction hypothesis, $d ⊩ ψ (G, w)$ so by clause (i) of Definition 2.10, $d ⊩ φ (G)$ .

If $φ \in Π_{2}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . By clause (ii) of Definition 2.10, for every $ρ \in T$ , every $w < | ρ |$ , and every $H \in {Apx}_{| ρ |} (c)$ , $(H, ρ, T^{[ρ]}) ⊮ \neg ψ (G, w)$ . As $S \subseteq T$ and $Apx (d) \subseteq Apx (c)$ , for every $ρ \in S$ , every $w < | ρ |$ , and every $H \in {Apx}_{| ρ |} (d)$ , $(H, ρ, T^{[ρ]}) ⊮ \neg ψ (G, w)$ . By Lemma 2.8, $(H, ρ, S^{[ρ]}) ⊮ \neg ψ (G, w)$ hence by clause (ii) of Definition 2.10, $d ⊩ φ (G)$ .

If $φ \in Π_{n + 3}^{0}$ then $φ (G)$ can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause (iii) of Definition 2.10, for every $e \in Ext (c)$ , $e ⊮ ψ (G)$ . As $Ext (d) \subseteq Ext (c)$ , for every $e \in Ext (d)$ , $e ⊮ ψ (G)$ , so by clause (iii) of Definition 2.10, $d ⊩ φ (G)$ . □

Lemma 2.12.
For every arithmetic formula φ, the following set is dense $\begin{matrix} {c \in P : c ⊩ φ (G) or c ⊩ \neg φ (G)} . \end{matrix}$
Proof.
We prove by induction over $n > 0$ that if φ is a $Σ_{n}^{0}$ ( $Π_{n}^{0}$ ) formula then the following set is dense $\begin{matrix} {c \in P : c ⊩ φ (G) or c ⊩ \neg φ (G)} . \end{matrix}$ It suffices to prove it for the case where φ is a $Σ_{n}^{0}$ formula, as the case where φ is a $Π_{n}^{0}$ formula is symmetric. Fix a condition $c = (F, σ, T)$ .
In case $n = 1$ , the formula φ is of the form $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . Suppose there exist a $w \in ω$ and a set $E \in Apx (c)$ such that $ψ (E, w)$ holds. The precondition $d = (E, σ, T)$ is a condition extending c by clause 1 of Lemma 2.6 and by definition of $Apx (c)$ . Moreover $d ⊩ (\exists x) ψ (G, x)$ by clause (i) of Definition 2.7 hence $d ⊩ φ (G)$ . Suppose now that for every $w \in ω$ and every $E \in Apx (c)$ , $ψ (E, w)$ does not hold. By clause (ii) of Definition 2.7, $c ⊩ (\forall x) \neg ψ (G, x)$ , hence $c ⊩ \neg φ (G)$ .

In case $n = 2$ , the formula φ is of the form $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . Let $\begin{matrix} S = {τ \in T : (\forall w < | τ |) (\forall E \in {Apx}_{| τ |} (c)) (E, τ, T^{[τ]}) ⊮ ψ (G, w)} . \end{matrix}$ The set S is obviously $\emptyset^{'}$ -p.r. We prove that it is a subtree of T. Suppose that $τ \in S$ and $ρ ⪯ τ$ . Fix a $w < | ρ |$ and $E \in {Apx}_{| ρ |} (c)$ . In particular $w < | τ |$ and $E \in {Apx}_{| τ |} (c)$ so $(E, τ, T^{[τ]}) ⊮ ψ (G, w)$ . Note that $(E, τ, T^{[τ]})$ is a precondition extending $(E, ρ, T^{[ρ]})$ , so by the contrapositive of Lemma 2.9, $(E, ρ, T^{[ρ]}) ⊮ ψ (G, w)$ . Therefore $ρ \in S$ . Hence S is a tree, and as $S \subseteq T$ , it is a subtree of T.

If S is infinite, then $d = (F, σ, S)$ is an extension of c such that for every $τ \in S$ , every $w < | τ |$ and every $E \in {Apx}_{| τ |} (c)$ , $(E, τ, T^{[τ]}) ⊮ ψ (G, w)$ . By Lemma 2.8, for every $E \in {Apx}_{| τ |} (c)$ , $(E, τ, S^{[τ]}) ⊮ ψ (G, w)$ and by clause 3 of Lemma 2.6, ${Apx}_{| τ |} (d) \subseteq {Apx}_{| τ |} (c)$ . Therefore, by clause (ii) of Definition 2.10, $d ⊩ (\forall x) \neg ψ (G, x)$ so $d ⊩ \neg φ (G)$ . If S is finite, then pick some $τ \in T ∖ S$ such that $T^{[τ]}$ is infinite. By choice of $τ \in T ∖ S$ , there exist a $w < | τ |$ and an $E \in {Apx}_{| τ |} (c)$ such that $(E, τ, T^{[τ]}) ⊩ ψ (G, w)$ . $d = (E, τ, T^{[τ]})$ is a valid condition extending c and by clause (i) of Definition 2.10 $d ⊩ φ (G)$ .

In case $n > 2$ , density follows from clause (iii) of Definition 2.10. □

Any sufficiently generic filter $F$ induces a unique generic real G defined by $\begin{matrix} G = ⋃ {F \in A : (F, σ, T) \in F} . \end{matrix}$ The following lemma informally asserts that the forcing relation is sound and complete. Sound because whenever a property is forced at some point, then this property actually holds over the generic real G. The forcing is also complete in that every property which holds over G is forced at some point whenever the filter is sufficiently generic.
Lemma 2.13.
Suppose that $F$ is a sufficiently generic filter and let G be the corresponding generic real. Then for each arithmetic formula $φ (G)$ , $φ (G)$ holds iff $c ⊩ φ (G)$ for some $c \in F$ .
Proof.
We prove by induction over the complexity of the arithmetic formula $φ (G)$ that $φ (G)$ holds iff $c ⊩ φ (G)$ for some $c \in F$ . Note that thanks to Lemma 2.12, it suffices to prove that if $c ⊩ φ (G)$ for some $c \in F$ then $φ (G)$ holds. Indeed, conversely if $φ (G)$ holds, then by genericity of G either $c ⊩ φ (G)$ or $c ⊩ \neg φ (G)$ for some $c \in F$ , but if $c ⊩ \neg φ (G)$ then $\neg φ (G)$ holds, contradicting the hypothesis. So $c ⊩ φ (G)$ .

We proceed by case analysis on the formula φ. Note that in the above argument, the converse of the Σ case is proved assuming the Π case. However, in our proof, we use the converse of the $Σ_{n + 3}^{0}$ case to prove the $Π_{n + 3}^{0}$ case. We need therefore to prove the converse of the $Σ_{n + 3}^{0}$ case without Lemma 2.12. Fix a condition $c = (F, σ, T) \in F$ such that $c ⊩ φ (G)$ .
If $φ \in Σ_{1}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause (i) of Definition 2.7, there exists a $w \in ω$ such that $ψ (F, w)$ holds. As $F \subseteq G$ and $G ∖ F \subseteq (max F, \infty)$ , then by continuity $ψ (G, w)$ holds, hence $φ (G)$ holds.

If $φ \in Π_{1}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause (ii) of Definition 2.7, for every $w \in ω$ and every $E \in Apx (c)$ , $ψ (E, w)$ holds. As ${E \subset_{fin} G : E \supseteq F} \subseteq Apx (c)$ , then for every $w \in ω$ , $ψ (G, w)$ holds, so $φ (G)$ holds.

If $φ \in Σ_{n + 2}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 1}^{0}$ . By clause (i) of Definition 2.10, there exists a $w \in ω$ such that $c ⊩ ψ (G, w)$ . By induction hypothesis, $ψ (G, w)$ holds, hence $φ (G)$ holds.

Conversely, suppose that $φ (G)$ holds. Then there exists a $w \in ω$ such that $ψ (G, w)$ holds, so by induction hypothesis $c ⊩ ψ (G, w)$ for some $c \in F$ , so by clause (i) of Definition 2.10, $c ⊩ φ (G)$ .

If $φ \in Π_{2}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . By clause (ii) of Definition 2.10, for every $τ \in T$ , every $w < | τ |$ , and every $E \in {Apx}_{| τ |} (c)$ , $(E, τ, T^{[τ]}) ⊮ \neg ψ (G, w)$ . Suppose by way of contradiction that $ψ (G, w)$ does not hold for some $w \in ω$ . Then by induction hypothesis, there exists a $d \in F$ such that $d ⊩ \neg ψ (G, w)$ . Let $e = (E, τ, S) \in F$ be such that $e ⊩ \neg ψ (G, w)$ , $| τ | > w$ and e extends both c and d. The condition e exists by Lemma 2.9. We can furthermore require that $E \in {Apx}_{| τ |} (c)$ , so $e ⊮ \neg ψ (G, w)$ and $e ⊩ \neg ψ (G, w)$ . Contradiction. Hence for every $w \in ω$ , $ψ (G, w)$ holds, so $φ (G)$ holds.

If $φ \in Π_{n + 3}^{0}$ then $φ (G)$ can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause (iii) of Definition 2.10, for every $d \in Ext (c)$ , $d ⊮ ψ (G)$ . By Lemma 2.11, $d ⊮ ψ (G)$ for every $d \in F$ , and by a previous case, $ψ (G)$ does not hold, so $φ (G)$ holds. □

We now prove that the forcing relation enjoys the desired definitional properties, that is, the complexity of the forcing relation is the same as the complexity of the formula forced. We start by analysing the complexity of some components of this notion of forcing. Lemma 2.14.

For every precondition c, $Apx (c)$ and ${Ext}_{1} (c)$ are $Δ_{1}^{0}$ uniformly in c.

For every condition c, $Ext (c)$ is $Π_{2}^{0}$ uniformly in c.

Proof.

Fix a precondition $c = (F, σ, T)$ . A set $E \in Apx (c)$ iff the following $Δ_{1}^{0}$ predicate holds: $\begin{matrix} (F \subseteq E) \land (\forall x \in E ∖ F) [x > max F \land x \in R_{σ}] . \end{matrix}$ Moreover, $(E, τ, S) \in {Ext}_{1} (c)$ iff the $Δ_{1}^{0}$ predicate $E \in Apx (c) \land τ = σ \land S = T$ holds. As already mentioned, the equality $S = T$ is translated into “the indices of S and T coincide” which is a $Σ_{0}^{0}$ statement.

Fix a condition $c = (F, σ, T)$ . By clause 2 of Lemma 2.6, $(E, τ, S) \in Ext (c)$ iff the following $Π_{2}^{0}$ formula holds $\begin{matrix} \begin{matrix} E \in Apx (c) \land σ ⪯ τ \\ \land (\forall ρ \in S) (\forall ξ) [ξ ⪯ ρ \to ξ \in S] & (S is a tree) \\ \land (\forall n) (\exists ρ \in 2^{n}) (ρ \in S) & (S is infinite) \\ \land (\forall ρ \in S) (σ ≺ ρ \lor ρ ⪯ σ) & (S has stem σ) \\ \land (\forall ρ \in S) (ρ \in T) & (S is a subset of T) . \end{matrix} \end{matrix}$
□
Lemma 2.15.
Fix an arithmetic formula $φ (G)$ .
Given a precondition c, if $φ (G)$ is a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula then so is the predicate $c ⊩ φ (G)$ .

Given a condition c, if $φ (G)$ is a $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula then so is the predicate $c ⊩ φ (G)$ .

Proof.
We prove our lemma by induction over the complexity of the formula $φ (G)$ . Fix a (pre)condition $c = (F, σ, T)$ .
If $φ (G) \in Σ_{1}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause (i) of Definition 2.7, $c ⊩ φ (G)$ if and only if the formula $(\exists w \in ω) ψ (F, w)$ holds. This is a $Σ_{1}^{0}$ predicate.

If $φ (G) \in Π_{1}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause (ii) of Definition 2.7, $c ⊩ φ (G)$ if and only if the formula $(\forall w \in ω) (\forall E \in Apx (c)) ψ (E, w)$ holds. By clause (a) of Lemma 2.14, this is a $Π_{1}^{0}$ predicate.

If $φ (G) \in Σ_{n + 2}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 1}^{0}$ . By clause (i) of Definition 2.10, $c ⊩ φ (G)$ if and only if the formula $(\exists w < | σ |) c ⊩ ψ (G, w)$ holds. This is a $Σ_{n + 2}^{0}$ predicate by induction hypothesis.

If $φ (G) \in Π_{2}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . By clause (ii) of Definition 2.10, $c ⊩ φ (G)$ if and only if the formula $(\forall τ \in T) (\forall w < | τ |) (\forall E \in {Apx}_{| τ |} (c)) (E, τ, T^{[τ]}) ⊮ \neg ψ (G, w)$ holds. By induction hypothesis, $(E, τ, T^{[τ]}) ⊮ \neg ψ (G, w)$ is a $Σ_{1}^{0}$ predicate, hence by clause (a) of Lemma 2.14, $c ⊩ φ (G)$ is a $Π_{2}^{0}$ predicate.

If $φ (G) \in Π_{n + 3}^{0}$ then it can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause (iii) of Definition 2.10, $c ⊩ φ (G)$ if and only if the formula $(\forall d) (d \notin Ext (c) \lor d ⊮ ψ (G))$ holds. By induction hypothesis, $d ⊮ ψ (G)$ is a $Π_{n + 3}^{0}$ predicate. Hence by clause (b) of Lemma 2.14, $c ⊩ φ (G)$ is a $Π_{n + 3}^{0}$ predicate. □

2.4. Preserving the arithmetic hierarchy

The following lemma asserts that every sufficiently generic real for this notion of forcing preserves the arithmetic hierarchy. The argument deeply relies on the fact that this notion of forcing admits a forcing relation with good definitional properties.

Lemma 2.16.
If $A \notin Σ_{n + 1}^{0}$ and $φ (G, x)$ is $Σ_{n + 1}^{0}$ , then the set of $c \in P$ satisfying the following property is dense: $\begin{matrix} [(\exists w \in A) c ⊩ \neg φ (G, w)] \lor [(\exists w \notin A) c ⊩ φ (G, w)] . \end{matrix}$
Proof.
Fix a condition $c = (F, σ, T)$ .
In case $n = 0$ , $φ (G, w)$ can be expressed as $(\exists x) ψ (G, w, x)$ where $ψ \in Σ_{0}^{0}$ . Let $U = {w \in ω : (\exists E \in Apx (c)) (\exists u) ψ (E, w, u)}$ . By clause (a) of Lemma 2.14, $U \in Σ_{1}^{0}$ , thus $U \neq A$ . Fix $w \in U Δ A$ . If $w \in U ∖ A$ then by definition of U, there exist an $E \in Apx (c)$ and a $u \in ω$ such that $ψ (E, w, u)$ holds. By definition of $Apx (c)$ and clause 1 of Lemma 2.6, $d = (E, σ, T)$ is a condition extending c. By clause (i) of Definition 2.7, $d ⊩ φ (G, w)$ . If $w \in A ∖ U$ , then for every $E \in Apx (c)$ and every $u \in ω$ , $ψ (E, w, u)$ does not hold, so by clause (ii) of Definition 2.7, $c ⊩ (\forall x) \neg ψ (G, w, x)$ , hence $c ⊩ \neg φ (G, w)$ .

In case $n = 1$ , $φ (G, w)$ can be expressed as $(\exists x) ψ (G, w, x)$ where $ψ \in Π_{1}^{0}$ . Let $U = {w \in ω : (\exists s) (\forall τ \in 2^{s} \cap T) (\exists u < s) (\exists E \in {Apx}_{s} (c)) (E, τ, T^{[τ]}) ⊩ ψ (G, w, u)}$ . By Lemma 2.15 and clause (a) of Lemma 2.14, $U \in Σ_{2}^{0}$ , thus $U \neq A$ . Fix $w \in U Δ A$ . If $w \in U ∖ A$ then by definition of U, there exist an $s \in ω$ , a $τ \in 2^{s} \cap T$ , a $u < s$ and an $E \in {Apx}_{s} (c)$ such that $T^{[τ]}$ is infinite and $(E, τ, T^{[τ]}) ⊩ ψ (G, w, u)$ . Thus $d = (E, τ, T^{[τ]})$ is a condition extending c and by clause (i) of Definition 2.10, $d ⊩ φ (G, w)$ . If $w \in A ∖ U$ , then let $S = {τ \in T : (\forall u < | τ |) (\forall E \in {Apx}_{| τ |} (c)) (E, τ, T^{[τ]}) ⊮ ψ (G, w, u)}$ . As proven in Lemma 2.12, S is a $\emptyset^{'}$ -p.r. subtree of T and by $w \notin U$ , S is infinite. Thus $d = (F, σ, S)$ is a condition extending c. By clause 3 of Lemma 2.6, $Apx (d) \subseteq Apx (c)$ , so for every $τ \in S$ , every $u < | τ |$ , and every $E \in {Apx}_{| τ |} (d)$ , $(E, τ, T^{[τ]}) ⊮ ψ (G, w, u)$ . By Lemma 2.8, $(E, τ, S^{[τ]}) ⊮ ψ (G, w, u)$ , so by clause (ii) of Definition 2.10, $d ⊩ (\forall x) \neg ψ (G, w, u)$ hence $d ⊩ \neg φ (G, w)$ .

In case $n > 1$ , let $U = {w \in ω : (\exists d \in Ext (c)) d ⊩ φ (G, w)}$ . By clause (b) of Lemmas 2.14 and 2.15, $U \in Σ_{n}^{0}$ , thus $U \neq A$ . Fix $w \in U Δ A$ . If $w \in U ∖ A$ then by definition of U, there exists a condition d extending c such that $d ⊩ φ (G, w)$ . If $w \in A ∖ U$ , then for every $d \in Ext (c) d ⊮ φ (G, w)$ so by clause (iii) of Definition 2.10, $c ⊩ \neg φ (G, w)$ . □

We are now ready to prove Theorem 2.2. Proof of Theorem 2.2.
Let C be a set and $R_{0}, R_{1}, \dots$ be a uniformly C-computable sequence of sets. Let $T_{0}$ be a $C^{'}$ -primitive recursive tree such that $[T_{0}] \subseteq C (\vec{R})$ . Let $F$ be a sufficiently generic filter containing $c_{0} = (\emptyset, ε, T_{0})$ . and let G be the corresponding generic real. By genericity, the set G is an infinite $\vec{R}$ -cohesive set. By Lemmas 2.16 and 2.15, G preserves non- $Σ_{n + 1}^{0}$ definitions relative to C for every $n \in ω$ . Therefore, by Proposition 2.2 of [22], G preserves the arithmetic hierarchy relative to C. □

3. The Erdős–Moser theorem preserves the arithmetic hierarchy

We now extend the previous result to the Erdős–Moser theorem. The Erdős–Moser theorem is a statement coming from graph theory. It can be used with the ascending descending principle ( $ADS$ ) to provide an alternative proof of Ramsey’s theorem for pairs ( $RT_{2}^{2}$ ). Indeed, every coloring $f : {[ω]}^{2} \to 2$ can be seen as a tournament R such that $R (x, y)$ holds if $x < y$ and $f (x, y) = 1$ , or $x > y$ and $f (y, x) = 0$ . Every infinite transitive subtournament induces a linear order whose infinite ascending or descending sequences are homogeneous for f.

Definition 3.1 (Erdős–Moser theorem).

A tournament T on a domain $D \subseteq ω$ is an irreflexive binary relation on D such that for all $x, y \in D$ with $x \neq y$ , exactly one of $T (x, y)$ or $T (y, x)$ holds. A tournament T is transitive if the corresponding relation T is transitive in the usual sense. A tournament T is stable if $(\forall x \in D) (\exists n) [(\forall s > n) T (x, s) \lor (\forall s > n) T (s, x)]$ . $EM$ is the statement “Every infinite tournament T has an infinite transitive subtournament”. $SEM$ is the restriction of $EM$ to stable tournaments.

Bovykin and Weiermann proved in [1] that $EM + ADS$ is equivalent to $RT_{2}^{2}$ over ${RCA}_{0}$ , and $SEM + SADS$ is equivalent to $SRT_{2}^{2}$ over ${RCA}_{0}$ . Lerman et al. [12] proceeded to a combinatorial and effective analysis of the Erdős–Moser theorem, and proved in particular that there is an ω-model of $EM$ which is not a model of $SRT_{2}^{2}$ . The author simplified their proof in [15] and showed in [16] that ${RCA}_{0} ⊢ EM \to [STS^{2} \lor COH]$ , where $STS^{2}$ stands for the stable thin set theorem for pairs. In particular, since Wang [22] proved that $STS^{2}$ does not admit preservation of the arithmetic hierarchy, Theorem 2.2 follows from Theorem 3.2. From a definitional point of view, Wang proved in [22] that $EM$ admits preservation of $Δ_{2}^{0}$ definitions and preservation of definitions beyond the $Δ_{2}^{0}$ level. He conjectured that $EM$ admits preservation of the arithmetic hierarchy. The balance of this section proves his conjecture.

Theorem 3.2.
$EM$ admits preservation of the arithmetic hierarchy.

Again, the core of the proof consists of finding a good forcing notion whose generics will preserve the arithmetic hierarchy. For simplicity, we will restrict ourselves to stable tournaments even though it is clear that the forcing notion can be adapted to arbitrary tournaments. The proof of Theorem 3.2 will be obtained by composing the proof that cohesiveness and the stable Erdős–Moser theorem admit preservation of the arithmetic hierarchy.

The following notion of minimal interval plays a fundamental role in the analysis of $EM$ . See [12] for a background analysis of $EM$ .
Definition 3.3 (Minimal interval).

Let T be an infinite tournament and $a, b \in T$ be such that $T (a, b)$ holds. The interval $(a, b)$ is the set of all $x \in T$ such that $T (a, x)$ and $T (x, b)$ hold. Let $F \subseteq T$ be a finite transitive subtournament of T. For $a, b \in F$ such that $T (a, b)$ holds, we say that $(a, b)$ is a minimal interval of F if there is no $c \in F \cap (a, b)$ , i.e., no $c \in F$ such that $T (a, c)$ and $T (c, b)$ both hold.

We must introduce an preliminary variant of Mathias forcing which is more suited to the Erdős–Moser theorem.

3.1. Erdős–Moser forcing

The following notion of Erdős–Moser forcing was implicitly first used by Lerman, Solomon and Towsner [12] to separate the Erdős–Moser theorem from stable Ramsey’s theorem for pairs. The author formalized this notion of forcing in [14] to construct a ${low}_{2}$ degree bounding the Erdős–Moser theorem.

Definition 3.4.
An Erdős–Moser condition (EM condition) for an infinite tournament R is a Mathias condition $(F, X)$ where
$F \cup {x}$ is R-transitive for each $x \in X$ ,

X is included in a minimal R-interval of F.

The Erdős–Moser extension is the usual Mathias extension. EM conditions have good properties for tournaments as shown by the following lemmas. Given a tournament R and two sets E and F, we denote by $E \to_{R} F$ the formula $(\forall x \in E) (\forall y \in F) R (x, y)$ holds. Lemma 3.5 (Patey [14]).

Fix an EM condition $(F, X)$ for a tournament R. For every $x \in F$ , ${x} \to_{R} X$ or $X \to_{R} {x}$ .

Lemma 3.6 (Patey [14]).

Fix an EM condition $c = (F, X)$ for a tournament R, an infinite subset $Y \subseteq X$ and a finite R-transitive set $F_{1} \subset X$ such that $F_{1} < Y$ and $[F_{1} \to_{R} Y \lor Y \to_{R} F_{1}]$ . Then $d = (F \cup F_{1}, Y)$ is a valid extension of c.

3.2. Partition trees

Given a string $σ \in k^{< ω}$ , we denote by ${set}_{ν} (σ)$ the set ${x < | σ | : σ (x) = ν}$ where $ν < k$ . The notion can be extended to sequences $P \in k^{ω}$ where ${set}_{ν} (P) = {x \in ω : P (x) = ν}$ .

Definition 3.7 (Partition tree).

A k-partition tree of $[t, \infty)$ for some $k, t \in ω$ is a tuple $(k, t, T)$ such that T is a subtree of $k^{< ω}$ . A partition tree is a k-partition tree of $[t, \infty)$ for some $k, t \in ω$ .

To simplify our notation, we may use the same letter T to denote both a partition tree $(k, t, T)$ and the actual tree $T \subseteq k^{< ω}$ . We then write $dom (T)$ for $[t, \infty)$ and $parts (T)$ for k. Given a p.r. partition tree T, we write $# T$ for its Turing index, and may refer to it as its code.

Definition 3.8 (Refinement).

Given a function $f : ℓ \to k$ , a string $σ \in ℓ^{< ω}$ f-refines a string $τ \in k^{< ω}$ if $| σ | = | τ |$ and for every $ν < ℓ$ , ${set}_{ν} (σ) \subseteq {set}_{f (ν)} (τ)$ . A p.r. ℓ-partition tree S of $[u, \infty)$ f-refines a p.r. k-partition tree T of $[t, \infty)$ (written $S ⩽_{f} T$ ) if $# S ⩾ # T$ , $ℓ ⩾ k$ , $u ⩾ t$ and for every $σ \in S$ , σ f-refines some $τ \in T$ .

The partition trees will act as the reservoirs in the forcing conditions defined in the next section. Consequently, refining a partition tree restricts the reservoir, as desired when extending a condition. The collection of partition trees is equipped with a partial order ⩽ such that $(ℓ, u, S) ⩽ (k, t, T)$ if there exists a function $f : ℓ \to k$ such that $S ⩽_{f} T$ . Given a k-partition tree of $[t, \infty)$ T, we say that part ν of T is acceptable if there exists a path P through T such that ${set}_{ν} (P)$ is infinite. Moreover, we say that part ν of T is empty if $(\forall σ \in T) [dom (T) \cap {set}_{ν} (σ) = \emptyset]$ . Note that each partition tree has at least one acceptable part since for every path P through T, ${set}_{ν} (P)$ is infinite for some $ν < k$ . It can also be the case that part ν of T is non-empty, while for every path P through T, ${set}_{ν} (P) \cap dom (T) = \emptyset$ . However, in this case, we can choose the infinite computable subtree $S = {σ \in T : {set}_{ν} (σ) \cap dom (T) = \emptyset}$ of T which has the same collection of infinite paths and such that part ν of S is empty.

Given a k-partition tree T, a finite set $F \subseteq ω$ and a part $ν < k$ , define $\begin{matrix} T^{[ν, F]} = {σ \in T : F \subseteq {set}_{ν} (σ) \lor | σ | < max F} . \end{matrix}$ The set $T^{[ν, F]}$ is a (possibly finite) subtree of T which id-refines T and such that $F \subseteq {set}_{ν} (P)$ for every path P through $T^{[ν, F]}$ .

We denote by $U$ the set of all ordered pairs $(ν, T)$ such that T is an infinite, primitive recursive k-partition tree of $[t, \infty)$ for some $t, k \in ω$ and $ν < k$ . The set $U$ is equipped with a partial ordering ⩽ such that $(μ, S) ⩽ (ν, T)$ if S f-refines T and $f (μ) = ν$ for some f. In this case we say that part μ of S refines part ν of T. Note that the domain of $U$ and the relation ⩽ are co-c.e. We denote by $U [T]$ the set of all $(ν, S) ⩽ (μ, T)$ for some $(μ, T) \in U$ .

Definition 3.9 (Promise for a partition tree).

Fix a p.r. k-partition tree of $[t, \infty)$ T. A class $C \subseteq U [T]$ is a promise for T if

$C$ is upward-closed under the ⩽ relation restricted to $U [T]$ ,

for every infinite p.r. partition tree $S ⩽ T$ , $(μ, S) \in C$ for some non-empty part μ of S.

A promise for T can be seen as a two-dimensional tree with at first level the acyclic digraph of refinement of partition trees. Given an infinite path in this digraph, the parts of the members of this path form an infinite, finitely branching tree. The following lemma holds for every $\emptyset^{'}$ -computable promise. However, we shall work later with conditions containing $\emptyset^{'}$ -primitive recursive promises in order to lower the definitional complexity of being a valid condition and to be able to prove Lemma 3.25. We therefore focus on $\emptyset^{'}$ -p.r. promises.

Lemma 3.10.
Let T and S be p.r. partition trees such that $S ⩽_{f} T$ for some function $f : parts (S) \to parts (T)$ and let $C$ be a $\emptyset^{'}$ -p.r. promise for T.
The predicate “T is an infinite k-partition tree of $[t, \infty)$ ” is $Π_{1}^{0}$ uniformly in T, k and t.

The relations “S f-refines T” and “part ν of S f-refines part μ of T” are $Π_{1}^{0}$ uniformly in S, T and f.

The predicate “ $C$ is a promise for T” is $Π_{2}^{0}$ uniformly in an index for $C$ and T.

Proof.

T is an infinite k-partition tree of $[t, \infty)$ if and only if the $Π_{1}^{0}$ formula $[(\forall σ \in T) (\forall τ ⪯ σ) τ \in T \cap k^{< \infty}] \land [(\forall n) (\exists τ \in k^{n}) τ \in T]$ holds.

Suppose that T is a k-partition tree of $[t, \infty)$ and S is an ℓ-partition tree of $[u, \infty)$ . S f-refines T if and only if the $Π_{1}^{0}$ formula holds: $\begin{matrix} u ⩾ t \land ℓ ⩾ k \land [(\forall σ \in S) (\exists τ \in k^{| σ |} \cap T) (\forall ν < u) {set}_{ν} (σ) \subseteq {set}_{f (ν)} (τ)] . \end{matrix}$ Part ν of S f-refines part μ of T if and only if $μ = f (ν)$ and S f-refines T.

Given $k, t \in ω$ , let $PartTree (k, t)$ denote the $Π_{1}^{0}$ set of all the infinite p.r. k-partition trees of $[t, \infty)$ . Given a k-partition tree S and a part ν of S, let $Empty (S, ν)$ denote the $Π_{1}^{0}$ formula “part ν of S is empty”, that is the formula $(\forall σ \in S) {set}_{ν} (σ) \cap dom (S) = \emptyset$ .

$C$ is a promise for T if and only if the following $Π_{2}^{0}$ formula holds: $\begin{array}{l} (\forall ℓ, u) (\forall S \in PartTree (ℓ, u)) [S ⩽ T \to ((\exists ν < ℓ) \neg Empty (S, ν) \land (ν, S) \in C)] \\ \land (\forall ℓ^{'}, u^{'}) (\forall V \in PartTree (ℓ^{'}, u^{'})) (\forall g : ℓ \to ℓ^{'}) [S ⩽_{g} V ⩽ T \\ \to (\forall ν < ℓ) ((ν, S) \in C \to (g (ν), V) \in C)] . \end{array}$
□

Given a promise $C$ for T and some infinite p.r. partition tree S refining T, we denote by $C [S]$ the set of all $(ν, S^{'}) \in C$ below some $(μ, S) \in C$ , that is, $C [S] = C \cap U [S]$ . Note that by clause (b) of Lemma 3.10, if $C$ is a $\emptyset^{'}$ -p.r. promise for T then $C [S]$ is a $\emptyset^{'}$ -p.r. promise for S.

Establishing a distinction between the acceptable parts and the non-acceptable ones requires a lot of definitional power. However, we prove that we can always find an extension where the distinction is $Δ_{2}^{0}$ . We say that an infinite p.r. partition tree T witnesses its acceptable parts if its parts are either acceptable or empty.
Lemma 3.11.
For every infinite p.r. k-partition tree T of $[t, \infty)$ , there exists an infinite p.r. k-partition tree S of $[u, \infty)$ refining T with the identity function and such that S witnesses its acceptable parts.
Proof.
Given a partition tree T, we let $I (T)$ be the set of its empty parts. Let T be a fixed infinite p.r. k-partition tree of $[t, \infty)$ . It suffices to prove that if ν is a non-empty and non-acceptable part of T, then there exists an infinite p.r. k-partition tree S refining T with the identity function, such that $ν \in I (S) ∖ I (T)$ . As $I (T) \subseteq I (S)$ and $| I (S) | ⩽ k$ , it suffices to iterate the process at most k times to obtain a refinement witnessing its acceptable parts.

So fix a non-empty and non-acceptable part ν of T. By definition of being non-acceptable, there exists a path P through T and an integer $u > max (t, {set}_{ν} (P))$ . Let $S = {σ \in T : {set}_{ν} (σ) \cap [u, \infty) = \emptyset}$ . The set S is a p.r. k-partition tree of $[u, \infty)$ refining T with the identity function and such that part ν of S is empty. Moreover, S is infinite since $P \in [S]$ . □

The following lemma strengthens clause (b) of Definition 3.9. Lemma 3.12.
Let T be a p.r. partition tree and $C$ be a promise for T. For every infinite p.r. partition tree $S ⩽ T$ , $(μ, S) \in C$ for some acceptable part μ of S.
Proof.
Fix an infinite p.r. ℓ-partition tree $S ⩽ T$ . By Lemma 3.11, there exists an infinite p.r. ℓ-partition tree $S^{'} ⩽_{id} S$ witnessing its acceptable parts. As $C$ is a promise for T and $S^{'} ⩽ T$ , there exists a non-empty (hence acceptable) part ν of $S^{'}$ such that $(ν, S^{'}) \in C$ . As $C$ is upward-closed, $(ν, S) \in C$ . □

3.3. Forcing conditions

We now describe the forcing notion for the Erdős–Moser theorem. Recall that an EM condition for an infinite tournament R is a Mathias condition $(F, X)$ where $F \cup {x}$ is R-transitive for each $x \in X$ and X is included in a minimal R-interval of F.

Definition 3.13.
We denote by $P$ the forcing notion whose conditions are tuples $(\vec{F}, T, C)$ where
T is an infinite p.r. partition tree,

$C$ is a $\emptyset^{'}$ -p.r. promise for T,

$(F_{ν}, dom (T))$ is an EM condition for R and each $ν < parts (T)$ .
A condition $d = (\vec{E}, S, D)$ extends $c = (\vec{F}, T, C)$ (written $d ⩽ c$ ) if there exists a function $f : ℓ \to k$ such that $D \subseteq C$ and the followings hold:
$(E_{ν}, dom (S))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$ .

We may think of a condition $c = (\vec{F}, T, C)$ as a collection of EM conditions $(F_{ν}, H_{ν})$ for R, where $H_{ν} = dom (T) \cap {set}_{ν} (P)$ for some path P through T. $H_{ν}$ must be infinite for at least one of the parts $ν < parts (T)$ . At a higher level, $D$ restricts the possible subtrees S and parts μ refining some part of T in the condition c. Given a condition $c = (\vec{F}, T, C)$ , we write $parts (c)$ for $parts (T)$ .
Lemma 3.14.
For every condition $c = (\vec{F}, T, C)$ and every $n \in ω$ , there exists an extension $d = (\vec{E}, S, D)$ such that $| E_{ν} | ⩾ n$ on each acceptable part ν of S.
Proof.
It suffices to prove that for every condition $c = (\vec{F}, T, C)$ and every acceptable part ν of T, there exists an extension $d = (\vec{E}, S, D)$ such that $S ⩽_{id} T$ and $| E_{ν} | ⩾ n$ . Iterating the process at most $parts (T)$ times completes the proof. Fix an acceptable part ν of T and a path P trough T such that ${set}_{ν} (P)$ is infinite. Let $F^{'}$ be an R-transitive subset of ${set}_{ν} (P) \cap dom (T)$ of size n. Such a set exists by the classical Erdős–Moser theorem. Let $\vec{E}$ be defined by $E_{μ} = F_{μ}$ if $μ \neq ν$ and $E_{ν} = F_{ν} \cup F^{'}$ otherwise. As the tournament R is stable, there exists some $u ⩾ t$ such that $(E_{ν}, [u, \infty))$ is an EM condition and therefore EM extends $(F_{ν}, dom (T))$ . Let S be the p.r. partition tree $T^{[ν, E_{ν}]}$ of $[u, \infty)$ . The condition $(\vec{E}, S, C [S])$ is the desired extension. □

Given a condition $c \in P$ , we denote by $Ext (c)$ the set of all its extensions.
3.4. The forcing relation

The forcing relation at the first level, namely, for $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas, is parameterized by some part of the tree of the considered condition. Thanks to the forcing relation we will define, we can build an infinite decreasing sequence of conditions which decide $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas effectively in $\emptyset^{'}$ . This sequence yields a $\emptyset^{'}$ -computably bounded $\emptyset^{'}$ -computable tree of (possibly empty) parts. Therefore, any PA degree relative to $\emptyset^{'}$ is sufficient to control the first jump of an infinite transitive subtournament of a stable infinite computable tournament.

We cannot do better since Kreuzer proved in [11] the existence of an infinite, stable, computable tournament with no low infinite transitive subtournament. If we ignore the promise part of a condition, the careful reader will recognize the construction of Cholak, Jockusch and Slaman [7] of a ${low}_{2}$ infinite subset of a $Δ_{2}^{0}$ set or its complement by the first jump control. The difference, which at first seems only notational, is in fact one of the key features of this notion of forcing. Indeed, forcing iterated jumps requires a definitionally weak description of the set of extensions of a condition, and it requires much less computational power to describe a primitive recursive tree than an infinite reservoir of a Mathias condition.

Definition 3.15.
Fix a condition $c = (\vec{F}, T, C)$ , a $Σ_{0}^{0}$ formula $φ (G, x)$ and a part $ν < parts (T)$ .
$c ⊩_{ν} (\exists x) φ (G, x)$ iff there exists a $w \in ω$ such that $φ (F_{ν}, w)$ holds.

$c ⊩_{ν} (\forall x) φ (G, x)$ iff for every $σ \in T$ , every $w < | σ |$ and every R-transitive set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ , $φ (F_{ν} \cup F^{'}, w)$ holds.

We start by proving some basic properties of the forcing relation over $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas. As one may expect, the forcing relation at first level is closed under the refinement relation.
Lemma 3.16.
Fix a condition $c = (\vec{F}, T, C)$ and a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula $φ (G)$ . If $c ⊩_{ν} φ (G)$ for some $ν < parts (T)$ , then for every $d = (\vec{E}, S, D) ⩽ c$ and every part μ of S refining part ν of T, $d ⊩_{μ} φ (G)$ .
Proof.
We have two cases.
If $φ \in Σ_{1}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 3.15, there exists a $w \in ω$ such that $ψ (F_{ν}, w)$ holds. By property (i) of the definition of an extension, $E_{μ} \supseteq F_{ν}$ and $(E_{μ} ∖ F_{ν}) \subset dom (T)$ , therefore $ψ (E_{μ}, w)$ holds by continuity, so by clause 1 of Definition 3.15, $d ⊩_{μ} (\exists x) ψ (G, x)$ .

If $φ \in Π_{1}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . Fix a $τ \in S$ , a $w < | τ |$ and an R-transitive set $F^{'} \subseteq dom (S) \cap {set}_{μ} (τ)$ . It suffices to prove that $φ (E_{μ} \cup F^{'})$ holds to conclude that $d ⊩_{μ} (\forall x) ψ (G, x)$ by clause 2 of Definition 3.15. By property (ii) of the definition of an extension, there exists a $σ \in T^{[ν, E_{μ}]}$ such that $| σ | = | τ |$ and ${set}_{μ} (τ) \subseteq {set}_{ν} (σ)$ . As $dom (S) \subseteq dom (T)$ , $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ . As $σ \in T^{[ν, E_{μ}]}$ , $E_{μ} \subseteq {set}_{ν} (σ)$ and by property (i) of the definition of an extension, $E_{μ} \subseteq dom (T)$ . So $E_{μ} \cup F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ . As $w < | τ | = | σ |$ and $E_{μ} \cup F^{'}$ is an R-transitive subset of $dom (T) \cap {set}_{ν} (σ)$ , then by clause 2 of Definition 3.15 applied to $c ⊩_{ν} (\forall x) ψ (G, x)$ , $φ (F_{ν} \cup (E_{μ} ∖ F_{ν}) \cup F^{'}, w)$ holds, hence $φ (E_{μ} \cup F^{'})$ holds. □

Before defining the forcing relation at higher levels, we prove a density lemma for $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas. It enables us in particular to reprove that every degree PA relative to $\emptyset^{'}$ computes the jump of an infinite R-transitive set.
Lemma 3.17.
For every $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula φ, the following set is dense $\begin{matrix} {c = (\vec{F}, T, C) \in P : (\forall ν < parts (T)) [c ⊩_{ν} φ (G) \lor c ⊩_{ν} \neg φ (G)]} . \end{matrix}$
Proof.
It suffices to prove the statement for the case where φ is a $Σ_{1}^{0}$ formula, as the case where φ is a $Π_{1}^{0}$ formula is symmetric. Fix a condition $c = (\vec{F}, T, C)$ and let $I (c)$ be the set of the parts $ν < parts (T)$ such that $c ⊮_{ν} φ (G)$ and $c ⊮_{ν} \neg φ (G)$ . If $I (c) = \emptyset$ then we are done, so suppose $I (c) \neq \emptyset$ and fix some $ν \in I (c)$ . We will construct an extension d of c such that $I (d) \subseteq I (c) ∖ {ν}$ . Iterating the operation completes the proof.

The formula φ is of the form $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . Define $f : k + 1 \to k$ as $f (μ) = μ$ if $μ < k$ and $f (k) = ν$ otherwise. Let S be the set of all $σ \in {(k + 1)}^{< ω}$ which f-refine some $τ \in T \cap k^{| σ |}$ and such that for every $w < | σ |$ , every part $μ \in {ν, k}$ and every finite R-transitive set $F^{'} \subseteq dom (T) \cap {set}_{μ} (σ)$ , $φ (F_{ν} \cup F^{'}, w)$ does not hold.

Note that S is a p.r. partition tree of $[t, \infty)$ refining T with witness function f. Suppose that S is infinite. Let $\vec{E}$ be defined by $E_{μ} = F_{μ}$ if $μ < k$ and $E_{k} = F_{ν}$ and consider the extension $d = (\vec{E}, S, C [S])$ . We claim that $ν, k \notin I (d)$ . Fix a part $μ \in {ν, k}$ of S. By definition of S, for every $σ \in S$ , every $w < | σ |$ and every R-transitive set $F^{'} \subseteq dom (S) \cap {set}_{μ} (σ)$ , $φ (E_{μ} \cup F^{'}, w)$ does not hold. Therefore, by clause 2 of Definition 3.15, $d ⊩_{μ} (\forall x) \neg ψ (G, x)$ , hence $d ⊩_{μ} \neg φ (G)$ . Note that $I (d) \subseteq I (c) ∖ {ν}$ .

Suppose now that S is finite. Fix a threshold $ℓ \in ω$ such that $(\forall σ \in S) | σ | < ℓ$ and a $τ \in T \cap k^{ℓ}$ such that $T^{[τ]}$ is infinite. Consider the 2-partition $E_{0} ⊔ E_{1}$ of ${set}_{ν} (τ) \cap dom (T)$ defined by $E_{0} = {i ⩾ t : τ (i) = ν \land (\exists n) (\forall s > n) R (i, s) holds}$ and $E_{1} = {i ⩾ t : τ (i) = ν \land (\exists n) (\forall s > n) R (s, i) holds}$ . This is a 2-partition since the tournament R is stable. As there exists no $σ \in S$ which f-refines τ, there exists a $w < ℓ$ and an R-transitive set $F^{'} \subseteq E_{0}$ or $F^{'} \subseteq E_{1}$ such that $φ (F_{ν} \cup F^{'}, w)$ holds. By choice of the partition, there exists a $t^{'} > t$ such that $F^{'} \to_{R} [t^{'}, \infty)$ or $[t^{'}, \infty) \to_{R} F^{'}$ . By Lemma 3.6, $(F_{ν} \cup F^{'}, [t^{'}, \infty))$ is a valid EM extension for $(F_{ν}, [t, \infty))$ . As $T^{[τ]}$ is infinite, $T^{[ν, F^{'}]}$ is also infinite. Let $\vec{E}$ be defined by $E_{μ} = F_{μ}$ if $μ \neq ν$ and $E_{μ} = F_{ν} \cup F^{'}$ otherwise. Let S be the k-partition tree $(k, t^{'}, T^{[ν, F^{'}]})$ . The condition $d = (\vec{E}, S, C [S])$ is a valid extension of c. By clause 1 of Definition 3.15, $d ⊩_{μ} φ (G)$ . Therefore $I (d) \subseteq I (c) ∖ {ν}$ . □

As in the previous notion of forcing, the following trivial lemma expresses the fact that the promise part of a condition has no effect in the forcing relation for a $Σ_{1}^{0}$ or $Π_{1}^{0}$ formula.
Lemma 3.18.
Fix two conditions $c = (\vec{F}, T, C)$ and $d = (\vec{F}, T, D)$ , and a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula. For every part ν of T, $c ⊩_{ν} φ (G)$ if and only if $d ⊩_{ν} φ (G)$ .
Proof.
If $φ \in Σ_{1}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 3.15, $c ⊩_{ν} φ (G)$ iff there exists a $w \in ω$ such that $ψ (F_{ν}, w)$ holds, iff $d ⊩_{ν} φ (G)$ . Similarly, if $φ \in Π_{1}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 2 of Definition 3.15, $c ⊩_{ν} φ (G)$ iff for every $σ \in T$ , every $w < | σ |$ and every R-transitive set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ , $φ (F_{ν} \cup F^{'}, w)$ holds, iff $d ⊩_{ν} φ (G)$ . □

We are now ready to define the forcing relation for an arbitrary arithmetic formula. Again, the natural forcing relation induced by the forcing of $Σ_{0}^{0}$ formulas is too complex, so we design a more effective relation which still enjoys the main properties of a forcing relation.
Definition 3.19.
Fix a condition $c = (\vec{F}, T, C)$ and an arithmetic formula $φ (G)$ .
If $φ (G) = (\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ then $c ⊩ φ (G)$ iff for every part $ν < parts (T)$ such that $(ν, T) \in C$ there exists a $w < dom (T)$ such that $c ⊩_{ν} ψ (G, w)$ .

If $φ (G) = (\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ then $c ⊩ φ (G)$ iff for every infinite p.r. $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ , every w and $\vec{E}$ smaller than $# S$ such that the followings hold
$(E_{ν}, dom (S))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$
for every $(μ, S) \in C$ , $(\vec{E}, S, C [S]) ⊮_{μ} \neg ψ (G, w)$ .

If $φ (G) = (\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ then $c ⊩ φ (G)$ iff there exists a $w \in ω$ such that $c ⊩ ψ (G, w)$ .

If $φ (G) = \neg ψ (G, x)$ where $ψ \in Σ_{n + 3}^{0}$ then $c ⊩ φ (G)$ iff $d ⊮ ψ (G)$ for every $d \in Ext (c)$ .

Notice that, unlike the forcing relation for $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas, the relation over higher formulas does not depend on the part of the relation. The careful reader will have recognized the combinatorics of the second jump control introduced by Cholak, Jockusch and Slaman in [7]. We now prove the main properties of this forcing relation.
Lemma 3.20.
Fix a condition c and a $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula $φ (G)$ . If $c ⊩ φ (G)$ then for every $d ⩽ c$ , $d ⊩ φ (G)$ .
Proof.
We prove the statement by induction over the complexity of the formula $φ (G)$ . Fix a condition $c = (\vec{F}, T, C)$ such that $c ⊩ φ (G)$ and an extension $d = (\vec{E}, S, D)$ of c.
If $φ \in Σ_{2}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . By clause 1 of Definition 3.19, for every part ν of T such that $(ν, T) \in C$ , there exists a $w < dom (T)$ such that $c ⊩_{ν} ψ (G, w)$ . Fix a part μ of S such that $(μ, S) \in D$ . As $D \subseteq C$ , $(μ, S) \in C$ . By upward-closure of $C$ , part μ of S refines some part ν of $C$ such that $(ν, T) \in C$ . Therefore by Lemma 3.16, $d ⊩_{μ} ψ (G, w)$ , with $w < dom (T) ⩽ dom (S)$ . Applying again clause 1 of Definition 3.19, we deduce that $d ⊩ (\forall x) ψ (G, x)$ , hence $d ⊩ φ (G)$ .

If $φ \in Π_{2}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . Suppose by way of contradiction that $d ⊮ (\forall x) ψ (G, x)$ . Let $f : parts (S) \to parts (T)$ witness the refinement $S ⩽ T$ . By clause 2 of Definition 3.19, there exists an infinite p.r. $k^{'}$ -partition tree $S^{'}$ , a function $g : parts (S^{'}) \to parts (S)$ , a $w \in ω$ , and $\vec{H}$ smaller than the code of $S^{'}$ such that
$(H_{ν}, dom (S^{'}))$ EM extends $(E_{g (ν)}, dom (S))$ for each $ν < parts (S^{'})$ ;

$S^{'}$ g-refines $⋂_{ν < parts (S^{'})} S^{[g (ν), H_{ν}]}$ ;

there exists a $(μ, S^{'}) \in D$ such that $(\vec{H}, S^{'}, D [S^{'}]) ⊩_{μ} \neg ψ (G, w)$ .
To deduce by clause 2 of Definition 3.19 that $c ⊮ (\forall x) ψ (G, x)$ and derive a contradiction, it suffices to prove that the same properties hold with respect to T.

By property (i) of the definition of an extension, $(E_{g (ν)}, dom (S))$ EM extends $(F_{f (g (ν))}, dom (T))$ and $(H_{ν}, dom (S^{'}))$ EM extends $(E_{g (ν)}, dom (S))$ , then $(H_{ν}, dom (S^{'}))$ EM extends $(F_{f (g (ν))}, dom (T))$ .

By property (ii) of the definition of an extension, S f-refines $⋂_{ν < parts (S^{'})} T^{[f (g (ν)), E_{g (ν)}]}$ and $S^{'}$ g-refines $⋂_{ν < parts (S^{'})} S^{[g (ν), H_{ν}]}$ , then $S^{'}$ $(g \circ f)$ -refines $⋂_{ν < parts (S^{'})} T^{[(g \circ f) (ν), H_{ν}]}$ .

As $D \subseteq C$ , there exists a part $(μ, S^{'}) \in C$ such that $(\vec{H}, S^{'}, D [S^{'}]) ⊩_{μ} \neg ψ (G, w)$ . By Lemma 3.18, $(\vec{H}, S^{'}, C [S^{'}]) ⊩_{μ} \neg ψ (G, w)$ .

If $φ \in Σ_{n + 3}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ . By clause 3 of Definition 3.19, there exists a $w \in ω$ such that $c ⊩ ψ (G, w)$ . By induction hypothesis, $d ⊩ ψ (G, w)$ so by clause 3 of Definition 3.19, $d ⊩ φ (G)$ .

If $φ \in Π_{n + 3}^{0}$ then $φ (G)$ can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause 4 of Definition 3.19, for every $e \in Ext (c)$ , $e ⊮ ψ (G)$ . As $Ext (d) \subseteq Ext (c)$ , for every $e \in Ext (d)$ , $e ⊮ ψ (G)$ , so by clause 4 of Definition 3.19, $d ⊩ φ (G)$ . □

Lemma 3.21.
For every $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula φ, the following set is dense $\begin{matrix} {c \in P : c ⊩ φ (G) or c ⊩ \neg φ (G)} . \end{matrix}$
Proof.
We prove the statement by induction over n. It suffices to treat the case where φ is a $Σ_{n + 2}^{0}$ formula, as the case where φ is a $Π_{n + 2}^{0}$ formula is symmetric. Fix a condition $c = (\vec{F}, T, C)$ .
In case $n = 0$ , the formula φ is of the form $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . Suppose there exist an infinite p.r. $k^{'}$ -partition tree S for some $k^{'} \in ω$ , a function $f : parts (S) \to parts (T)$ and a $k^{'}$ -tuple of finite sets $\vec{E}$ such that
$(E_{ν}, [ℓ, \infty))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$ ,

for each non-empty part ν of S such that $(ν, S) \in C$ , $(\vec{E}, S, C [S]) ⊩_{ν} ψ (G, w)$ for some $w < # S$ .
We can choose $dom (S)$ so that $(E_{ν}, dom (S))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ . Properties (i)–(ii) remain trivially true. By Lemma 3.16 and Lemma 3.18, property (iii) remains true too. Let $D = C [S] ∖ {(ν, S^{'}) \in C : part ν of S^{'} is empty}$ . As $C$ is an $\emptyset^{'}$ -p.r. promise for T, $C [S]$ is an $\emptyset^{'}$ -p.r. promise for S. As $D$ is obtained from $C [S]$ by removing only empty parts, $D$ is also an $\emptyset^{'}$ -p.r. promise for S. By clause 1 of Definition 3.19, $d = (\vec{E}, S, D) ⊩ (\exists x) ψ (G, x)$ hence $d ⊩ φ (G)$ .

We may choose a coding of the p.r. trees such that the code of S is sufficiently large to witness ℓ and $\vec{E}$ . So suppose now that for every infinite p.r. $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ and $\vec{E}$ smaller than the code of S such that properties (i)–(ii) hold, there exists a non-empty part ν of S such that $(ν, S) \in C$ and $(\vec{E}, S, C) ⊮_{ν} ψ (G, w)$ for every $w < ℓ$ . Let $D$ be the collection of all such $(ν, S)$ . The set $D$ is $\emptyset^{'}$ -p.r. since by Lemma 3.25, both $(\vec{E}, S, C) ⊮_{ν} ψ (G, w)$ and “part ν of S is non-empty” are $Σ_{1}^{0}$ . By Lemma 3.16 and since we require that $# S ⩾ # T$ in the definition of $S ⩽ T$ , $D$ is upward-closed under the refinement relation, hence is a promise for T. By clause 2 of Definition 3.19, $d = (\vec{F}, T, D) ⊩ (\forall x) \neg ψ (G, x)$ , hence $d ⊩ \neg φ (G)$ .

In case $n > 0$ , density follows from clause 4 of Definition 3.19. □

By Lemma 3.12, given any filter $F = {c_{0}, c_{1}, \dots}$ with $c_{s} = ({\vec{F}}_{s}, T_{s}, C_{s})$ , the set of the acceptable parts ν of $T_{s}$ such that $(ν, T_{s}) \in C_{s}$ forms an infinite, directed acyclic graph $G (F)$ . Whenever $F$ is sufficiently generic, the graph $G (F)$ has a unique infinite path P. The path P induces an infinite set $G = ⋃_{s} F_{P (s), s}$ . We call P the generic path and G the generic real.
Lemma 3.22.
Suppose that $F$ is sufficiently generic and let P and G be the generic path and the generic real, respectively. For any $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula $φ (G)$ , $φ (G)$ holds iff $c_{s} ⊩_{P (s)} φ (G)$ for some $c_{s} \in F$ .
Proof.
Fix a condition $c_{s} = (\vec{F}, T, C) \in F$ such that $c ⊩_{P (s)} φ (G)$ , and let $ν = P (s)$ .
If $φ \in Σ_{1}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 3.15, there exists a $w \in ω$ such that $ψ (F_{ν}, w)$ holds. As $ν = P (s)$ , $F_{ν} = F_{P (s)} \subseteq G$ and $G ∖ F_{ν} \subseteq (max F_{ν}, \infty)$ , so $ψ (G, w)$ holds by continuity, hence $φ (G)$ holds.

If $φ \in Π_{1}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 2 of Definition 3.15, for every $σ \in T$ , every $w < | σ |$ and every R-transitive set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ , $ψ (F_{ν} \cup F^{'}, w)$ holds. For every $F^{'} \subseteq G ∖ F_{ν}$ , and $w \in ω$ there exists a $σ \in T$ such that $w < | σ |$ and $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ . Hence $ψ (F_{ν} \cup F^{'}, w)$ holds. Therefore, for every $w \in ω$ , $ψ (G, w)$ holds, so $φ (G)$ holds.
The other direction holds by Lemma 3.17. □
Lemma 3.23.
Suppose that $F$ is sufficiently generic and let P and G be the generic path and the generic real, respectively. For any $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula $φ (G)$ , $φ (G)$ holds iff $c_{s} ⊩ φ (G)$ for some $c_{s} \in F$ .
Proof.
Assuming the reversal, we first show that if $φ (G)$ holds, then $c_{s} ⊩ φ (G)$ for some $c_{s} \in F$ . Indeed, by Lemma 3.21 and by genericity of $F$ either $c_{s} ⊩ φ (G)$ or $c_{s} ⊩ \neg φ (G)$ , but if $c ⊩ \neg φ (G)$ then $\neg φ (G)$ holds, contradicting the hypothesis. So $c_{s} ⊩ φ (G)$ . We now prove the forward implication by induction over the complexity of the formula $φ (G)$ . Fix a condition $c_{s} = (\vec{F}, T, C) \in F$ such that $c_{s} ⊩ φ (G)$ . We proceed by case analysis on φ.
If $φ \in Σ_{2}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . By clause 1 of Definition 3.19, for every part ν of T such that $(ν, T) \in C$ , there exists a $w < dom (T)$ such that $c_{s} ⊩_{ν} ψ (G, w)$ . In particular $(P (s), T) \in C$ , so $c_{s} ⊩_{P (s)} ψ (G, w)$ . By Lemma 3.22, $ψ (G, w)$ holds, hence $φ (G)$ holds.

If $φ \in Π_{2}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . By clause 2 of Definition 3.19, for every infinite $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ , every w and $\vec{E}$ smaller than the code of S such that the followings hold
$(E_{ν}, dom (S))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$
for every $(μ, S) \in C$ , $(\vec{E}, S, C [S]) ⊮_{μ} \neg ψ (G, w)$ . Suppose by way of contradiction that $ψ (G, w)$ does not hold for some $w \in ω$ . Then by Lemma 3.22, there exists a $d_{t} \in F$ such that $d_{t} ⊩_{P (t)} \neg ψ (G, w)$ . Since $F$ is a filter, there is a condition $e_{r} = (\vec{E}, S, D) \in F$ extending both $c_{s}$ and $d_{t}$ . Let $μ = P (r)$ . By choice of P, $(μ, S) \in C$ , so by clause (ii), $(\vec{E}, S, C [S]) ⊮_{μ} ψ (G, w)$ , hence by Lemma 3.18, $e_{r} ⊮_{μ} \neg ψ (G, w)$ . However, since part μ of S refines part $P (t)$ of $d_{t}$ , then by Lemma 3.16, $e_{r} ⊩_{μ} \neg ψ (G, w)$ . Contradiction. Hence for every $w \in ω$ , $ψ (G, w)$ holds, so $φ (G)$ holds.

If $φ \in Σ_{n + 3}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ . By clause 3 of Definition 3.19, there exists a $w \in ω$ such that $c_{s} ⊩ ψ (G, w)$ . By induction hypothesis, $ψ (G, w)$ holds, hence $φ (G)$ holds.

Conversely, if $φ (G)$ holds, then there exists a $w \in ω$ such that $ψ (G, w)$ holds, so by induction hypothesis $c_{s} ⊩ ψ (G, w)$ for some $c_{s} \in F$ , so by clause 3 of Definition 3.19, $c_{s} ⊩ φ (G)$ . The proof of the reversal is not redundant with the first paragraph of the proof since it is used in the next case at the same rank.

If $φ \in Π_{n + 3}^{0}$ then $φ (G)$ can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause 4 of Definition 3.19, for every $d \in Ext (c_{s})$ , $d ⊮ ψ (G)$ . By Lemma 3.20, $d ⊮ ψ (G)$ for every $d \in F$ and by the previous case, $ψ (G)$ does not hold, so $φ (G)$ holds. □

We now prove that the forcing relation has good definitional properties as we did with the notion of forcing for cohesiveness. Lemma 3.24.
For every condition c, $Ext (c)$ is $Π_{2}^{0}$ uniformly in c.
Proof.
Recall from Lemma 3.10 that given $k, t \in ω$ , $PartTree (k, t)$ denotes the $Π_{1}^{0}$ set of all the infinite p.r. k-partition trees of $[t, \infty)$ , and given a k-partition tree S and a part ν of S, the predicate $Empty (S, ν)$ denotes the $Π_{1}^{0}$ formula “part ν of S is empty”, that is, the formula $(\forall σ \in S) [{set}_{ν} (σ) \cap dom (S) = \emptyset]$ . If T is p.r. then so is $T^{[ν, H]}$ for some finite set H.

Fix a condition $c = (\vec{F}, (k, t, T), C)$ . By definition, $(\vec{H}, (k^{'}, t^{'}, S), D) \in Ext (c)$ iff the following formula holds: $\begin{matrix} \begin{matrix} (\exists f : k^{'} \to k) \\ (\forall ν < k^{'}) (H_{ν}, [t^{'}, \infty)) EM extends (F_{f (ν)}, [t, \infty)) & (Π_{1}^{0}) \\ \land S \in PartTree (k^{'}, t^{'}) \land S ⩽_{f} \underset{ν < k^{'}}{⋀} T^{[f (ν), H_{ν}]} & (Π_{1}^{0}) \\ \land D is a promise for S \land D \subseteq C & (Π_{2}^{0}) . \end{matrix} \end{matrix}$ By Lemma 3.10 and the fact that $⋀_{ν < k^{'}} T^{[f (ν), H_{ν}]}$ is p.r. uniformly in T, f, $\vec{H}$ and $k^{'}$ , the above formula is $Π_{2}^{0}$ . □
Lemma 3.25.
Fix an arithmetic formula $φ (G)$ , a condition $c = (\vec{F}, T, C)$ and a part ν of T.
If $φ (G)$ is a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula then so is the predicate $c ⊩_{ν} φ (G)$ .

If $φ (G)$ is a $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula then so is the predicate $c ⊩ φ (G)$ .

Proof.
We prove our lemma by induction over the complexity of the formula $φ (G)$ .
If $φ (G) \in Σ_{1}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 3.15, $c ⊩_{ν} φ (G)$ if and only if the formula $(\exists w \in ω) ψ (F_{ν}, w)$ holds. This is a $Σ_{1}^{0}$ predicate.

If $φ (G) \in Π_{1}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 2 of Definition 3.15, $c ⊩_{ν} φ (G)$ if and only if the formula $(\forall σ \in T) (\forall w < | σ |) (\forall F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)) [F^{'} R -transitive \to ψ (F_{ν} \cup F^{'}, w)]$ holds. This is a $Π_{1}^{0}$ predicate.

If $φ (G) \in Σ_{2}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . By clause 1 of Definition 3.19, $c ⊩ φ (G)$ if and only if the formula $(\forall ν < parts (T)) (\exists w < dom (T)) [(ν, T) \in C \to c ⊩_{ν} ψ (G, w)]$ holds. This is a $Σ_{2}^{0}$ predicate by induction hypothesis and the fact that $C$ is $\emptyset^{'}$ -computable.

If $φ (G) \in Π_{2}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . By clause 2 of Definition 3.19, $c ⊩ φ (G)$ if and only if for every infinite $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ , every w and $\vec{E}$ smaller than the code of S such that the followings hold
$(E_{ν}, dom (S))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$
for every $(μ, S) \in C$ , $(\vec{E}, S, C [S]) ⊮_{μ} \neg ψ (G, w)$ . By Lemma 3.10, properties (i)–(ii) are $Δ_{2}^{0}$ . Moreover, the predicate $(μ, S) \in C$ is $Δ_{2}^{0}$ . By induction hypothesis, $(\vec{E}, S, C) ⊮_{μ} \neg ψ (G, w)$ is $Σ_{1}^{0}$ . Therefore $c ⊩ φ (G)$ is a $Π_{2}^{0}$ predicate.

If $φ (G) \in Σ_{n + 3}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ . By clause 3 of Definition 3.19, $c ⊩ φ (G)$ if and only if the formula $(\exists w \in ω) c ⊩ ψ (G, w)$ holds. This is a $Σ_{n + 3}^{0}$ predicate by induction hypothesis.

If $φ (G) \in Π_{n + 3}^{0}$ then it can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause 4 of Definition 3.19, $c ⊩ φ (G)$ if and only if the formula $(\forall d) (d \notin Ext (c) \lor d ⊮ ψ (G))$ holds. By induction hypothesis, $d ⊮ ψ (G)$ is a $Π_{n + 3}^{0}$ predicate. By Lemma 3.24, the set $Ext (c)$ is $Π_{2}^{0}$ -computable uniformly in c, thus $c ⊩ φ (G)$ is a $Π_{n + 3}^{0}$ predicate. □

3.5. Preserving the arithmetic hierarchy

We now prove the core lemmas showing that every sufficiently generic real preserves the arithmetic hierarchy. The proof is split into two lemmas since the forcing relation for $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas depends on the part of the condition, and therefore has to be treated separately.

Lemma 3.26.
If $A \notin Σ_{1}^{0}$ and $φ (G, x)$ is $Σ_{1}^{0}$ , then the set of $c = (\vec{F}, T, C) \in P$ satisfying the following property is dense: $\begin{matrix} (\forall ν < parts (T)) [(\exists w \in A) c_{s} ⊩_{ν} \neg φ (G, w)] \lor [(\exists w \notin A) c_{s} ⊩_{ν} φ (G, w)] . \end{matrix}$
Proof.
The formula $φ (G, w)$ can be expressed as $(\exists x) ψ (G, w, x)$ where $ψ \in Σ_{0}^{0}$ . Given a condition $c = (\vec{F}, T, C)$ , let $I (c)$ be the set of the parts ν of T such that for every $w \in A$ , $c ⊮_{ν} \neg φ (G, w)$ and for every $w \in \overline{A}$ , $c ⊮_{ν} φ (G, w)$ . If $I (c) = \emptyset$ then we are done, so suppose $I (c) \neq \emptyset$ and fix some $ν \in I (c)$ . We will construct an extension d such that $I (d) \subseteq I (c) ∖ {ν}$ . Iterating the operation completes the proof.

Say that T is a k-partition tree of $[t, \infty)$ for some $k, t \in ω$ . Define $f : k + 1 \to k$ as $f (μ) = μ$ if $μ < k$ and $f (k) = ν$ otherwise. Given an integer $w \in ω$ , let $S_{w}$ be the set of all $σ \in {(k + 1)}^{< ω}$ which f-refine some $τ \in T \cap k^{| σ |}$ and such that for every $u < | σ |$ , every part $μ \in {ν, k}$ and every finite R-transitive set $F^{'} \subseteq dom (T) \cap {set}_{μ} (σ)$ , $φ (F_{ν} \cup F^{'}, w, u)$ does not hold.

The set $S_{w}$ is a p.r. (uniformly in w) partition tree of $[t, \infty)$ refining T with witness function f. Let $U = {w \in ω : S_{w} is finite}$ . $U \in Σ_{1}^{0}$ , thus $U \neq A$ . Fix some $w \in U Δ A$ . Suppose first that $w \in A ∖ U$ . By definition of U, $S_{w}$ is infinite. Let $\vec{E}$ be defined by $E_{μ} = F_{μ}$ if $μ < k$ and $E_{k} = F_{ν}$ , and consider the extension $d = (\vec{E}, S_{w}, C [S_{w}])$ . We claim that $I (d) \subseteq I (c) ∖ {ν}$ . Fix a part $μ \in {ν, k}$ of $S_{w}$ . By definition of $S_{w}$ , for every $σ \in S_{w}$ , every $u < | σ |$ and every R-transitive set $F^{'} \subseteq dom (S_{w}) \cap {set}_{μ} (σ)$ , $φ (E_{μ} \cup F^{'}, w, u)$ does not hold. Therefore, by clause 2 of Definition 3.15, $d ⊩_{μ} (\forall x) \neg ψ (G, w, x)$ , hence $d ⊩_{μ} \neg φ (G, w)$ , and this for some $w \in A$ . Thus $I (d) \subseteq I (c) ∖ {ν}$ .

Suppose now that $w \in U ∖ A$ , so $S_{w}$ is finite. Fix an $ℓ \in ω$ such that $(\forall σ \in S) | σ | < ℓ$ and a $τ \in T \cap k^{ℓ}$ such that $T^{[τ]}$ is infinite. Consider the 2-partition $E_{0} \cup E_{1}$ of ${set}_{ν} (τ) \cap dom (T)$ defined by $E_{0} = {i ⩾ t : τ (i) = ν \land (\exists n) (\forall s > n) R (i, s) holds}$ and $E_{0} = {i ⩾ t : τ (i) = ν \land (\exists n) (\forall s > n) R (s, i) holds}$ . As there exists no $σ \in S_{w}$ which f-refines τ, there exists a $u < ℓ$ and an R-transitive set $F^{'} \subseteq E_{0}$ or $F^{'} \subseteq E_{1}$ such that $φ (F_{ν} \cup F^{'}, w, u)$ holds. By choice of the partition, there exists a $t^{'} > t$ such that $F^{'} \to_{R} [t^{'}, \infty)$ or $[t^{'}, \infty) \to_{R} F^{'}$ . By Lemma 3.6, $(F_{ν} \cup F^{'}, [t^{'}, \infty))$ is a valid EM extension of $(F_{ν}, [t, \infty))$ . As $T^{[τ]}$ is infinite, $T^{[ν, F^{'}]}$ is also infinite. Let $\vec{E}$ be defined by $E_{μ} = F_{μ}$ if $μ \neq ν$ and $E_{μ} = F_{ν} \cup F^{'}$ otherwise. Let S be the k-partition tree $(k, t^{'}, T^{[ν, F^{'}]})$ . The condition $d = (\vec{E}, S, C [S])$ is a valid extension of c. By clause 1 of Definition 3.15, $d ⊩_{μ} φ (G, w)$ with $w \notin A$ . Therefore $I (d) \subseteq I (c) ∖ {ν}$ . □
Lemma 3.27.
If $A \notin Σ_{n + 2}^{0}$ and $φ (G, x)$ is $Σ_{n + 2}^{0}$ , then the set of $c \in P$ satisfying the following property is dense: $\begin{matrix} [(\exists w \in A) c ⊩ \neg φ (G, w)] \lor [(\exists w \notin A) c ⊩ φ (G, w)] . \end{matrix}$
Proof.
Fix a condition $c = (\vec{F}, T, C)$ .
In case $n = 0$ , $φ (G, w)$ can be expressed as $(\exists x) ψ (G, w, x)$ where $ψ \in Π_{1}^{0}$ . Let U be the set of integers w such that there exists an infinite p.r. $k^{'}$ -partition tree S for some $k^{'} \in ω$ , a function $f : parts (S) \to parts (T)$ and a $k^{'}$ -tuple of finite sets $\vec{E}$ such that
$(E_{ν}, [ℓ, \infty))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$ ,

for each non-empty part ν of S such that $(ν, S) \in C$ , $(\vec{E}, S, C [S]) ⊩_{ν} ψ (G, w, u)$ for some $u < # S$ .
By Lemmas 3.25 and 3.10, $U \in Σ_{2}^{0}$ , thus $U \neq A$ . Let $w \in U Δ A$ . Suppose that $w \in U ∖ A$ . We can choose $dom (S)$ so that $(E_{ν}, dom (S))$ EM extends $(F_{f (ν)}, dom (T))$ for each $ν < parts (S)$ . By Lemmas 3.16 and 3.18, properties (i)–(ii) remain true. Let $D = C [S] ∖ {(ν, S^{'}) \in C : part ν of S^{'} is empty}$ . As $C$ is an $\emptyset^{'}$ -p.r. promise for T, $C [S]$ is an $\emptyset^{'}$ -p.r. promise for S. As $D$ is obtained from $C [S]$ by removing only empty parts, $D$ is also an $\emptyset^{'}$ -p.r. promise for S. By clause 1 of Definition 3.19, $d = (\vec{E}, S, D) ⊩ (\exists x) ψ (G, w, x)$ hence $d ⊩ φ (G, w)$ for some $w \notin A$ .

We may choose a coding of the p.r. trees such that the code of S is sufficiently large to witness u and $\vec{E}$ . So suppose now that $w \in A ∖ U$ . Then for every infinite p.r. $k^{'}$ -partition tree S, every ℓ and $\vec{E}$ smaller than the code of S such that properties (i)–(ii) hold, there exists a non-empty part ν of S such that $(ν, S) \in C$ and $(\vec{E}, S, C) ⊮_{ν} ψ (G, w, u)$ for every $u < ℓ$ . Let $D$ be the collection of all such $(ν, S)$ . The set $D$ is $\emptyset^{'}$ -p.r. By Lemma 3.16 and since $# S ⩾ # T$ whenever $S ⩽_{f} T$ , $D$ is upward-closed under the refinement relation, hence it is a promise for T. By clause 2 of Definition 3.19, $d = (\vec{F}, T, D) ⊩ (\forall x) \neg ψ (G, w, x)$ , hence $d ⊩ \neg φ (G, w)$ for some $w \in A$ .

In case $n > 0$ , let $U = {w \in ω : (\exists d \in Ext (c)) d ⊩ φ (G, w)}$ . By Lemmas 3.24 and 3.25, $U \in Σ_{n + 2}^{0}$ , thus $U \neq A$ . Fix some $w \in U Δ A$ . If $w \in U ∖ A$ then by definition of U, there exists a condition d extending c such that $d ⊩ φ (G, w)$ . If $w \in A ∖ U$ , then for every $d \in Ext (c)$ , $d ⊮ φ (G, w)$ so by clause 4 of Definition 3.19, $c ⊩ \neg φ (G, w)$ . □

We are now ready to prove Theorem 3.2. It follows from the preservation of the arithmetic hierarchy for cohesiveness and the stable Erdős–Moser theorem. Proof of Theorem 3.2.
Since ${RCA}_{0} ⊢ COH \land SEM \to EM$ , then by Theorem 2.2 it suffices to prove that $SEM$ admits preservation of the arithmetic hierarchy. Fix some set C and a C-computable stable infinite tournament R. Let $C_{0}$ be the $C^{'}$ -p.r. set of all $(ν, T) \in U$ such that $(ν, T) ⩽ (0, 1^{< ω})$ . Let $F$ be a sufficiently generic filter containing $c_{0} = ({\emptyset}, 1^{< ω}, C_{0})$ . Let P and G be the corresponding generic path and generic real, respectively. By definition of a condition, the set G is R-transitive. By Lemma 3.14, G is infinite. By Lemmas 3.26 and 3.25, G preserves non- $Σ_{1}^{0}$ definitions relative to C. By Lemmas 3.27 and 3.25, G preserves non- $Σ_{n + 2}^{0}$ definitions relative to C for every $n \in ω$ . Therefore, by Proposition 2.2 of [22], G preserves the arithmetic hierarchy relative to C. □

4. $D_{2}^{2}$ preserves higher definitions

Among the Ramsey-type hierarchies, the $D$ hierarchy is conceptually the simplest one. It is therefore natural to study it in order to understand better the control of iterated jumps and focus on the core combinatorics without the technicalities specific to another hierarchy.

Definition 4.1.
For every $n, k ⩾ 1$ , $D_{k}^{n}$ is the statement “Every $Δ_{n}^{0}$ k-partition of the integers has an infinite subset in one of its parts”.

In particular, $D_{k}^{1}$ is nothing but $RT_{k}^{1}$ for computable colorings. Cholak et al. [7] proved that $D_{k}^{2}$ and stable Ramsey’s theorem for pairs and k colors ( $SRT_{k}^{2}$ ) are computably equivalent and that the proof is formalizable over ${RCA}_{0} + B Σ_{2}^{0}$ . Later, Chong et al. [8] proved that $D_{2}^{2}$ implies $B Σ_{2}^{0}$ over ${RCA}_{0}$ , showing therefore that ${RCA}_{0} ⊢ D_{k}^{2} \leftrightarrow SRT_{ℓ}^{2}$ for every $k, ℓ ⩾ 2$ . Wang [22] studied Ramsey’s theorem within his framework of preservation of definitions and proved that $D_{2}^{2}$ admits preservation of Ξ definitions simultaneously for all Ξ in ${Σ_{n + 2}^{0}, Π_{n + 2}^{0}, Δ_{n + 2}^{0} : n \in ω}$ , but not $Δ_{2}^{0}$ definitions. More precisely, he prove that $SADS$ , which is a consequence of $D_{2}^{2}$ , does not admit preservation of $Δ_{2}^{0}$ definitions. He used for this a combination of the first jump control of Cholak, Jockusch and Slaman [7] and a relativization of the preservation of the arithmetic hierarchy by ${WKL}_{0}$ .

In this section, we design a notion of forcing for $D_{2}^{2}$ with a forcing relation which has the same definitional complexity as the formula it forces. It enables us to reprove that $D_{2}^{2}$ admits preservation of Ξ definitions simultaneously for all Ξ in ${Σ_{n + 2}^{0}, Π_{n + 2}^{0}, Δ_{n + 3}^{0} : n \in ω}$ . The proof is significantly more involved than the previous proofs of preservation of the arithmetic hierarchy.
4.1. Sides of a sequence of sets

A main feature in the construction of a solution to an instance $R_{0}$ , $R_{1}$ of $D_{2}^{2}$ is the parallel construction of a subset of $R_{0}$ and a subset of $R_{1}$ . The intrinsic disjunction in the forcing argument prevents us from applying the same strategy as for the Erdős–Moser theorem and obtain a preservation of the arithmetic hierarchy. Given some $α < 2$ , we shall refer to $R_{α}$ or simply α as a side of $\vec{R}$ . We also need to define a relative notion of acceptation and emptiness of a part.

Definition 4.2.
Fix a k-partition tree T of $[t, \infty)$ and a set X. We say that part ν of T is X-acceptable if there exists a path P through T such that ${set}_{ν} (P) \cap X$ is infinite. We say that part ν of T is X-empty if $(\forall σ \in T) [dom (T) \cap {set}_{ν} (σ) \cap X = \emptyset]$ .

The intended uses of those notions will be $R_{α}$ -acceptation and $R_{α}$ -emptiness. Every partition tree has an $R_{α}$ -acceptable part for some $α < 2$ . The notion of X-emptiness is $Π_{1}^{0, X}$ , and therefore $Π_{2}^{0}$ if X is $Δ_{2}^{0}$ , which raises new problems for obtaining a forcing relation of weak definitional complexity. We would like to define a stronger notion of “witnessing its acceptable parts” and prove that for every infinite p.r. partition tree T, there is a p.r. refined tree S such that for each side α and each part ν of S, either ν is $R_{α}$ -empty in S, or ν is $R_{α}$ -acceptable. However, the resulting tree S would be $\emptyset^{'}$ -p.r. since $R_{α}$ is $\emptyset^{'}$ -computable. Thankfully, we will be able to circumvent this problem in Lemma 4.17.
4.2. Forcing conditions

Fix a $Δ_{2}^{0}$ 2-partition $R_{0} \cup R_{1} = ω$ . We now describe the notion of forcing to build an infinite subset of $R_{0}$ or of $R_{1}$ .

Definition 4.3.
We denote by $P$ the forcing notion whose conditions are tuples $((F_{ν}^{α} : α < 2, ν < k), T, C)$ where
T is an infinite, p.r. k-partition tree,

$C$ is a $\emptyset^{'}$ -p.r. promise for T,

$(F_{ν}^{α}, dom (T))$ is a Mathias condition for each $ν < k$ and $α < 2$ .
A condition $d = (\vec{E}, S, D)$ extends $c = (\vec{F}, T, C)$ (written $d ⩽ c$ ) if there exists a function $f : parts (S) \to parts (T)$ such that $D \subseteq C$ and the followings hold
$(E_{ν}^{α}, dom (S) \cap R_{α})$ Mathias extends $(F_{f (ν)}^{α}, dom (T) \cap R_{α})$ for each $ν < parts (S)$ and $α < 2$ ,

S f-refines $⋂_{ν < parts (S), α < 2} T^{[f (ν), E_{ν}^{α}]}$ .

In the whole construction, the index α indicates that we are constructing a set which is almost included in $R_{α}$ . Given a condition $c = (\vec{F}, T, C)$ , we write again $parts (c)$ for $parts (T)$ . The following lemma shows that we can force our constructed set to be infinite if we choose it among the acceptable parts.
Lemma 4.4.
For every condition $c = (\vec{F}, T, C)$ and every $n \in ω$ , there exists an extension $d = (\vec{E}, S, D)$ such that $| E_{ν}^{α} | ⩾ n$ on each $R_{α}$ -acceptable part ν of S for each $α < 2$ .
Proof.
It suffices to prove that for every condition $c = (\vec{F}, T, C)$ , every side $α < 2$ and every $R_{α}$ -acceptable part ν of T, there exists an extension $d = (\vec{E}, S, D)$ such that $S ⩽_{id} T$ and $| E_{ν}^{α} | ⩾ n$ . Iterating the process at most $parts (T) \times 2$ times completes the proof. Fix an $R_{α}$ -acceptable part ν of T and a path P through T such that ${set}_{ν} (P) \cap R_{α}$ is infinite. Let $F^{'}$ be a subset of ${set}_{ν} (P) \cap dom (T) \cap R_{α}$ of size n. Let $\vec{E}$ be defined by $E_{μ}^{β} = F_{μ}^{β}$ if $μ \neq ν \lor β \neq α$ and $E_{ν}^{α} = F_{ν}^{α} \cup F^{'}$ otherwise. Let S be the p.r. partition tree obtained from $T^{[ν, E_{ν}^{α}]}$ by restricting its domain so that $(E_{ν}^{α}, dom (S) \cap R_{α})$ Mathias extends $(F_{ν}^{α}, dom (T) \cap R_{α})$ . The condition $(\vec{E}, S, C [S])$ is the desired extension. □

Given a condition c, we denote by $Ext (c)$ the set of all its extensions.
4.3. Forcing relation

We need to define two forcing relations at the first level: the “true” forcing relation, i.e., the one having the good density properties but whose decision requires too much computational power, and a “weak” forcing relation having better computational properties, but which does not behave well with respect to the forcing. We start with the definition of the true forcing relation.

Definition 4.5 (True forcing relation).

Fix a condition $c = (\vec{F}, T, C)$ , a $Σ_{0}^{0}$ formula $φ (G, x)$ , a part $ν < parts (T)$ , and a side $α < 2$ .

$c ⊪_{ν}^{α} (\exists x) φ (G, x)$ iff there exists a $w \in ω$ such that $φ (F_{ν}^{α}, w)$ holds.

$c ⊪_{ν}^{α} (\forall x) φ (G, x)$ iff for every $σ \in T$ such that $T^{[σ]}$ is infinite, every $w < | σ |$ and every set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ) \cap R_{α}$ , $φ (F_{ν}^{α} \cup F^{'}, w)$ holds.

Given a condition c, a side $α < 2$ , a part ν of c and a $Π_{1}^{0}$ formula φ, the relation $c ⊪_{ν}^{α} φ (G)$ is $Π_{1}^{0, \emptyset^{'} \oplus R_{α}}$ , hence $Π_{2}^{0}$ as $R_{α}$ is $Δ_{2}^{0}$ . This relation enjoys the good properties of a forcing relation, that is, it is downward-closed under the refinement relation (Lemma 4.6), and the set of the conditions forcing either a $Σ_{1}^{0}$ formula or its negation is dense (Lemma 4.7).

Lemma 4.6.
Fix a condition $c = (\vec{F}, T, C)$ and a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula $φ (G)$ . If $c ⊪_{ν}^{α} φ (G)$ for some $ν < parts (T)$ and $α < 2$ , then for every $d = (\vec{E}, S, D) ⩽ c$ and every part μ of S refining part ν of T, $d ⊪_{μ}^{α} φ (G)$ .
Proof.

If $φ \in Σ_{1}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 4.5, there exists a $w \in ω$ such that $ψ (F_{ν}^{α}, w)$ holds. By property (i) of the definition of an extension, $E_{μ}^{α} \supseteq F_{ν}^{α}$ and $(E_{μ}^{α} ∖ F_{ν}^{α}) \subset dom (T) \cap R_{α}$ , therefore by continuity $ψ (E_{μ}^{α}, w)$ holds, so by clause 1 of Definition 4.5, $d ⊪_{μ}^{α} (\exists x) ψ (G, x)$ .

If $φ \in Π_{1}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . Fix a $τ \in S$ such that $S^{[τ]}$ is infinite, a $w < | τ |$ and a set $F^{'} \subseteq dom (S) \cap {set}_{μ} (τ) \cap R_{α}$ . Let f be the function witnessing $d ⩽ c$ . By property (ii) of the definition of an extension, τ f-refines a $σ \in T^{[ν, E_{μ}^{α}]}$ . We claim that we can even choose σ to be extendible in $T^{[ν, E_{μ}^{α}]}$ . Indeed, since τ is extendible in S, let P be a path through S extending τ and let U be the set of σ’s in T such that $P ↾ s$ f-refines σ for some s. The set U is an infinite subtree of T. Let σ be a string of length $| τ |$ and extendible in U, hence in T. By definition of U, τ f-refines σ. By definition of a refinement, such that $| σ | = | τ |$ and ${set}_{μ} (τ) \subseteq {set}_{ν} (σ)$ . As $w < | τ |$ and $dom (S) \subseteq dom (T)$ , $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ) \cap R_{α}$ . As $σ \in T^{[ν, E_{μ}^{α}]}$ , $E_{μ}^{α} \subseteq {set}_{ν} (σ)$ and by property (i) of the definition of an extension, $E_{μ}^{α} \subseteq dom (T) \cap R_{α}$ so $E_{μ}^{α} \subseteq dom (T) \cap R_{α}$ . Therefore $E_{μ}^{α} \cup F^{'} \subseteq dom (T) \cap {set}_{ν} (σ) \cap R_{α}$ . By clause 2 of Definition 4.5 applied to $c ⊪_{ν}^{α} (\forall x) ψ (G, x)$ , $ψ (F_{ν}^{α} \cup (E_{μ}^{α} ∖ F_{ν}^{α}) \cup F^{'}, w)$ holds, hence $ψ (E_{μ}^{α} \cup F^{'}, w)$ holds and still by clause 2 of Definition 4.5, $d ⊪_{μ} (\forall x) ψ (G, x)$ . □

Lemma 4.7.
For every $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula φ, the following set is dense in $P$ : $\begin{matrix} {c \in P : (\forall ν < parts (c)) (\forall α < 2) [c ⊪_{ν}^{α} φ (G) or c ⊪_{ν}^{α} \neg φ (G)]} . \end{matrix}$
Proof.
It suffices to prove the statement for the case where φ is a $Σ_{1}^{0}$ formula, as the case where φ is a $Π_{1}^{0}$ formula is symmetric. Fix a condition $c = (\vec{F}, T, C)$ and let $I (c)$ be the set of pairs $(ν, α) \in parts (T) \times 2$ such that $c {⊪̸}_{ν}^{α} φ (G)$ and $c {⊪̸}_{ν}^{α} \neg φ (G)$ . If $I (c) = \emptyset$ we are done, so suppose $I (c) \neq \emptyset$ . Fix some $(α, ν) \in I (c)$ . We will construct an extension d such that $I (d) \subseteq I (c) ∖ {(α, ν)}$ . Iterating the operation completes the proof.

The formula φ is of the form $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . Suppose there exists a $σ \in T$ such that $T^{[σ]}$ is infinite, a $w < | σ |$ and a set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ) \cap R_{α}$ such that $ψ (F_{ν}^{α} \cup F^{'}, w)$ holds. In this case, letting $\vec{E}$ be defined by $E_{μ}^{β} = F_{μ}^{β}$ if $μ \neq ν \lor β \neq α$ and $E_{ν}^{α} = F_{ν}^{α} \cup F^{'}$ , and letting S be the tree $T^{[σ]}$ where the domain is restricted so that $(E_{ν}^{α}, dom (S))$ Mathias extends $(F_{ν}^{α}, dom (T))$ , by clause 1 of Definition 4.5, the condition $d = (\vec{E}, S, C [S])$ is a valid extension of c such that $d_{ν}^{α} ⊪ φ (G)$ .

Suppose now that for every $σ \in T$ such that $T^{[σ]}$ is infinite, every $w < | σ |$ and every set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ) \cap R_{α}$ , $ψ (F_{ν}^{α} \cup F^{'}, w)$ does not hold. In this case, by clause 2 of Definition 4.5, $c ⊪_{ν}^{α} \neg φ (G)$ . □

We now define the weak forcing relation which is almost the same as the true one, except that the set $F^{'}$ is not required to be a subset of $R_{α}$ and that $T^{[σ]}$ might be finite. Because of this, whenever a condition forces a $Π_{1}^{0}$ formula by the weak forcing relation, so does it by the strong forcing relation.
Definition 4.8 (Weak forcing relation).

Fix a condition $c = (\vec{F}, T, C)$ , a $Σ_{0}^{0}$ formula $φ (G, x)$ , a part $ν < parts (T)$ and a side $α < 2$ .

$c ⊩_{ν}^{α} (\exists x) φ (G, x)$ iff there exists a $w \in ω$ such that $φ (F_{ν}^{α}, w)$ holds.

$c ⊩_{ν}^{α} (\forall x) φ (G, x)$ iff for every $σ \in T$ , every $w < | σ |$ and every set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ , $φ (F_{ν}^{α} \cup F^{'}, w)$ holds.

As one may expect, the weak forcing relation at the first level is also closed under the refinement relation.

Lemma 4.9.
Fix a condition $c = (\vec{F}, T, C)$ and a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula $φ (G)$ . If $c ⊩_{ν}^{α} φ (G)$ for some $ν < parts (T)$ and $α < 2$ , then for every $d = (\vec{E}, S, D) ⩽ c$ and every part μ of S refining part ν of T, $d ⊩_{μ}^{α} φ (G)$ .
Proof.

If $φ \in Σ_{1}^{0}$ then this is exactly clause 1 of Lemma 4.6 since the definition of the weak and the true forcing relations coincide for $Σ_{1}^{0}$ formulas.

If $φ \in Π_{1}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . Fix a $τ \in S$ , a $w < | τ |$ and a set $F^{'} \subseteq dom (S) \cap {set}_{μ} (τ)$ . By property (ii) of the definition of an extension, there exists a $σ \in T^{[ν, E_{μ}^{α}]}$ such that $| σ | = | τ |$ and ${set}_{μ} (τ) \subseteq {set}_{ν} (σ)$ . As $w < | τ |$ and $dom (S) \subseteq dom (T)$ , $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ . As $σ \in T^{[ν, E_{μ}^{α}]}$ , $E_{μ}^{α} \subseteq {set}_{ν} (σ)$ and by property (i) of the definition of an extension, $E_{μ}^{α} \subseteq dom (T)$ . Therefore $E_{μ}^{α} \cup F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ . By clause 2 of Definition 4.8 applied to $c ⊩_{ν}^{α} (\forall x) ψ (G, x)$ , $ψ (F_{ν}^{α} \cup (E_{μ}^{α} ∖ F_{ν}^{α}) \cup F^{'}, w)$ holds, hence $ψ (E_{μ}^{α} \cup F^{'}, w)$ holds and still by clause 2 of Definition 4.8, $d ⊩_{μ}^{α} (\forall x) ψ (G, x)$ . □

The following trivial lemma simply reflects the fact that the promise $C$ is not part of the definition of the weak forcing relation for $Σ_{1}^{0}$ or $Π_{1}^{0}$ formulas, and therefore has no effect on it.
Lemma 4.10.
Fix two conditions $c = (\vec{F}, T, C)$ and $d = (\vec{E}, T, D)$ and a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula. For every part ν of T such that $F_{ν}^{α} = E_{ν}^{α}$ , $c ⊩_{ν}^{α} φ (G)$ if and only if $d ⊩_{ν}^{α} φ (G)$ .
Proof.
If $φ \in Σ_{1}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 4.8, $c ⊩_{ν}^{α} φ (G)$ iff there exists a $w \in ω$ such that $ψ (F_{ν}^{α}, w)$ holds. As $F_{ν}^{α} = E_{ν}^{α}$ , $c ⊩_{ν}^{α} φ (G)$ iff $d ⊩_{ν}^{α} φ (G)$ . Similarly, if $φ \in Π_{1}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 2 of Definition 4.8, $c ⊩_{ν}^{α} φ (G)$ iff for every $σ \in T$ , every $w < | σ |$ and every set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ , $ψ (F_{ν}^{α} \cup F^{'}, w)$ holds. As $F_{ν}^{α} = E_{ν}^{α}$ , $c ⊩_{ν}^{α} φ (G)$ iff $d ⊩_{ν}^{α} φ (G)$ . □

We can now define the forcing relation over higher formulas. It is defined inductively, starting with $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas. We extend the weak forcing relation instead of the true one for effectiveness purposes. We shall see later that the weak forcing relation behaves like the true one for some parts and some sides of a condition, and therefore that it tells us something about the truth of the formula over some carefully defined generic real G. Note that the forcing relation over higher formulas is still parameterized by the side α of the condition.
Definition 4.11.
Fix a condition $c = (\vec{F}, T, C)$ , a side $α < 2$ and an arithmetic formula $φ (G)$ .
If $φ (G) = (\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ then $c ⊩^{α} φ (G)$ iff for every part ν of T such that $(ν, T) \in C$ there exists a $w < dom (T)$ such that $c ⊩_{ν}^{α} ψ (G, w)$ .

If $φ (G) = (\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ then $c ⊩^{α} φ (G)$ iff for every infinite p.r. $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ , every w and $\vec{E}$ smaller than $# S$ such that the followings hold
$E_{ν}^{β} = F_{f (ν)}^{β}$ for each $ν < parts (S)$ and $β \neq α$ ,

$(E_{ν}^{α}, dom (S) \cap R_{α})$ Mathias extends $(F_{f (ν)}^{α}, dom (T) \cap R_{α})$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}^{α}]}$
for every $(μ, S) \in C$ , $(\vec{E}, S, C [S]) ⊮_{μ}^{α} \neg ψ (G, w)$ .

If $φ (G) = (\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ then $c ⊩^{α} φ (G)$ iff there exists a $w \in ω$ such that $c ⊩^{α} ψ (G, w)$ .

If $φ (G) = \neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ then $c ⊩^{α} φ (G)$ iff $d ⊮^{α} ψ (G)$ for every $d \in Ext (c)$ .

Note that clause 2(ii) of Definition 4.11 seems to be $Π_{2}^{0}$ since $R_{α}$ is $Δ_{2}^{0}$ . However, in fact, one just needs to ensure that $dom (S) \subseteq dom (T)$ and $E_{ν}^{α} ∖ F_{f (ν)}^{α} \subseteq dom (T) \cap R_{α}$ . This is a $Δ_{2}^{0}$ predicate, and so is its negation, so one can already easily check that the forcing relation over a $Π_{2}^{0}$ formula will be also $Π_{2}^{0}$ . Before proving the usual properties about the forcing relation, we need to discuss the role of the sides in the forcing relation. We are now ready to prove that the forcing relation is closed under extension.
Lemma 4.12.
Fix a condition c, a side $α < 2$ and a $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula $φ (G)$ . If $c ⊩^{α} φ (G)$ then for every $d ⩽ c$ , $d ⊩^{α} φ (G)$ .
Proof.
We prove the statement by induction over the complexity of the formula $φ (G)$ . Fix a condition $c = (\vec{F}, T, C)$ and a side $α < 2$ such that $c ⊩^{α} φ (G)$ . Fix an extension $d = (\vec{E}, S, D)$ of c.
If $φ \in Σ_{2}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . By clause 1 of Definition 4.11, for every part ν of T such that $(ν, T) \in C$ , there exists a $w < dom (T)$ such that $c ⊩_{ν}^{α} ψ (G, w)$ . Fix a part μ of S such that $(μ, S) \in D$ . As $D \subseteq C$ , $(μ, S) \in C$ . By upward-closure of $C$ , part μ of S refines some part ν of $C$ such that $(ν, T) \in C$ . Therefore by Lemma 4.9, $d ⊩_{μ}^{α} ψ (G, w)$ , with $w < dom (T) ⩽ dom (S)$ . Applying again clause 1 of Definition 4.11, we deduce that $d ⊩ (\forall x) ψ (G, x)$ , hence $d ⊩^{α} φ (G)$ .

If $φ \in Π_{2}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . Suppose by way of contradiction that $d ⊮^{α} (\forall x) ψ (G, x)$ . Let $f : parts (S) \to parts (T)$ witness the refinement $S ⩽ T$ . By clause 2 of Definition 4.11, there exist an infinite p.r. $k^{'}$ -partition tree $S^{'}$ , a function $g : parts (S^{'}) \to parts (S)$ , a $w \in ω$ , and a $2 k^{'}$ -tuple of finite sets $\vec{H}$ smaller than the code of $S^{'}$ such that
$H_{ν}^{β} = E_{g (ν)}^{β}$ for each $ν < parts (S^{'})$ and $β \neq α$ ,

$(H_{ν}^{α}, dom (S^{'}) \cap R_{α})$ Mathias extends $(E_{g (ν)}^{α}, dom (S) \cap R_{α})$ for each $ν < parts (S^{'})$ ,

$S^{'}$ g-refines $⋂_{ν < parts (S^{'})} S^{[g (ν), H_{ν}^{α}]}$ ,

there exists a $(μ, S^{'}) \in D$ such that $(\vec{H}, S^{'}, D [S^{'}]) ⊩_{μ}^{α} \neg ψ (G, w)$ .
To deduce by clause 2 of Definition 4.11 that $c ⊮^{α} (\forall x) ψ (G, x)$ and derive a contradiction, it suffices to prove that the same properties hold with respect to T. Let ${\vec{H}}^{'}$ be defined by $H_{ν}^{^{'} β} = F_{f (g (ν))}^{β}$ for each $ν < parts (S^{'})$ and $β \neq α$ and $H_{ν}^{^{'} α} = H_{ν}^{α}$ .

It trivially holds by choice of ${\vec{H}}^{'}$ .

By property (i) of the definition of an extension, $(E_{g (ν)}^{α}, dom (S))$ Mathias extends $(F_{f (g (ν))}^{α}, dom (T))$ . Moreover $(H_{ν}^{α}, dom (S^{'}))$ Mathias extends $(E_{g (ν)}^{α}, dom (S))$ , so $(H_{ν}^{^{'} α}, dom (S^{'})) = (H_{ν}^{α}, dom (S^{'}))$ Mathias extends $(F_{f (g (ν))}, dom (T))$ .

As by property (ii) of the definition of an extension, $\begin{array}{l} S f -refines ⋂_{ν < parts (S^{'})} T^{[f (g (ν)), E_{g (ν)}^{α}]}, and \\ S^{'} g -refines ⋂_{ν < parts (S^{'})} S^{[g (ν), H_{ν}^{α}]} then \\ S^{'} (g \circ f) -refines ⋂_{ν < parts (S^{'})} T^{[g (ν), H_{ν}^{^{'} α}]} . \end{array}$

As $D \subseteq C$ , there exists a part $(μ, S^{'}) \in C$ such that $(\vec{H}, S^{'}, D [S^{'}]) ⊩_{μ}^{α} \neg ψ (G, w)$ . By Lemma 4.10, $({\vec{H}}^{'}, S^{'}, C [S^{'}]) ⊩_{μ}^{α} \neg ψ (G, w)$ .

If $φ \in Σ_{n + 3}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ . By clause 3 of Definition 4.11, there exists a $w \in ω$ such that $c ⊩^{α} ψ (G, w)$ . By induction hypothesis, $d ⊩^{α} ψ (G, w)$ so by clause 3 of Definition 4.11, $d ⊩^{α} φ (G)$ .

If $φ \in Π_{n + 3}^{0}$ then $φ (G)$ can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . Suppose by way of contradiction that $d ⊮^{α} φ (G)$ . By clause 4 of Definition 4.11, there exists an $e \in Ext (d)$ such that $e ⊩^{α} ψ (G)$ . In particular, $e \in Ext (c)$ , so by clause 4 of Definition 4.11, $e ⊮^{α} ψ (G)$ since $c ⊩^{α} φ (G)$ . Contradiction. □

Although the weak forcing relation does not satisfy the density property, the forcing relation over higher formulas does. The reason is that the extended forcing relation does not involve the weak forcing relation over $Σ_{1}^{0}$ formulas in the clause 2 of Definition 4.11, but uses instead the weaker statement “c does not force the negation of the $Σ_{1}^{0}$ formula”. The link between this statement and the statement “c has an extension which forces the $Σ_{1}^{0}$ formula” is used when proving that $φ (G)$ holds iff $c ⊩ φ (G)$ for some condition belonging to a sufficiently generic filter. We now prove the density of the forcing relation for higher formulas.
Lemma 4.13.
For every $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula φ, the following set is dense in $P$ : $\begin{matrix} {c \in P : (\forall α < 2) [c ⊩^{α} φ (G) or c ⊩^{α} \neg φ (G)]} . \end{matrix}$
Proof.
We prove the statement by induction over n. It suffices to treat the case where φ is a $Σ_{n + 2}^{0}$ formula, as the case where φ is a $Π_{n + 2}^{0}$ formula is symmetric. Moreover, it is enough to prove that for every condition c and every $α < 2$ , there exists an extension $d ⩽ c$ such that $d ⊩^{α} φ (G)$ or $d ⊩^{α} \neg φ (G)$ . Iterating the process at most twice completes the proof. Fix a condition $c = (\vec{F}, T, C)$ and a part $α < 2$ .
In case $n = 0$ , the formula φ is of the form $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . Suppose there exists an infinite p.r. $k^{'}$ -partition tree S for some $k^{'} \in ω$ , a function $f : parts (S) \to parts (T)$ , and a $2 k^{'}$ -tuple of finite sets $\vec{E}$ such that
$E_{ν}^{β} = F_{f (ν)}^{β}$ for each $ν < parts (S)$ and $β \neq α$ ,

$(E_{ν}^{α}, dom (S) \cap R_{α})$ Mathias extends $(F_{f (ν)}^{α}, dom (T) \cap R_{α})$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}^{α}]}$ ,

for each non-empty part ν of S such that $(ν, S) \in C$ , $(\vec{E}, S, C [S]) ⊩_{ν}^{α} ψ (G, w)$ for some $w < # S$ .
Let $D = C [S] ∖ {(ν, S^{'}) \in C : part ν of S^{'} is empty}$ . As $C$ is an $\emptyset^{'}$ -p.r. promise for T, $C [S]$ is an $\emptyset^{'}$ -p.r. promise for S. As $D$ is obtained from $C [S]$ by removing only empty parts, $D$ is also an $\emptyset^{'}$ -p.r. promise for S. By clause 1 of Definition 4.11, $d = (\vec{E}, S, D) ⊩^{α} (\exists x) ψ (G, x)$ hence $d ⊩^{α} φ (G)$ .

We may choose a coding of the p.r. trees such that the code of S is sufficiently large to witness f, ℓ and $\vec{E}$ . So suppose now that for every infinite p.r. $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ , $ℓ \in ω$ and $\vec{E}$ smaller than the code of S such that properties i-iii) hold, there exists a non-empty part ν of S such that $(ν, S) \in C$ and $(\vec{E}, S, C [S]) ⊮_{ν}^{α} ψ (G, w)$ for every $w < ℓ$ . Let $D$ be the collection of all such $(ν, S)$ . $D$ is $\emptyset^{'}$ -p.r. By Lemma 4.9 and since we require that $# S ⩾ # T$ in the definition of $S ⩽ T$ , $D$ is upward-closed, hence is a promise for T. By clause 2 of Definition 4.11, $d = (\vec{F}, T, D) ⊩^{α} (\forall x) \neg ψ (G, x)$ , hence $d ⊩^{α} \neg φ (G)$ .

In case $n > 0$ , density follows from clause 4 of Definition 4.11. □

We now prove that the weak forcing relation extended to any arithmetic formula enjoys the desired definability properties. For this, we start with a lemma showing that the extension relation is $Π_{2}^{0}$ . Therefore, only the first two levels have to be treated independently, since the extension relation does not add some extra complexity to the forcing relation for higher formulas. Lemma 4.14.
For every condition c, $Ext (c)$ is $Π_{2}^{0}$ uniformly in c.
Proof.
Recall from Lemma 3.10 that given $k, t \in ω$ , the set $PartTree (k, t)$ denotes the $Π_{1}^{0}$ set of all the infinite p.r. k-partition trees of $[t, \infty)$ , and given a k-partition tree S and a part ν of S, the predicate $Empty (S, ν)$ denotes the $Π_{1}^{0}$ formula “part ν of S is empty”, that is, the formula $(\forall σ \in S) [{set}_{ν} (σ) \cap dom (S) = \emptyset]$ . If T is p.r. then so is $T^{[ν, H]}$ for some finite set H.

Fix a condition $c = (\vec{F}, (k, t, T), C)$ . $(\vec{H}, (k^{'}, t^{'}, S), D) \in Ext (c)$ iff the following formula holds: $\begin{matrix} \begin{matrix} (\exists f : k^{'} \to k) \\ (\forall ν < k^{'}) (\forall α < 2) (H_{ν}^{α}, [t^{'}, \infty) \cap R_{α}) Mathias extends (F_{f (ν)}^{α}, [t, \infty) \cap R_{α}) & (Π_{2}^{0}) \\ \land S \in PartTree (k^{'}, t^{'}) \land S ⩽_{f} \underset{ν < k^{'}, α < 2}{⋀} T^{[f (ν), H_{ν}^{α}]} & (Π_{1}^{0}) \\ \land D is a promise for S \land D \subseteq C & (Π_{2}^{0}) . \end{matrix} \end{matrix}$ The formula $(H_{ν}^{α}, [t^{'}, \infty) \cap R_{α}) Mathias extends (F_{f (ν)}^{α}, [t, \infty) \cap R_{α})$ can be written $(\forall x < t) [x \in H_{ν}^{α} \leftrightarrow x \in F_{f (ν)}^{α}] \land t^{'} ⩾ t \land (\forall x \in H_{ν}^{α} ∖ F_{f (ν)}^{α}) x \in R_{α}$ and therefore is $Π_{2}^{0}$ . By Lemma 3.10 and the fact that $⋀_{ν < k^{'}, α < 2} T^{[f (ν), H_{ν}^{α}]}$ is p.r. uniformly in T, f, $\vec{H}$ and $k^{'}$ , the above formula is $Π_{2}^{0}$ . □
Lemma 4.15.
Fix an arithmetic formula $φ (G)$ , a condition $c = (\vec{F}, T, C)$ , a side $α < 2$ and a part ν of T.
If $φ (G)$ is a $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula then so is the predicate $c ⊩_{ν}^{α} φ (G)$ .

If $φ (G)$ is a $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula then so is the predicate $c ⊩^{α} φ (G)$ .

Proof.
We prove our lemma by induction over the complexity of the formula $φ (G)$ .
If $φ (G) \in Σ_{1}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 4.8, $c ⊩_{ν}^{α} φ (G)$ if and only if the formula $(\exists w \in ω) ψ (F_{ν}^{α}, w)$ holds. This is a $Σ_{1}^{0}$ predicate.

If $φ (G) \in Π_{1}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 2 of Definition 4.8, $c ⊩_{ν}^{α} φ (G)$ if and only if the formula $(\forall σ \in T) (\forall w < | σ |) (\forall F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)) ψ (F_{ν}^{α} \cup F^{'}, w)$ holds. This is a $Π_{1}^{0}$ predicate.

If $φ (G) \in Σ_{2}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . By clause 1 of Definition 4.11, $c ⊩^{α} φ (G)$ if and only if the formula $(\forall ν < parts (T)) (\exists w < dom (T)) [(ν, T) \in C \to c ⊩_{ν}^{α} ψ (G, w)]$ holds. This is a $Σ_{2}^{0}$ predicate by induction hypothesis and the fact that $C$ is $\emptyset^{'}$ -computable.

If $φ (G) \in Π_{2}^{0}$ then it can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . By clause 2 of Definition 4.11, $c ⊩ φ (G)$ if and only if for every infinite $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ , every w and $\vec{E}$ smaller than the code of S such that the followings hold
$(E_{ν}, dom (S) \cap R_{α})$ Mathias extends $(F_{f (ν)}, dom (T) \cap R_{α})$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$
for every $(μ, S) \in C$ , $(\vec{E}, S, C [S]) ⊮_{μ}^{α} \neg ψ (G, w)$ . By Lemma 3.10, properties (i)–(ii) are $Δ_{2}^{0}$ . Moreover the predicate $(μ, S) \in C$ is $Δ_{2}^{0}$ since $C$ is $\emptyset^{'}$ -p.r. By induction hypothesis, $(\vec{E}, S, C [S]) ⊮_{μ}^{α} \neg ψ (G, w)$ is $Σ_{1}^{0}$ . Therefore $c ⊩^{α} φ (G)$ is a $Π_{2}^{0}$ predicate.

If $φ (G) \in Σ_{n + 3}^{0}$ then it can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ . By clause 3 of Definition 4.11, $c ⊩^{α} φ (G)$ if and only if the formula $(\exists w \in ω) c ⊩^{α} ψ (G, w)$ holds. This is a $Σ_{n + 3}^{0}$ predicate by induction hypothesis.

If $φ (G) \in Π_{n + 3}^{0}$ then it can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause 4 of Definition 4.11, $c ⊩^{α} φ (G)$ if and only if the formula $(\forall d) (d \notin Ext (c) \lor d ⊮^{α} ψ (G))$ holds. By induction hypothesis, $d ⊮^{α} ψ (G)$ is a $Π_{n + 3}^{0}$ predicate. By Lemma 4.14, the set $Ext (c)$ is $Π_{2}^{0}$ -computable uniformly in c, thus $c ⊩^{α} φ (G)$ is a $Π_{n + 3}^{0}$ predicate. □

4.4. Validity

As we already saw, we have two candidate forcing relations for $Σ_{1}^{0}$ and $Π_{1}^{0}$ formulas:

The “true” forcing relation $c ⊪^{α} φ (G)$ . This relation has been shown to have the expected density properties through Lemma 4.7. However deciding such a relation requires too much computational power.

The “weak” forcing relation $c ⊩^{α} φ (G)$ . Deciding such a relation requires the same definitional power as the formula it forces. It provides a sufficient condition for forcing the formula $φ (G)$ as $c ⊩^{α} φ (G)$ implies $c ⊪^{α} φ (G)$ , but the converse does not hold and we cannot prove the density property in the general case.

Thankfully, there exist some sides and parts of any condition on which those two forcing relations coincide. This leads to the notion of validity.

Definition 4.16 (Validity).

Fix an enumeration $φ_{0} (G), φ_{1} (G), \dots$ of all $Π_{1}^{0}$ formulas. Fix a condition $c = (\vec{F}, T, C)$ , a side $α < 2$ , and a part ν of T. We say that side α is n-valid in part ν of T for some $n \in ω$ if part ν of T is $R_{α}$ -acceptable and for every $i < n$ , $c ⊪_{ν}^{α} φ_{i} (G)$ iff $c ⊩_{ν}^{α} φ_{i} (G)$ .

The following lemma shows that given some $n \in ω$ , we can restrict $C$ so that it “witnesses its n-valid parts”.

Lemma 4.17.
For every $n \in ω$ , the following set is dense in $P$ : $\begin{matrix} {(\vec{F}, T, C) \in P : (\forall ν) (\exists α < 2) [(ν, T) \in C \to side α is n -valid in part ν of T]} . \end{matrix}$
Proof.
Given a condition $c = (\vec{F}, T, C)$ , let $I (c)$ be the set of the parts ν of T such that $(ν, T) \in C$ and no $α < 2$ is valid for φ in part ν of T. Fix a condition $c = (\vec{F}, T, C) \in P$ . By iterating Lemma 4.13, we can assume without loss of generality that for each $i < n$ , $\begin{matrix} (\forall α < 2) [c ⊩^{α} (\exists x) φ_{i} (G) or c ⊩^{α} (\forall x) \neg φ_{i} (G)] . \end{matrix}$ The dummy variable x ensures that the forcing relation for $Σ_{2}^{0}$ and $Π_{2}^{0}$ is applied. It suffices to prove that for every $ν \in I (c)$ , there exists an extension $d = (\vec{E}, S, D)$ such that $I (d) \subseteq I (c) ∖ {ν}$ . Iterating the process at most $| parts (T) |$ times completes the proof.

Fix a part $ν \in I (c)$ and let $D$ be the set of $(μ, S) \in C$ such that part μ of S does not refine part ν of T. The set $D$ is a $\emptyset^{'}$ -p.r. upward-closed subset of $C$ . It suffices to prove that for every infinite p.r. partition tree $S ⩽ T$ , there exists a non-empty part μ of S such that $(μ, S) \in D$ to deduce that $D$ is a promise for T and obtain an extension $d = (\vec{E}, T, D)$ of c such that $I (d) \subseteq I (c) ∖ {ν}$ .

Fix an infinite p.r. partition tree $S ⩽_{g} T$ for some g and let μ be a part of S g-refining part ν of T. By choice of ν, for every $α < 2$ , either μ is not $R_{α}$ -acceptable in S, or $c ⊪_{ν}^{α} φ_{i_{α}} (G)$ but $c ⊮_{ν}^{α} φ_{i_{α}} (G)$ for some $i_{α} < n$ . In the latter case, by choice of c, $c ⊩_{ν}^{α} (\forall x) \neg φ_{i_{α}} (G)$ .

We now assume that S has k parts, among which m parts g-refine ν. Let $f : k + m \to k$ be the function such that $f (μ) = μ$ for each part μ of S not g-refining part ν of T, and such that $f (μ_{α}) = μ$ for each part μ of S g-refining part ν of T and each $α < 2$ . In other words, f forks each part μ of S g-refining the part μ of T into 2 parts $μ_{0}$ and $μ_{1}$ . Let P be a path through S, and let $t \in ω$ be large enough to “witness the non $R_{α}$ -acceptable sides”. More formally, let t be such that for every $α < 2$ , either ${set}_{μ} (P) \cap R_{α} \cap [t, \infty) = \emptyset$ for each part μ of S g-refining part ν of T, or $c ⊪_{ν}^{α} φ_{i_{α}} (G)$ but $c ⊮_{ν}^{α} φ_{i_{α}} (G)$ .

Let $S^{'}$ be the p.r. tree of all the τ’s f-refining some $σ \in S$ and such that for each $α < 2$ and each part μ of S g-refining part ν of T, either ${set}_{μ_{α}} (τ) \cap [t, \infty) = \emptyset$ , or $φ_{i_{α}} (F_{ν}^{α} \cup F^{'})$ holds for each $F^{'} \subseteq dom (S) \cap {set}_{μ_{α}} (τ)$ . The tree $S^{'}$ is a $(k + m)$ -partition tree of $[t, \infty)$ f-refining S. We claim that $S^{'}$ is infinite. Fix some $s \in ω$ , we will prove that $τ \in S^{'}$ for some string τ of length s. Let $σ = P ↾ s$ . In particular, $S^{[σ]}$ is infinite, so for every $α < 2$ and every part μ of S g-refining part ν of T, either ${set}_{μ} (P) \cap R_{α} \cap [t, \infty) = \emptyset$ by definition of t, or, unfolding clause 2 of Definition 4.5 for $c ⊪_{ν}^{α} φ_{i_{α}} (G)$ and since σ g-refines some extendible node in T, for every set $F^{'} \subseteq dom (S) \cap {set}_{μ} (σ) \cap R_{α}$ , $φ (F_{ν}^{α} \cup F^{'})$ holds. Let τ be the string refining σ such that ${set}_{μ_{α}} (τ) = {set}_{μ} (σ) \cap R_{α}$ for each $α < 2$ and each part μ of S g-refining part ν of T. By definition of $S^{'}$ , $τ \in S^{'}$ . Therefore $S^{'}$ is infinite. Moreover, by definition of $S^{'}$ , for each $α < 2$ , either $μ_{α}$ is empty in $S^{'}$ or $(\vec{E}, S^{'}, C [S^{'}]) ⊩_{μ_{α}}^{α} φ_{i_{α}} (G)$ , where $\vec{E}$ is obtained by duplicating the sets in $\vec{F}$ according the forks of $g \circ f$ .

By definition of $c ⊩_{ν}^{α} (\forall x) \neg φ_{i_{α}} (G)$ , $(\vec{E}, S^{'}, C [S^{'}]) ⊮_{μ_{α}}^{α} φ_{i_{α}} (G)$ for each $α < 2$ and each part μ of S g-refining part ν of T such that $(μ_{α}, S^{'}) \in C$ . Then, for each $α < 2$ , either $μ_{α}$ is empty in $S^{'}$ , or $(μ_{α}, S^{'}) \notin C$ , as otherwise it would contradict $(\vec{E}, S^{'}, C [S^{'}]) ⊩_{μ_{α}}^{α} φ (G)$ . So there must exists a non-empty part μ of $S^{'}$ not refining part ν of T such that $(μ, S^{'}) \in C$ , and by upward closure of a promise, there exists a non-empty part μ of S not refining part ν of T such that $(μ, S) \in C$ . By definition of $D$ , $(μ, S) \in D$ . Therefore $D$ is a promise for T and we conclude. □

Given any filter $F = {c_{0}, c_{1}, \dots}$ with $c_{s} = ({\vec{F}}_{s}, T_{s}, C_{s})$ the set of pairs $(α, ν_{s})$ such that $(ν_{s}, T_{s}) \in C_{s}$ forms again an infinite, directed acyclic graph $G (F)$ . By Lemma 4.17, whenever $F$ is sufficiently generic, the graph $G (F)$ yields a sequence of parts P such that for every s if $c_{s}$ refines $c_{t}$ , then part $P (s)$ of $c_{s}$ refines part $P (t)$ of $c_{t}$ , and such that for every n, there is some s and some side $α < 2$ such that the side α is n-valid in part $P (s)$ of $c_{s}$ . The path P induces an infinite set $G = ⋃ {F_{P (s), s}^{α} : s \in ω}$ . Since whenever α is n-valid in part $P (s)$ of $c_{s}$ , then it is m-valid in part $P (s)$ of $c_{s}$ for every $m < n$ , we can fix an $α < 2$ such that for every n, there is some s such that the side α is n-valid in part $P (s)$ of $c_{s}$ . We call α the generic side, P the generic path and G the generic real.

By choosing a generic path that goes through valid sides and parts of the conditions, we recovered the density property for the weak forcing relation and can therefore prove that a property holds over the generic real if and only if it can be forced by some condition belonging to the generic filter. Lemma 4.18.
Suppose that $F$ is sufficiently generic and let α, P and G be the generic side, the generic path and the generic real, respectively. For every $Σ_{1}^{0}$ ( $Π_{1}^{0}$ ) formula $φ (G)$ , $φ (G)$ holds iff $c_{s} ⊩_{P (s)}^{α} φ (G)$ for some $c_{s} \in F$ .
Proof.
Thanks to validity, it suffices to prove that if $c_{s} ⊩_{ν}^{α} φ (G)$ for some $c_{s} \in F$ , then $φ (G)$ holds. Indeed, if $φ (G)$ holds, then by genericity of $F$ , $c_{s} ⊪_{P (s)}^{α} φ (G)$ or $c_{s} ⊪_{P (s)}^{α} \neg φ (G)$ for some $c_{s} \in F$ . By validity of side α in part $P (s)$ of $c_{s}$ , $c_{s} ⊩_{P (s)}^{α} φ (G)$ or $c_{s} ⊩_{P (s)}^{α} \neg φ (G)$ . If $c_{s} ⊩_{P (s)}^{α} \neg φ (G)$ then $\neg φ (G)$ holds, contradicting the hypothesis. So $c_{s} ⊩_{P (s)}^{α} φ (G)$ . Fix a condition $c_{s} = (\vec{F}, T, C) \in F$ such that $c_{s} ⊩_{ν}^{α} φ (G)$ , where $ν = P (s)$ .
If $φ \in Σ_{1}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 1 of Definition 4.8, there exists a $w \in ω$ such that $ψ (F_{ν}^{α}, w)$ holds. As $ν = P (s)$ , $F_{ν}^{α} = F_{P (s)}^{α} \subseteq G$ and $G ∖ F_{ν}^{α} \subseteq (max F_{ν}^{α}, \infty)$ , so $ψ (G, w)$ holds by continuity, hence $φ (G)$ holds.

If $φ \in Π_{1}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{0}^{0}$ . By clause 2 of Definition 4.8, for every $σ \in T$ , every $w < | σ |$ and every set $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ , $ψ (F_{ν}^{α} \cup F^{'}, w)$ holds. For every $F^{'} \subseteq G ∖ F_{ν}^{α}$ , and $w \in ω$ there exists a $σ \in T$ such that $w < | σ |$ and $F^{'} \subseteq dom (T) \cap {set}_{ν} (σ)$ . Hence $ψ (F_{ν}^{α} \cup F^{'}, w)$ holds. Therefore, for every $w \in ω$ , $ψ (G, w)$ holds, so $φ (G)$ holds. □

Lemma 4.19.
Suppose that $F$ is sufficiently generic and let α and G be the generic side and the generic real, respectively. For every $Σ_{n + 2}^{0}$ ( $Π_{n + 2}^{0}$ ) formula $φ (G)$ , $φ (G)$ holds iff $c_{s} ⊩^{α} φ (G)$ for some $c_{s} \in F$ .
Proof.
This lemma uses validity implicitly by calling Lemma 4.18, where it was used explicitly. Emulating the proof of Lemma 3.23, it suffices to prove that if $c_{s} ⊩^{α} φ (G)$ for some $c_{s} \in F$ then $φ (G)$ holds. Let P be the generic path induced by the generic filter $F$ . Fix a condition $c_{s} = (\vec{F}, T, C) \in F$ such that $c_{s} ⊩^{α} φ (G)$ . We proceed by case analysis on φ.
If $φ \in Σ_{2}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{1}^{0}$ . By clause 1 of Definition 4.11, for every part ν of T such that $(ν, T) \in C$ , there exists a $w < dom (T)$ such that $c_{s} ⊩_{ν}^{α} ψ (G, w)$ . Since $(P (s), T) \in C$ , $c_{s} ⊩_{P (s)}^{α} ψ (G, w)$ . By Lemma 4.18, $ψ (G, w)$ holds, hence $φ (G)$ holds.

If $φ \in Π_{2}^{0}$ then $φ (G)$ can be expressed as $(\forall x) ψ (G, x)$ where $ψ \in Σ_{1}^{0}$ . By clause 2 of Definition 4.11, for every infinite $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ , every w and $\vec{E}$ smaller than the code of S such that the followings hold
$(E_{ν}, dom (S) \cap R_{α})$ Mathias extends $(F_{f (ν)}, dom (T) \cap R_{α})$ for each $ν < parts (S)$ ,

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}]}$
for every $(μ, S) \in C$ , $(\vec{E}, S, C [S]) ⊮_{μ}^{α} \neg ψ (G, w)$ . Suppose by way of contradiction that $ψ (G, w)$ does not hold for some $w \in ω$ . Then by Lemma 4.18, there exists a $c_{t} \in F$ such that $c_{t} ⊩_{P (t)}^{α} \neg ψ (G, w)$ . Since $F$ is a filter, there is a condition $c_{e} = (\vec{E}, S, D) \in F$ extending $c_{s}$ and $c_{t}$ . By choice of P, $(P (e), S) \in C$ , so by clause (ii), $(\vec{E}, S, C [S]) ⊮_{P (e)}^{α} ψ (G, w)$ , hence by Lemma 4.10, $c_{e} ⊮_{P (e)}^{α} ψ (G, w)$ . However, since part $P (e)$ of $c_{e}$ refines part $P (t)$ of $c_{t}$ , then by Lemma 4.9, $c_{e} ⊩_{P (e)}^{α} ψ (G, w)$ . Contradiction. Hence, for every $w \in ω$ , $ψ (G, w)$ holds, so $φ (G)$ holds.

If $φ \in Σ_{n + 3}^{0}$ then $φ (G)$ can be expressed as $(\exists x) ψ (G, x)$ where $ψ \in Π_{n + 2}^{0}$ . By clause 3 of Definition 4.11, there exists a $w \in ω$ such that $c_{s} ⊩^{α} ψ (G, w)$ . By induction hypothesis, $ψ (G, w)$ holds, hence $φ (G)$ holds.

Conversely, if $φ (G)$ holds, then there exists a $w \in ω$ such that $ψ (G, w)$ holds, so by induction hypothesis $c_{s} ⊩^{α} ψ (G, w)$ for some $c_{s} \in F$ , so by clause 3 of Definition 4.11, $c_{s} ⊩^{α} φ (G)$ .

If $φ \in Π_{n + 3}^{0}$ then $φ (G)$ can be expressed as $\neg ψ (G)$ where $ψ \in Σ_{n + 3}^{0}$ . By clause 4 of Definition 4.11, for every $d \in Ext (c_{s})$ , $d ⊮^{α} ψ (G)$ . By Lemma 4.12, $d ⊮^{α} ψ (G)$ for every $d \in F$ , and by a previous case, $ψ (G)$ does not hold, so $φ (G)$ holds. □

4.5. Preserving definitions

The following (and last) lemma shows that every sufficiently generic real preserves higher definitions. This preservation property cannot be proved in the case of non- $Σ_{1}^{0}$ sets since the weak forcing relation does not have the good density property in general.

Lemma 4.20.
If $A \notin Σ_{n + 2}^{0}$ and $φ (G, x)$ is $Σ_{n + 2}^{0}$ , then the set of $c \in P$ satisfying the following property is dense: $\begin{matrix} (\forall α < 2) [(\exists w \in A) c ⊩^{α} \neg φ (G, w)] \lor [(\exists w \notin A) c ⊩^{α} φ (G, w)] . \end{matrix}$
Proof.
It is sufficient to find, given a condition c and a side $α < 2$ , an extension d of c such that the following holds: $\begin{matrix} [(\exists w \in A) c ⊩^{α} \neg φ (G, w)] \lor [(\exists w \notin A) c ⊩^{α} φ (G, w)] . \end{matrix}$ Fix a condition $c = (\vec{F}, T, C)$ and a side $α < 2$ .
In case $n = 0$ , $φ (G, w)$ can be expressed as $(\exists x) ψ (G, w, x)$ where $ψ \in Π_{1}^{0}$ . Let U be the set of integers w such that there exists an infinite p.r. $k^{'}$ -partition tree S for some $k^{'} \in ω$ , a function $f : parts (S) \to parts (T)$ and a $2 k^{'}$ -tuple of finite sets $\vec{E}$ such that
$E_{ν}^{β} = F_{f (ν)}^{β}$ for each $ν < parts (S)$ and $β \neq α$ ;

$(E_{ν}^{α}, dom (S) \cap R_{α})$ Mathias extends $(F_{f (ν)}^{α}, dom (T))$ for each $ν < parts (S)$ ;

S f-refines $⋂_{ν < parts (S)} T^{[f (ν), E_{ν}^{α}]}$ ;

for each non-empty part ν of S such that $(ν, S) \in C$ , $(\vec{E}, S, C [S]) ⊩_{ν}^{α} ψ (G, w, u)$ for some $u < # S$ .
By Lemma 4.15 and Lemma 3.10, $U \in Σ_{2}^{0}$ , thus $U \neq A$ . Let $w \in U Δ A$ .

Suppose that $w \in U ∖ A$ . Let $D = C [S] ∖ {(ν, S^{'}) \in C : part ν of S^{'} is empty}$ . As $C$ is an $\emptyset^{'}$ -p.r. promise for T, $C [S]$ is an $\emptyset^{'}$ -p.r. promise for S. As $D$ is obtained from $C [S]$ by removing only empty parts, $D$ is also an $\emptyset^{'}$ -p.r. promise for S. By Lemma 4.10, for every part ν of S such that $(ν, S) \in D \subseteq C$ , $(\vec{E}, S, D) ⊩_{ν}^{α} ψ (G, w, u)$ for some $u < dom (S)$ , hence by clause 1 of Definition 4.11, $d = (\vec{E}, S, D) ⊩^{α} (\exists x) ψ (G, w, x)$ . In other words, $d ⊩^{α} φ (G)$ for some $w \notin A$ .

We may choose a coding of the p.r. trees such that the code of S is sufficiently large to witness w and $\vec{E}$ . So suppose now that $w \in A ∖ U$ . Then for every infinite p.r. $k^{'}$ -partition tree S, every function $f : parts (S) \to parts (T)$ and every $\vec{E}$ smaller than the code of S such that properties i-iii) hold, there exists a non-empty part ν of S such that $(ν, S) \in C$ and $(\vec{E}, S, C [S]) ⊮_{ν}^{α} ψ (G, w, u)$ for every $u < # S$ . Let $D$ be the collection of all such $(ν, S)$ . $D$ is $\emptyset^{'}$ -p.r. By Lemma 4.9 and since $# S ⩾ # T$ whenever $S ⩽ T$ , $D$ is upward-closed under the refinement relation, hence is a promise for T. By clause 2 of Definition 4.11, $d = (\vec{F}, T, D) ⊩^{α} (\forall x) \neg ψ (G, w, x)$ , hence $d ⊩^{α} \neg φ (G, w)$ for some $w \in A$ .

In case $n > 0$ , let $U = {w \in ω : (\exists d \in Ext (c)) d ⊩^{α} φ (G, w)}$ . By Lemma 3.24 and Lemma 3.25, $U \in Σ_{n + 2}^{0}$ , thus $U \neq A$ . Fix $w \in U Δ A$ . If $w \in U ∖ A$ then by definition of U, there exists a condition d extending c such that $d ⊩^{α} φ (G, w)$ . If $w \in A ∖ U$ , then for every $d \in Ext (c)$ , $d ⊮^{α} φ (G, w)$ so by clause 4 of Definition 4.11, $c ⊩^{α} \neg φ (G, w)$ . □

We are now ready to reprove Corollary 3.29 from Wang [22].
Theorem 4.21 (Wang [22]).

$RT_{2}^{2}$ admits preservation of Ξ definitions simultaneously for all Ξ in ${Σ_{n + 2}^{0}, Π_{n + 2}^{0}, Δ_{n + 3}^{0} : n \in ω}$ .

Proof.

Since ${RCA}_{0} ⊢ COH \land D_{2}^{2} \to RT_{2}^{2}$ , and $COH$ admits preservation of the arithmetic hierarchy, it suffices to prove that $D_{2}^{2}$ admits preservation of Ξ definitions simultaneously for all Ξ in ${Σ_{n + 2}^{0}, Π_{n + 2}^{0}, Δ_{n + 3}^{0} : n \in ω}$ . Fix some set C and a $Δ_{2}^{0, C}$ 2-partition $R_{0} \cup R_{1} = ω$ . Let $C_{0}$ be the $C^{'}$ -p.r. set of all $(ν, T) \in U$ such that $(ν, T) ⩽ (0, 1^{< ω})$ . Let $F$ be a sufficiently generic filter containing $c_{0} = ({\emptyset, \emptyset}, 1^{< ω}, C_{0})$ . Let G be the corresponding generic real. By definition of a condition, the set G is $\vec{R}$ -cohesive. By Lemma 4.20 and Lemma 4.15, G preserves non- $Σ_{n + 2}^{0}$ definitions relative to C for every $n \in ω$ . Therefore, by Proposition 2.2 of [22], G preserves Ξ definitions relative to C simultaneously for all Ξ in ${Σ_{n + 2}^{0}, Π_{n + 2}^{0}, Δ_{n + 3}^{0} : n \in ω}$ . □

Footnotes

Acknowledgements

The author is thankful to Wei Wang for interesting comments and discussions. The author is funded by the John Templeton Foundation (‘Structure and Randomness in the Theory of Computation’ project). The opinions expressed in this publication are those of the author(s) and do not necessarily reflect the views of the John Templeton Foundation.

References

Bovykin and

Weiermann, The strength of infinitary Ramseyan principles can be accessed by their densities, Annals of Pure and Applied Logic (2005), 4, to appear.

C.G.

Jockusch, Degrees in which the recursive sets are uniformly recursive, Canad. J. Math. 24 (1972), 1092–1099.

C.G.

Jockusch, Ramsey’s theorem and recursion theory, Journal of Symbolic Logic 37(2) (1972), 268–280.

C.G.

Jockusch and

Stephan, A cohesive set which is not high, Mathematical Logic Quarterly 39(1) (1993), 515–530.

P.A.

Cholak,

D.D.

Dzhafarov,

J.L.

Hirst and

T.A.

Slaman, Generics for computable Mathias forcing, Annals of Pure and Applied Logic 165(9) (2014), 1418–1428.

P.A.

Cholak,

Giusto,

J.L.

Hirst and

C.G.

JockuschJr., Free sets and reverse mathematics, Reverse Mathematics 21 (2001), 104–119.

P.A.

Cholak,

C.G.

Jockusch and

T.A.

Slaman, On the strength of Ramsey’s theorem for pairs, Journal of Symbolic Logic 66(01) (2001), 1–55.

Chong,

Lempp and

Yang, On the role of the collection principle for

Σ_{2}^{0}

-formulas in second-order reverse mathematics, Proceedings of the American Mathematical Society 138(3) (2010), 1093–1100.

B.F.

Csima and

J.R.

Mileti, The strength of the rainbow Ramsey theorem, Journal of Symbolic Logic 74(04) (2009), 1310–1324.

10.

D.R.

Hirschfeldt, Slicing the Truth: On the Computable and Reverse Mathematics of Combinatorial Principles,

Chong,

Feng,

T.A.

Slaman,

W.H.

Woodin and

Yang, eds, Lecture Notes Series. Institute for Mathematical Sciences. National University of Singapore, Vol. 28, World Scientific Publishing Co. Pte. Ltd, Hackensack, NJ, 2015.

11.

A.P.

Kreuzer, Primitive recursion and the chain antichain principle, Notre Dame Journal of Formal Logic 53(2) (2012), 245–265.

12.

Lerman,

Solomon and

Towsner, Separating principles below Ramsey’s theorem for pairs, Journal of Mathematical Logic 13(02) (2013), 1350007.

13.

J.R.

Mileti, Partition theorems and computability theory, ProQuest LLC, Ann Arbor, MI, Ph.D. thesis, University of Illinois at Urbana-Champaign, 2004.

14.

Patey, Degrees bounding principles and universal instances in reverse mathematics, Annals of Pure and Applied Logic 166(11) (2015), 1165–1185.

15.

Patey, Iterative forcing and hyperimmunity in reverse mathematics, in: Evolving Computability (CiE),

Beckmann,

Mitrana and

Soskova, eds, Lecture Notes in Computer Science, Vol. 9136, Springer International Publishing, 2015, pp. 291–301.

16.

Patey, Somewhere over the rainbow Ramsey theorem for pairs, 2015, submitted, available at: http://arxiv.org/abs/1501.07424.

17.

Patey, The weakness of being cohesive, thin or free in reverse mathematics, 2015, submitted, available at: http://arxiv.org/abs/1502.03709.

18.

Seetapun and

T.A.

Slaman, On the strength of Ramsey’s theorem, Notre Dame Journal of Formal Logic 36(4) (1995), 570–582.

19.

S.G.

Simpson, Subsystems of Second Order Arithmetic, Cambridge University Press, 2009.

20.

Wang, Cohesive sets and rainbows, Annals of Pure and Applied Logic 165(2) (2014), 389–408.

21.

Wang, Some logically weak Ramseyan theorems, Advances in Mathematics 261 (2014), 1–25.

22.

Wang, The definability strength of combinatorial principles, 2014, to appear, available at: http://arxiv.org/abs/1408.1465.

Controlling iterated jumps of solutions to combinatorial problems

Abstract

Keywords

1. Introduction

1.1. Reverse mathematics

1.2. Controlling iterated jumps

1.3. Preservation of the arithmetic hierarchy

Definition 1.1 (Preservation of definitions).

Theorem 1.2. COH and EM admit preservation of the arithmetic hierarchy. 1.4. Definitions and notation

2. Cohesiveness preserves the arithmetic hierarchy

Definition 2.1 (Cohesiveness).

Definition 2.5 (Precondition).

Definition 3.1 (Erdős–Moser theorem).

3.1. Erdős–Moser forcing

Lemma 3.6 (Patey [14]).

3.2. Partition trees

Definition 3.7 (Partition tree).

Definition 3.8 (Refinement).

Definition 3.9 (Promise for a partition tree).

Definition 4.5 (True forcing relation).

Definition 4.16 (Validity).

Footnotes

Acknowledgements

References

Theorem 1.2.
$COH$ and $EM$ admit preservation of the arithmetic hierarchy.

1.4. Definitions and notation