Paul-Elliot Angles D'auriac

L U Liu

Bastien Mignoty
email: bastien.mignoty@ens-lyon.fr

Ludovic Patey
email: ludovic.patey@computability.fr

CARLSON-SIMPSON'S LEMMA AND APPLICATIONS IN REVERSE MATHEMATICS

We study the reverse mathematics of infinitary extensions of the Hales-Jewett theorem, due to Carlson and Simpson. These theorems have multiple applications in Ramsey's theory, such as the existence of finite big Ramsey degrees for the triangle-free graph, or the Dual Ramsey theorem. We show in particular that the Open Dual Ramsey theorem holds in ACA + 0 .

Introduction

Tree partition theorems play an important role in Structural Ramsey theory, by providing a combinatorial core to which many other structural theorems can be reduced. For example, Milliken's tree theorem, states that, given an infinite finitely branching tree T , for every finite coloring of the strongly embedded subtrees of length n of T , there is a strongly embedded subtree of infinite height S such that all embedded subtrees of length n are monochromatic. Milliken's tree theorem is known to be the combinatorial core to prove the existence of a big Ramsey degree for colorings of the rationals and of the Rado graph (see Todorcevic [START_REF] Todorcevic | Introduction to Ramsey spaces[END_REF]).

We study the reverse mathematics of infinitary extensions of the Hales-Jewett theorem, due to Carlson and Simpson [START_REF] Carlson | A dual form of Ramsey's theorem[END_REF], and prove that they hold over ACA 0 . The higher-order version of Carlson-Simpson's lemma holds in ACA + 0 and was used by Carlson and Simpson to prove a dual version of Ramsey's theorem [START_REF] Carlson | A dual form of Ramsey's theorem[END_REF]. More recently, Hubička [START_REF] Hubička | Big ramsey degrees using parameter spaces[END_REF] proved that the existence of a big Ramsey degree for the universal triangle-free graph followed from the higher-order version of Carlson-Simpson's lemma. This gave a simpler proof, yet less accurate, than the original proof of Dobrinen [START_REF] Dobrinen | The Ramsey theory of the universal homogeneous triangle-free graph[END_REF]. Thanks to our reverse mathematical analysis of Carlson-Simpson's lemma, we deduce that the existence of a big Ramsey degree for the universal triangle-free graph, and the restriction of the Dual Ramsey theorem to open sets both hold in ACA + 0 .

1.1. Variable words. We identify a non-negative integer k ∈ ω with the set {0, . . . , k -1}. A word over a finite alphabet A is a finite ordered sequence w = ⟨a 0 , . . . , a n-1 ⟩ ∈ A n for some n ∈ ω. An infinite word over A is a function W : ω → A. We denote by A <ω and A ω the sets of finite and infinite words over A, respectively. For w = ⟨a 0 , . . . , a n-1 ⟩, we write |w| for the length n of the word w and given i < n, we let w(i) = a i .

An ω-variable word over A is an infinite word W over the alphabet A ⊔ {x j : j ∈ N} where each variable kind x j appears at least once and the first occurrence of x j appears before the first occurrence of x j+1 . We write A ω,ω for the set of all ω-variable words over A. Given an ω-variable word W over A and a word u over A, we write W [u] for the finite word over A where each occurrences of x j is replaced by u(j), and cut before the first occurrence of x |u| . In particular, letting ϵ be the empty word, W (ϵ) is the initial segment of w before the first occurence of x 0 . The substitution notation W [a] must not be confused with W (i): the former notation denotes the finite word obtained by substitution of all the occurrences of x 0 by the letter a and cutting before the first occurrence of x 1 , while the latter notation denotes the letter in W at position i.

Example 1.1. Then sequence 01101x 0 1010x 1 10x 0 101x 2 0110x 0 01010x 1 is a valid initial segment of an ωvariable word over 2. On the other hand, 010x 1 0101x 0 is not, since the first occurrence of x 1 appears before the first occurrence of x 0 . Similarly, 00191x 0 101x 2 is not a valid initial segment, since in an ω-variable word over 2, the variable x 1 must appear at some point, before the first occurrence of x 2 . If W is an ω-variable word over 2 starting with 01x 0 10x 1 01x 0 001x 2 , then W The following theorem was proven by Carlson and Simpson [START_REF] Carlson | A dual form of Ramsey's theorem[END_REF]Lemma 2.4]: Theorem 1.2 (Carlson-Simpson Lemma1 ). For every finite alphabet A and every finite partition C 0 ⊔ • • • ⊔ C ℓ-1 = A <ω , there is some color i < ℓ and an ω-variable word W such that {W [u] : u ∈ A <ω } ⊆ C i .

We write CSL(k, ℓ) the statement of theorem 1.2 for ℓ-colorings and alphabets of size k. The Carlson-Simpson Lemma has several consequences in combinatorics, among which a dual version of Ramsey's theorem and the existence of a big Ramsey degree of the universal triangle-free graph.

Carlson and Simpson [1, Theorem 6.3] actually proved a stronger statement, known as the Ordered Variable Word theorem. An ω-variable word over A is ordered if the last occurrence of x j appears before the first occurrence of x j+1 . Note that if W is an ordered ω-variable word, then each variable must appear finitely often, unlike in the general case. We write A ω,ω < for the set of all ordered ω-variable words over A.

Theorem 1.3 (Ordered Variable Word theorem). For every finite alphabet A and every finite partition

C 0 ⊔ • • • ⊔ C ℓ-1 = A <ω ,
there is some color i < ℓ, and an ordered ω-variable word W over A such that

{W [u] : u ∈ A <ω } ⊆ C i .
We write OVW(k, ℓ) the statement of theorem 1.3 for ℓ-colorings of words over finite alphabets of size k. We study the reverse mathematics of the Ordered Variable Word theorem in Section 3 and Section 4, and prove that it holds over ACA 0 . It is currently unknown whether OVW(k, ℓ) is strictly weaker.

1.2. Higher-order Variable Words. The same way Ramsey's theorem for n-tuples can be proven inductively from the pigeonhole principle, the Carlson-Simpson Lemma can be used as a pigeonhole principle to prove inductively a higher-order version coloring finite multivariable words. An (ordered) n-variable word over A is a word w over the alphabet A ⊔ {x j : j < n} where each x j appears at least once and the first (last) occurrence of x j appears before the first occurrence of x j+1 . We call n the dimension of the n-variable word w. Denote by A <ω,n and A <ω,n < the sets of unordered and ordered n-variable words over A, respectively. Note that A <ω = A <ω,0 , and that A <ω,n ⊆ (A ⊔ {x 0 , . . . , x n-1 }) <ω . The higher-order version of the Carlson-Simpson Lemma is about finite colorings of n-variable words. The order of the theorem is the dimension of the variable words which are colored. Theorem 1.4 (Higher-order Carlson-Simpson Lemma). Fix n ≥ 0 and ℓ ≥ 1. For every finite alphabet A and every finite partition

C 0 ⊔ • • • ⊔ C ℓ-1 = A <ω,n
, there is some color i < ℓ and an infinite ω-variable word

W such that {W [u] : u ∈ A <ω,n } ⊆ C i .
We write CSL n (k, ℓ) the statement of theorem 1.4 for ℓ-colorings of n-variable words over finite alphabets of size k. In particular, CSL 0 (k, ℓ) is the statement CSL(k, ℓ). We study the reverse mathematics of the Higher-order Carlson-Simpson Lemma in Section 5 and prove that it holds over ACA + 0 . The Ordered Variable Word theorem also admits a higher-order counterpart, due to Carlson. The two last theorems of this introduction will not be studied in this paper, but we state them for the sake of completion: Theorem 1.5 (Higher-order Ordered Variable Word theorem). Fix n ≥ 0 and ℓ ≥ 1. For every finite alphabet A and every finite partition

C 0 ⊔ • • • ⊔ C ℓ-1 = A <ω,n < , there is some color i < ℓ and an infinite ordered ω-variable word W such that {W [u] : u ∈ A <ω,n } ⊆ C i .
We write OVW n (k, ℓ) the statement of theorem 1.5 for ℓ-colorings of ordered n-variable words over finite alphabets of size k. Here again, OVW 0 (k, ℓ) is the statement OVW(k, ℓ). However, OVW n (k, ℓ) cannot be proven by iterating its zero-dimensional version as in the case of the Carlson-Simpson Lemma. Theorem 1.5 follows from a stronger theorem known as Carlson's theorem. OVW n (k, ℓ) and Carlson's theorem have not been studied so far in reverse mathematics, as the only two known proofs of Carlson's theorem involve thirdorder objects, namely, ultrafilters in combinatorics, and Ellis enveloping semigroup in topological dynamics.

The Higher-order Ordered Variable Word theorem of dimension 1 for unary alphabets is actually equivalent to Hindman's theorem over RCA 0 . Given a set X ⊆ ω, we write FS(X) for the set of all non-empty sums over X with no repetitions, that is, FS(X) = { F : F ⊆ fin X ∧ F ̸ = ∅}. Theorem 1.6 (Hindman's theorem). For every finite partition C 0 ⊔ • • • ⊔ C ℓ-1 = ω; there is some color i < ℓ and an infinite set X ⊆ ω such that FS(X) ⊆ C i .

There exist several proofs of Hindman's theorem, which was extensively studied in reverse mathematics. Hindman's theorem is provable in ACA + 0 and implies ACA 0 . The exact strength of Hindman's theorem is one of the most important open question in reverse mathematics. 1.3. Organization of the paper. In Section 2, we fix some notation and definitions which will be useful all along the paper. Then, in Section 3 and Section 4, we give two proofs of the Ordered Variable Word theorem in ACA 0 , based on two different largeness notions: piecewise syndeticity and positive upper density. In Section 5, we iterate either proof of the Ordered Variable Word in ACA 0 to obtain a proof of the Higher-order Carlson-Simpson Lemma in ACA + 0 . Last, we explore two applications of the Higher-order Carlson-Simpson Lemma, namely, the Dual Ramsey Theorem for open sets in Section 6 and the existence of a big Ramsey degree of the universal triangle-free graph in Section 7. Both consequences are shown to hold over ACA + 0 .

Notation and background

In the introduction, we stated the Ordered Variable Word theorem and the Carlson-Simpson Lemma in terms of variable words. However, it is sometimes more convenient to consider the set of words obtained by taking all the possible instantiations of a variable word. Definition 2.1 (Ordered Variable Word tree). An OVW-tree over A of dimension n ∈ ω ∪ {ω} is a set of the form T = {w[u] : u ∈ A <n } for some ordered n-variable word w over A. We call w its generating variable word. An OVW-line is an OVW-tree of dimension 1.

We write T (j) = {w[u] : u ∈ A j } for the j-th level of T , L(T ) = {|u| : u ∈ T } for the set of levels of T and |T | = max(L(T )) for the size of T . Note that the size of T is different from the cardinality of T as a set, and from the dimension of T as well. The size of T coincides with the length of its generating variable word. An OVW-subtree of T is an OVW-tree which is a subset of T .

Example 2.2. For any c ∈ A <ω , {c} is an OVW-tree of dimension 0. The OVW-trees of dimension 1 are the sets of the form T = {c} ∪ {c ⌢ a ⌢ w[a] : a ∈ A} for some variable word w over A. Say A = {0, 1}, c = 10 and w = 01x 0 10. Then T = {10, 10001010, 10101110}, T (0) = {10} and T (1) = {10001010, 10101110}. On the other hand, S = {10, 1010, 1001} is not an OVW-tree.

It is easy to see that there is a one-to-one correspondence between OVW-trees and their generating variable words. The tree presentation is especially convenient when dealing with iterations. The Ordered Variable Word theorem can be stated in terms of OVW-trees as follows:

Theorem 2.3 (Ordered Variable Word theorem). For every finite alphabet A, every OVW-tree T ⊆ A <ω over A of dimension ω and every finite partition C 0 ⊔ • • • ⊔ C ℓ-1 = T , there is some color i < ℓ and an OVW-subtree S ⊆ T of dimension ω such that S ⊆ C i .

Proof. Let f : T → A <ω be the canonical computable isomorphism. Define

D 0 ⊔ • • • ⊔ D ℓ-1 = A <ω by D i = {u ∈ A <ω : f (u) ∈ C i }. By theorem 1.3, there is an ordered ω-variable word W over A and a color i < ℓ such that {W [u] : u ∈ A <ω } ⊆ D i . In particular, S = {f -1 (W [u]) : u ∈ A <ω } is an OVW-subtree of T such that S ⊆ C i . □
In some occasions, it will also be convenient to see an ordered n-variable word as a finite sequence σ, w 0 , w 1 , . . . , w n where σ ∈ A <ω is a word over A, and w i are left 1-variable words over A, that is, 1-variable words such that the variable occurs first at position 0. There is again a one-to-one correspondence between OVW-trees of dimension n and sequences of this form.

2.1. Largeness and partition regularity. Partition theorems are often refined in terms of large sets which are partition regular. These refinements can be seen as quantitative versions of these theorems. As it happens, the proofs of the refined versions are sometimes more elementary from a reverse mathematical viewpoint, although combinatorially more complicated.

Definition 2.4. A class C ⊆ P(A <ω ) is partition regular if (1) it is non-empty (2) if B ∈ C and B ⊆ C, then C ∈ C (3) if B ∈ C and C 0 ⊔ C 1 = B, then either C 0 ∈ C or C 1 ∈ Cc
We shall consider two refinements of the Ordered Variable Words, based on two standard partition regular notions : positive upper density and piecewise syndeticity. It is clear that A <ω has positive upper density, and that if D has positive upper density, then so have its supersets. Thus, properties (1) and ( 2) of the definition of partition regularity are satisfied for the class of all sets of positive upper density. The following lemma shows that property (3) is also satisfied, hence the class is partition regular. Proof. Let ϵ > 0 be such that the set B = {n : dens A n (D) > ϵ} is infinite. Suppose that E does not have positive upper density. Then the set C = {n : dens

A n (E) > ϵ/2} is finite. It follows that the set B ∖ C is infinite. Note that ∀n ∈ B ∖ C, dens A n (D) = dens A n (E) + dens A n (F ) > ϵ and dens A n (E) ≤ ϵ/2, so dens A n (F ) > ϵ/2. It follows that lim sup n→∞ dens A n (F ) > ϵ/2. □
We will prove in Section 4 that every set of positive upper density admits a solution to the Ordered Variable Word theorem.

2.1.2. Thickness and syndeticity. Given a set F ⊆ A <ω and a word σ ∈ A <ω , we let

F • σ = {τ σ : τ ∈ F }. Definition 2.7. A set S ⊆ A <ω is syndetic if there is some ℓ such that for every σ ∈ A <ω , there is some τ ∈ A ≤ℓ such that τ σ ∈ S. For a given ℓ we call such a set ℓ-syndetic. A set T ⊆ A <ω is thick if for each ℓ ∈ ω, there is some σ ∈ A <ω such that A ≤ℓ • σ ⊆ T . A set P ⊆ A <ω is piecewise syndetic if it
is the intersection of a thick set and a syndetic set.

Thickness and syndeticity are not partition regular notions, as they are not closed under partitioning. They play a dual role, in that a set is thick if and only if it intersects every syndetic set. We shall see on the other hand that piecewise syndeticity is partition regular. Lemma 2.8 (RCA 0 ). Let P ⊆ A <ω be a piecewise syndetic set, and let P = B ⊔ C, then either B or C is piecewise syndetic.

Proof. Assume that P = S ∩ T , where S is syndetic and T is thick, and let P = B ⊔ C. Let S := B ∪ (S ∖ P ). First, note that B ⊆ S and B ⊆ P ⊆ T , so B ⊆ S ∩ T . Also note that S ∩ T ⊆ B ∪ ((S ∖ P ) ∩ T ) ⊆ B, so B = S ∩ T . It follows that if S is syndetic, then B is piecewise syndetic, and the proof is finished. But if, on the contrary, S is not syndetic, then T := A <ω ∖ S is thick. Finally observe that

C = P ∖ B = (S ∖ B) ∩ (S ∩ P ) = (S ∖ B) ∩ (S ∖ (S ∖ P )) = S ∖ S = (A <ω ∖ S) ∩ S = T ∩ S, which shows that in this case C is piecewise syndetic. □
We will actually need the following iterated version of the previous lemma, which is a generalization of the so-called Brown's lemma. Brown's lemma was originally proved for locally finite semigroups. Frittaion [START_REF] Frittaion | Brown's lemma in second-order arithmetic[END_REF] studied it from a reverse mathematical viewpoint for the semigroup (N, +) and showed that it is equivalent to IΣ 0 2 over RCA 0 . The following proof is essentially the same, recasted in the setting of the semigroup (A <ω , •). Lemma 2.9 (Brown, RCA 0 + IΣ 0 2 ). Let P ⊆ A <ω be a piecewise syndetic set, and let P = ⊔ i<k C i for some k ∈ ω. Then there is some i < k such that C i is piecewise syndetic.

Proof. Let P = S ∩ T , where S is syndetic and T is thick. By bounded Σ 0 2 comprehension, the following set exists:

I = {B ⊆ {0, . . . , k -1} : (A <ω ∖ T ) ∪ i∈B C i is syndetic } Note that P ∪ (A <ω ∖ T ) is syndetic, hence {0, . . . , k -1} ∈ I. Let B ∈ I be minimal for the inclusion. Note that B ̸ = ∅. Fix any i ∈ B. Since (A <ω ∖ T ) ∪ j∈B C j } is syndetic, then either (A <ω ∖ T ) ∪ j∈B∖{i} C j is syndetic, or C i is piecewise syndetic.
The former case would contradict minimality of B, so the latter case holds. □

Before finishing this section, we prove a small technical lemma which will be useful in the proof of the Ordered Variable Word theorem. Lemma 2.10 (RCA 0 ). Suppose I ⊆ A <ω is a thick set and ℓ ∈ ω. Then the set J = {σ ∈ I :

A ≤ℓ • σ ⊆ I} is thick.
Proof. Fix some m ∈ ω. Since I is thick, there is some τ ∈ A <ω such that A ≤m+ℓ • τ ⊆ I. Let us show that A ≤m • τ ⊆ J, in other words, for every σ ∈ A ≤m , A ≤ℓ • στ ∈ I. Fix any σ ∈ A ≤m and ρ ∈ A ≤ℓ . Then since

A ≤m+ℓ • τ ⊆ I, ρστ ∈ I. □ 3. A proof of the Ordered Variable Word theorem in ACA 0
The purpose of this section is to prove the following piecewise syndetic version of the Ordered Variable Word over ACA 0 . Theorem 3.1 (Piecewise Syndetic Ordered Variable Word Theorem, ACA 0 ). Let P ⊆ A <ω be a piecewise syndetic set. Then there exists an OVW-tree T ⊆ P over A of dimension ω.

Since piecewise syndeticity is partition regular, Theorem 3.1 implies in particular the Ordered Variable Word theorem. Corollary 3.2 (ACA 0 ). For every finite alphabet A and every finite partition

C 0 ⊔ • • • ⊔ C ℓ-1 = A <ω ,
there is some color i < ℓ and an OVW-tree T ⊆ C i of dimension ω.

Proof. By Brown's lemma (see Lemma 2.9), there is some i < ℓ such that C i is piecewise syndetic. By Theorem 3.1, there exists an OVW-tree T ⊆ C i over A of dimension ω. □

We are going to use the following finitary version of the Ordered Variable Word.

Theorem 3.3 (RCA 0 ). Fix a finite alphabet A, a finite set of colors C. For every coloring f : A <ω → C, there is a monochromatic OVW-line S ⊆ A <ω and a letter a ∈ A such that S(0) and S(1) • a are both f -homogeneous for the same color.

It follows by compactness from the Ordered Variable Word theorem, but Dodos, Kanellopoulos and Tyros [5, Section 4] gave an elementary proof which can be formalized in RCA 0 .

Remark 3.4. The statement of Theorem 3.3 is slightly different from the one of [5, Section 4], but can be recovered by taking a monochromatic OVW-tree T ⊆ A <ω of dimension 2, then picking any non-empty σ ∈ A <ω such that T (1) • σ ⊆ T (2). Let σ * be the word σ truncated from its last letter a, and let S = T (0) ∪ (T (1) • σ * ). Then S is an OVW-line such that S(0) and S(1) • a are both f -homogeneous for the same color.

We are now ready to prove the main combinatorial lemma. The piecewise syndetic version of the Ordered Variable Word follows by iterating the following lemma. Lemma 3.5 (RCA 0 + IΣ 0 2 ). Let I ⊆ A <ω be a thick set and X : I → C be a coloring. There is an OVW-line S ⊆ A <ω and a piecewise syndetic P ⊆ I such that S(0) and S(1) • P are X-homogeneous for the same color.

Proof. Fix I and C. Suppose the lemma does not hold. We will build an infinite sequence of words σ 0 , σ 1 , . . . such that, letting w n be the left variable word x 0 σ n and N n = m≤n |w n |, the following property holds (for convenience, let N -1 = 0):

(3.1)
For every n ∈ ω, every b ∈ A, every OVW-line S ⊆ A <ω such that |S| = N n-1 , with S(0) ⊆ I, we have A Nn-1+1 • σ n ⊆ I and S(0) and S(1) • w n [b] are not X-homogeneous for the same color. Let σ 0 be such that A • σ 0 ⊆ I. Assume σ 0 , . . . , σ n-1 have been defined.

Let K be the set of all τ ∈ I such that there is an OVW-line S ⊆ A <ω with |S| = N n-1 and S(0) ⊆ I such that S(0) and S(1) • τ are X-homogeneous for the same color. If K is piecewise syndetic, then by Brown's lemma (Lemma 2.9), there is an OVW-line S ⊆ A <ω such that |S| = N n-1 , with S(0) ⊆ I, and a piecewise syndetic set P ⊆ K such that S(0) and S(1) • P are X-homogeneous for the same color. Then the lemma is satisfied and we are done.

Otherwise, the set J = I ∖ K is thick. Then for every OVW-line S ⊆ A <ω with |S| = N n-1 and S(0) ⊆ I, every τ ∈ J with S(1) • τ ⊆ I, we have S(0) and S(1) • τ are not X-homogeneous for the same color. Let σ n be such that A ≤Nn-1+1 • σ n ⊆ J, and let w n = x 0 σ n . We claim that σ n satisfies (3. Consider the embedding h : □

A <ω → C defined by h(a 0 • • • a n ) = w 0 [a 0 ] • • • w n [a n ]
It will be convenient to reformulate the previous lemma into the following equivalent lemma, which is in terms of piecewise syndetic sets instead of finite colorings of thick sets. One can indeed see a piecewise syndetic set as a particular coloring of a thick set, where the color is the witness of syndeticity. Lemma 3.6 (RCA 0 + IΣ 0 2 ). Let P ⊆ A <ω be a piecewise syndetic set. Then there is an OVW-line S ⊆ A <ω and a piecewise syndetic subset Q such that S(0) ⊆ P and S(1) • Q ⊆ P .

Proof. Say P = P ∩I, where P is m-syndetic and I is thick. By Lemma 2.10, the set J = {σ ∈ I : A ≤m •σ ⊆ I} is thick. Let X : J → A ≤m be defined by X(σ) = ρ such that ρσ ∈ P . Note that

X(σ) • σ ∈ P for all σ ∈ J. (3.2)
By Lemma 3.5, there is an OVW-line T ⊆ A <ω , a piecewise syndetic subset Q ⊆ J and a color ρ such that T (0) and

T (1) • Q are in color ρ of X. By (3.2), ρ • T (0), ρ • T (1) • Q ⊆ P . Thus the OVW-line S = ρ • T is as desired. □
We are now ready to prove Theorem 3.1.

Proof of Theorem 3.1. Let P ⊆ A <ω be a piecewise syndetic set. By Lemma 3.6, there an OVW-line S and a piecewise syndetic set P 0 ⊆ A <ω such that S(0) ⊆ P and S(1) • P 0 ⊆ P . Set T 0 = S(0) and let w 0 be the left variable word such that S(1) = S(0) • w 0 [A]. Note that T 0 is an OVW-tree of dimension 0.

Assume by induction T s is an OVW-tree over A of dimension s, w s is a left variable word and P s ⊆ A <ω is a piecewise syndetic set such that (a) T s ⊆ P and (b) T s (s) • w s [A] • P s ⊆ P. By Lemma 3.6, there is an OVW-line S and a piecewise syndetic set P s+1 ⊆ A <ω such that S(0) ⊆ P s and S(1)

• P s+1 ⊆ P s . Let T s+1 = T s ∪ (T s (s) • w s [A]
• S(0)) and let w s+1 be the left variable word such that S(1) = S(0) • w s+1 [A]. Note that T s+1 is an OVW-tree over A of dimension s + 1. It suffices to verify the induction assumption.

Claim 1: T s+1 ⊆ P . Indeed, by (a) T s ⊆ P and by (b) and S(0) ⊆ P s ,

T s+1 (s + 1) = T s (s) • w s [A] • S(0) ⊆ T s (s) • w s [A] • P s ⊆ P. Claim 2: T s+1 (s + 1) • w s+1 [A] • P s+1 ⊆ P . T s+1 (s + 1) • w s+1 [A] • P s+1 = T s (s) • w s [A] • S(0) • w s+1 [A] • P s+1 = T s (s) • w s [A] • S(1) • P s+1 ⊆ T s (s) • w s [A] • P s ⊆ P.
The four equalities are due to: definition of T s+1 , definition of w s+1 , S(1) • P s+1 ⊆ P s and (b). □ Remark 3.7. Although the proofs of Lemma 3.6 and Lemma 3.5 are over RCA, that is, RCA 0 with more induction, the proof of Theorem 3.1 holds in ACA 0 with restricted induction. Indeed, ACA 0 proves the existence of a countable coded ω-model of RCA 0 (see Theorem VIII.2.11 of Simpson [START_REF] Stephen | Subsystems of Second Order Arithmetic[END_REF]). Since every countable coded ω-model satisfies full induction, then every Π 1 2 consequence of RCA is provable in ACA 0 . Simply note that Lemma 3.6 and Lemma 3.5 are Π 1 2 statements.

Note that if the coloring is computable, then the sequences built in the proof of Theorem 3.1 are computable in any PA over ∅ ′ . Therefore, for any set P of PA degree over ∅ ′ , any computable instance of the Ordered Variable Word theorem admits a P -computable solution. We say that a problem P admits cone avoidance if for every pair of sets Z, C such that C ̸ ≤ C Z, every Z-computable instance of P admits a solution Y such that C ̸ ≤ T Z ⊕ Y . It admits strong cone avoidance if we relax the requirement on Z to be computable in the definition of cone avoidance. The following question remains open: Question 3.8. Does the Ordered Variable Word theorem admit cone avoidance or even strong cone avoidance? 4. A proof of the Density Ordered Variable Word theorem in ACA 0 Dodos, Kanellopoulos and Tyros proved in [START_REF] Dodos | A density version of the Carlson-Simpson theorem[END_REF] a density version of the Ordered Variable Word theorem, a stronger result where the color is fixed and of positive lim sup. The goal of this section is to show that their result holds in ACA 0 : Theorem 4.1 (Density Ordered Variable Word Theorem, [START_REF] Dodos | A density version of the Carlson-Simpson theorem[END_REF], ACA 0 ). Fix a finite alphabet A, and let D ⊆ A <ω be of positive upper density. Then there exists an OVW-tree T ⊆ D over A of dimension ω.

As for piecewise syndeticity, positive upper density is partition regular, so Theorem 4.1 implies the Ordered Variable Word theorem. Corollary 4.2 (ACA 0 ). For every finite alphabet A and every finite partition

C 0 ⊔ • • • ⊔ C ℓ-1 = A <ω ,
there is some color i < ℓ and an OVW-tree T ⊆ C i of dimension ω.

Proof. Let i < ℓ be such that lim sup r dens A r (C i ) > 0. By Theorem 4.1, there is an OVW-tree T ⊆ C i over A of dimension ω. □

The OVW-tree T of dimension ω of theorem 4.1 will be constructed as the union of a sequence of OVWtree of finite but increasing dimension. The "finitary part" of the proof of theorem 4.1 is the following theorem, which is a direct consequence of [ (1) L ′ is sufficiently big: card (L ′ ) ≥ n, and (2) D S is of sufficiently big density, at the length inside L ′ : for any r ∈ L ′ ,

dens A r-size(S) (D S ) > δ 2 8 × card (OVWLine(L 0 ))
where OVWLine(L 0 ) is the finite set of OVW-lines with set of levels included in L 0 .

In order to study the reverse mathematics of Theorem 4.1, we shall consider Theorem 4.3 as a blackbox. Its proof involves an elaborate, but finite, combinatorial machinery, which is elementary from a logical viewpoint. Theorem 4.3 for n = 1 implies the following lemma, which is the analog of Lemma 3.6, with piecewise syndetic largeness replaced by positive upper density. Proof. Let δ > 0 be such that the set L 1 = {r ∈ ω : dens A r (D) > δ} is is infinite. Let N 0 = N 0 (k, δ) and N 1 = N 1 (k, 1, δ), and let δ = δ 2 /(8 × card (OVWLine(L 0 ))). For each r ∈ L 1 , let (if it exists) S r ⊆ D by an OVW-line satisfying L(S) ⊆ L 0 and dens A r-size(S) r (D Sr ) > δ. By Theorem 4.3, there are at most N 1 many r for which S r does not exist. Since L 0 is finite, by the infinite pigeonhole principle, there is an OVW-line S so that the set L = {r ∈ L 1 : S r = S} is infinite. The set L is computable and S and L can both be found uniformly in any ∅ ′ -PA degree. □

We are now ready to prove Theorem 4.1. As mentioned in the introduction, many partition theorems admit higher-order counterparts. In the case of variable word theorems, an n-dimensional version consists of coloring n-variable words rather than words. The two applications of the variable word theorems that we are going to study in Section 6 and Section 7 involve their higher-order counterparts.

There exists a simple inductive proof of the higher-order version of the Carlson-Simpson lemma. The general idea consists considering the variables as part of the alphabet. Typically, the Carlson-Simpson lemma for dimension 1 and alphabet of size k uses ω applications the Carlson-Simpson lemma for dimension 0 and alphabet of size k + 1. The variables being treated as part of the alphabet, they will occur infinitely often in the solution. As a consequence, even using the Ordered Variable Word as the base statement, which is a stronger statement where each variable occurs finitely often, the resulting higher-order version yields only a solution to Carlson-Simpson's lemma.

The following inductive proof is standard in combinatorics. It essentially corresponds to the original proof of Carlson and Simpson [1, Section 2]. It was studied in the reverse mathematical setting by Dzhafarov, Flood, Solomon and Brown Westrick [6, Section 3.5]. We include the proof of the sake of completeness.

Theorem 5.1. For every n ∈ ω, ACA + 0 ⊢ ∀k∀ℓCSL n (k, ℓ). The proof uses induction on n. Let A be an alphabet of size k ; when we say ω-variable word, it means over A unless claimed otherwise. We will use the notion of prehomogeneous ω-variable word (see Definition 5.2) to reduce an ℓ-coloring of A <ω,n+1 to an ℓ-coloring of A <ω,n . Definition 5.2. An ω-variable word W over A is prehomogeneous for a coloring f : A <ω,n+1 → ℓ if for every s ∈ A <ω,n and t 0 , t 1 ∈ A <ω,n+1 such that s ⌢ x n is prefix of both t 0 and t

1 , f (W [t 0 ]) = f (W [t 1 ]).
For ω-variable words W, Ŵ and m ∈ ω, we write Ŵ ≤ m W iff Ŵ = W [V ] where V is an ω-variable word so that z 0 • • • z m-1 ≺ V . Clearly ≤ m is transitive and ≤ m+1 implies ≤ m . Lemma 5.3 (ACA 0 ). Let W be an ω-variable word, and s ∈ A <ω,n . There exists an ω-variable word Ŵ ≤ |s|+1 W and a color i such that for every t ∈ A <ω,n+1 with s ⌢ x n ⪯ t, we have f ( Ŵ [t]) = i.

Proof. Let  = A ⊔ {x 0 , . . . , x n }. We define f s : Â<ω → ℓ in the following way: for every u ∈ Â<ω ,

f s (u) = f (W [s ⌢ x n ⌢ u]
). Note that f s can be seen as an instance of CSL(k + n + 1, ℓ). Let U be an ωvariable word over  with variable set (y n ) n∈N such that f s is constant, of value i < ℓ on {U [u] : u ∈ Â<ω }. Replacing (x m : m ≤ n) in U by (z jm : m ≤ n) where j m is the first occurrence x m in s ⌢ x n , we obtain an ω-variable word Û (over A instead of over Â); and let

Ŵ = W [z 0 • • • z ⌢ |s| Û ].
The motivation to use Û is that for every word û over Â, there is a word

u over  such that Ŵ [s ⌢ x ⌢ n û] = W [s ⌢ x ⌢ n U [u]
] (this not necessarily true for other ŝ ∈ A <ω,n ). Therefore, for every t ∈ A <ω,n+1 with s ⌢ x n ⪯ t, say t = s ⌢ x ⌢ n û, we have, for some word u over Â,

f ( Ŵ [t]) = f ( Ŵ [s ⌢ x ⌢ n û]) = f (W [s ⌢ x ⌢ n U [u]]) = f s (U [u]) = i. Clearly Ŵ ≤ |s|+1 W
and is an ω-variable word (over A). Thus we are done. □

We are now ready to prove Theorem 5.1.

Proof of Theorem 5.1. The proof uses induction on n. The case n = 0 is a direct consequence of Theorem 4.1, since an ordered ω-variable word is a particular case of ω-variable word. Assume ∀k∀ℓCSL n (k, ℓ) holds and fix k, ℓ. We prove CSL n+1 (k, ℓ).

Let A be an alphabet of size k and fix a coloring f : A <ω,n+1 → ℓ. Iterating Lemma 5.3, there exists a sequence of ω-variable words

W = W 0 ≥ n+1 W 1 ≥ n+2 W 2 ≥ n+3 • • •
as well as a coloring on words g : A <ω,n → ℓ such that for every m ∈ ω, every s ∈ A <ω,n , every t ∈ A <ω,n+1 with s ⌢ x n ⪯ t and |s| = n + m, we have f (W m+1 [t]) = g(s); which implies f (W m[t]) = g(s) for all m ≥ m + 1. It is easy to see that the limit W ω = lim m W m exists (by definition of ≤ m ). Now for every s ∈ A <ω,n and t ∈ A <ω,n+1 with s ⌢ x n ⪯ t, we have (let m be sufficiently large),

f (W ω [t]) = f (W m[t]) = g(s).
That is, W ω is prehomogeneous for f . It remains to restrain the space so that g is constant. Let W ′ be the ω-variable word given by the application of CSL n (k, ℓ) to the coloring g, so that g • W ′ is constant for some color i < ℓ. Let t ∈ A <ω,n+1 and s ∈ A <ω,n be such that s ⌢ x n ⪯ t. Then

f (W ω [W ′ [t]]) = g(W ′ [s]) = i. Thus, W = W ω [W ′ ]
is a witness of the theorem. This completes the proof of Theorem 5.1. □

When constructing the prehomogeneous variable word W ω , we invoke CSL(k, ℓ) infinitely many times which blows up the complexity. However, it is unknown whether CSL(k, ℓ) holds in RCA 0 . Were it provable in RCA 0 , then CSL n (k, ℓ) and results on the Dual Ramsey Theorem and the Big Ramsey degree of universal triangle-free graph would be provable in ACA 0 . It is not even known whether RCA 0 implies CSL(2, ℓ).

Question 5.4 (Joe Miller and Solomon, [START_REF] Miller | Effectiveness for infinite variable words and the dual Ramsey theorem[END_REF]). Does RCA 0 imply CSL(k, ℓ)? The first application of the Carlson-Simpson lemma is a dual version of Ramsey's theorem. This was actually the theorem which motivated the proof of the Carlson-Simpson theorem. While Ramsey's theorem is about finite colorings of the integers, the Dual Ramsey theorem is about finite colorings of colorings.

For α ∈ ω + , we note (ω) α the class of partitions of ω in exactly α sets. Such a partition can be seen as a surjective ordered function from ω to α. Therefore (ω) α inherits of a natural topology from α ω . Given a partition p ∈ (ω) ω and α ∈ ω + , we write (X) ω for the class of Y ∈ (ω) α coarsening X, that is, for every n, m such that X(m) = X(n), then Y (m) = Y (n). Carlson and Simpson [START_REF] Carlson | A dual form of Ramsey's theorem[END_REF] proved the following theorem: Theorem 6.1 (Borel Dual Ramsey theorem). For any n, ℓ ∈ ω, let C 0 ∪ ... ∪ C ℓ-1 be a partition of (ω) n where each C i is a Borel set. Then there is partition X ∈ (ω) ω such that (X) n ⊆ C i for some i < ℓ.

The dual Ramsey theorem does not hold for arbitrary colorings. There exists in particular a 2-partition C 0 ∪ C 1 of (ω) 2 such that for all X ∈ (ω) ω , neither (X) 2 ⊆ C 0 nor (X) 2 ⊆ C 1 (see [START_REF] Carlson | A dual form of Ramsey's theorem[END_REF]Section 1.4]). On the other hand, the dual Ramsey theorem can be generalized to any coloring which admits the Baire property (see Prömel and Voigt [START_REF] Hans | Baire sets of k-parameter words are Ramsey[END_REF]). From a mathematical viewpoint, it is well-known that Borel classes have the Baire property, hence the Baire version of the Dual Ramsey theorem implies its Borel version. However, from a computational and reverse mathematical viewpoint, the situation is more complicated. Indeed, the proof that Borel classes have the Baire property is non-trivial, and requires a careful analysis of the way to represent Borel classes in second-order arithmetic.

Dzhafarov, Flood, Solomon and Westrick [START_REF] Dzhafarov | Effectiveness for the dual ramsey theorem[END_REF] studied the reverse mathematics of the various versions of the Dual Ramsey theorem, namely, its restrictions to the Baire, the Borel, and the open colorings. They proved that the Borel Dual Ramsey theorem implies the Baire version, which is itself equivalent to the Open Dual Ramsey theorem. All these variants were proven to hold in Π 1 1 -CA 0 by Slaman [START_REF] Slaman | A note on dual ramsey theorem[END_REF]. In their analysis, Dzhafarov and al. [START_REF] Dzhafarov | Effectiveness for the dual ramsey theorem[END_REF] reduced the Open Dual Ramsey theorem to a combinatorial statement, which they called the Combinatorial Dual Ramsey theorem: Theorem 6.2 (Combinatorial Dual Ramsey theorem). For any n, ℓ ≥ 2 let C 0 ∪...∪C ℓ-1 be a finite partition of ∅ <ω,n-1 , then there is a color i < ℓ and an ω-variable word W such that {W [u], u ∈ ∅ <ω,n-1 } ⊆ C i We will write ODRT n (ℓ) the statement of the Open Dual Ramsey theorem for ℓ-colorings of (ω) n and CDRT n (ℓ) the statement of the Combinatorial Dual Ramsey theorem for ℓ-colorings of ∅ <ω,n-1 . Dzhafarov and al. [START_REF] Dzhafarov | Effectiveness for the dual ramsey theorem[END_REF] proved that ODRT n (ℓ) and CDRT n (ℓ) are equivalent over RCA 0 . They proved CDRT n (ℓ) from the Carlson-Simpson lemma inductively as in Section 5, leaving the Carlson-Simpson lemma unproved, as a blackbox. The proof is optimal, in the following sense: Theorem 6.3. The following propositions are equivalent over RCA 0 :

(1) For all n, k, ℓ, CSL n (k, ℓ)

(2) For all n, ℓ > 2, CDRT n (ℓ)

Proof.

(1) clearly implies (2) since CDRT n (ℓ) is exactly CSL n-1 (0, ℓ). We just need to prove that (2) implies [START_REF] Carlson | A dual form of Ramsey's theorem[END_REF]. Let n, k, ℓ some integers, and we consider the statement CSL n (k, ℓ). Let A = {a 0 , ..., a k-1 } an alphabet of size k, and C 0 ⊔ • • • ⊔ C ℓ-1 a partition of A <ω,n . This induces a partition Ĉ0 ⊔ • • • ⊔ Ĉℓ-1 of ∅ ω,k+n by replacing the first k variables by a letter in A. Now, by using CDRT k+n+1 (ℓ), we have a color i and an ω-variable word Ŵ on alphabet ∅ such that { Ŵ [u], u ∈ ∅ <ω,k+n } ⊆ Ĉi . Then consider the ω-variable word W = Ŵ [a 0 a 1 ...a k-1 x 0 x 1 ...] on alphabet A. For all u ∈ A <ω,n , since the letters in a 0 a 1 ...a ⌢ k-1 u appear in order, this word can be seen as a k + n-variable word û ∈ ∅ ω,k+n . Therefore, since Ŵ [û] ∈ Ĉi , we also have The big Ramsey degree of B in A is the smallest L ∈ ω + such that A -→ (A) B k,L for every k ∈ ω, and a infinite structure A is said to have finite big Ramsey degrees if for all finite substructure of B, B has a finite big Ramsey degree in A. The study of big Ramsey degrees was initiated by Laver, who proved the order of rationals has finite big Ramsey degrees [START_REF] Devlin | Some partition theorems and ultrafilters on ω[END_REF].

Ŵ [a 0 a 1 ...a ⌢ k-1 u] = W [u] ∈ C i ,
Most recent results on big Ramsey degrees rely on a combinatorial core which is usually a tree partition theorem. The most famous one is Milliken's tree theorem, which was used by Devlin [START_REF] Devlin | Some partition theorems and ultrafilters on ω[END_REF] in 1979 to give a precise characterization of big Ramsey degrees on the order of rationals, and by Laflamme, Sauer, and Vuksanovic [START_REF] Laflamme | Canonical partitions of universal structures[END_REF] in 2006 to characterize the big Ramsey degrees of the Rado graph. The reverse mathematics of Milliken's tree theorem and its applications were studied by Anglès d'Auriac, Cholak, Dzhafarov, Monin and Patey [START_REF] Anglès D'auriac | Milliken's tree theorem and its applications: a computability-theoretic perspective[END_REF], who proved that they all hold in ACA 0 .

However, Milliken's tree theorem fails to serve as a combinatorial core to prove that some non-universal relational structures admit finite big Ramsey degrees. In 2020, Dobrinen [START_REF] Dobrinen | The Ramsey theory of the universal homogeneous triangle-free graph[END_REF] proved that the triangle-free Henson graph admits finite big Ramsey degrees by proving a combinatorial statement about coding trees, using an involved notion of forcing. More recently, Hubička [START_REF] Hubička | Big ramsey degrees using parameter spaces[END_REF] gave an alternative proof of Dobrinen's theorem using the higher-order Carlson-Simpson lemma as a combinatorial core. Although this proof is less accurate than the original proof of Dobrinen, it has the advantage of relying on a partition theorem with a known combinatorial proof. In this section, we analyse the proof by Hubička and show that it holds in ACA + 0 . The analysis is straightforward, but we include it for the sake of completeness.

By the usual back-and-forth argument, any computable copy of the triangle-free Henson graph is computably isomorphic. We will first enrich the set {0} <ω,1 of variable words over the unary alphabet {0} with a symmetric irreflexive binary relation E so that ({0} <ω,1 , E) is a universal triangle-free graph, hence computably isomorphic to H 3 . Definition 7.2. Let E be the symmetric binary relation on {0} <ω,1 defined as follows: for v, w ∈ {0} (2) Triangle-freeness condition: there is no i < |v| with v(i) = w(i) = x 0 . We write G the graph ({0} <ω,1 , E) One can see the set {0} <ω,1 as the full binary tree 2 <ω truncated from the set {0, 00, 000, . . . }. Based on this intuition, the previous construction is very similar to the one of Laflamme, Sauer, and Vuksanovic [START_REF] Laflamme | Canonical partitions of universal structures[END_REF] where they represent a Rado graph by the full binary tree with an edge relation based on the passing number property. The following lemma shows how the second property of the edge relation ensures that G is triangle-free. Lemma 7.3. G is triangle-free.

Proof. Assume by contradiction that we have three words s, t, u ∈ {0} <ω,1 , forming a triangle. Without loss of generality, we assume |s| < |t| < |u|. Therefore we must have t(|s|) = x 0 . But we also have u(|s|) = x 0 , and this contradicts the triangle-freeness condition between t and u. □

The triangle-freeness condition ensures that there will not be too many edges, the risk being that the resulting edge relation is too restrictive and that we lose universality. The following theorem shows that the edge relation is general enough. Theorem 7.4 (RCA 0 ). G is the universal triangle-free graph.

Proof. We define φ : H 3 → {0} <ω,1 with for all i, φ(i) = s where s is such that |s| = i and for all j < i :

• s(j) = x 0 if there is an edge between i and j in H • s(j) = 0 otherwise It is clear that φ is an embedding φ : H 3 → G therefore since G is triangle-free and by unicity of the universal triangle-graph, G is the universal triangle-free graph. □

The following observation shows that for every ω-variable word W , the induced subgraph ({W [u] : u ∈ {0} <ω,1 }, E) remains universal: Let us show that the triangle-freeness condition is preserved. Suppose there is some i < |u| such that u(i) = v(i) = x 0 . Then let j be the position of any occurrence of x i in W . We have W [u](j) = u(i) = v(i) = W [v](j) = x 0 . Conversely, suppose there is some j < |W [u]| such that W [u](j) = W [v](j) = x 0 . Then W (j) = x i for some i < |u|. In particular, W [u](j) = u(i) and W [v](j) = v(i), so u(i) = v(i) = x 0 . □ Remark 7.6. The previous lemma is precisely the reason why we consider variable words over {0} rather than binary words, and use the Carlson-Simpson lemma rather than Milliken's tree theorem. Indeed, identifying {0} <ω,1 as 2 <ω ∖ {0, 00, 000, . . . }, an application of Milliken's tree theorem yields a strong infinite subtree S.

The issue that the graph (S, E) is not universal in general. For example, if there is some n ∈ ω such that every w ∈ S satisfies w(n) = 1, then the graph (S, E) is an anticlique, by the triangle-freeness condition.

The following notions of envelope and embedding types are now standard in the study of big Ramsey degrees. We define the appropriate notions under the scope of variable words : Definition 7.7. Let A an alphabet and S a set of finite variable words over A. An envelope of S is a (< ω)-variable word W such that for all s ∈ S there is a variable word t such that W [t] = s. We say that W is minimal if there is no envelope of S with fewer variables than W .

A simple computation shows that if W is a minimal envelope of S, then it has at most 2 |S| + |S| -1 variables (see [START_REF] Hubička | Big ramsey degrees using parameter spaces[END_REF]Proposition 3.1]). (7.1) In what follows, given two graphs F, G, we write G F for the set of all embeddings from F to G. We write F ∼ =φ G iff F is isomorphic to G via φ. Theorem 7.8 (RCA 0 +∀kCSL 2 n +n-1 (1, k)). Let F be a finite triangle-free graph of size n, there is an integer ℓ such that for any integer k > 0 and any finite coloring χ : G F → k, there exists f ∈ G G such that χ attain at most ℓ colors on f (G) F .

Proof. Let  be {0} ∪ {x 0 }. Firstly, we note that χ give rise to a coloring χ ≤ T χ of {0} <ω,2 n +n-1 , where χ(u) records the coloring profile of ⟨φ : T ⊆ Â≤2 n +n-1 and F ∼ =φ u[T ]⟩, namely χ(u) = ⟨χ(φ) : T ⊆ Â≤2 n +n-1 and F ∼ =φ u[T ]⟩.

By CSL 2 n +n-1 (1, k) (for some sufficiently large k), there exists an ω-variable word W (over {0}) such that {W [u] : u ∈ {0} <ω,2 n +n-1 } is homogeneous for χ. By Lemma 7.5, the graph {W [t] : t ∈ Â<ω } is isomorphic to G. It suffices to show that for any embedding φ of F into the graph {W [t] : t ∈ Â<ω }, we have χ(φ) ∈ L where L is the range of χ, namely for every u ∈ {0} <ω,2 n +n-1 , let û = W

  [ϵ] = 01, W [0] = 01010, W [1] = Ø110, W [01] = 010101010001 and W [10] = 011100011001.

2. 1 . 1 .Definition 2 . 5 .

 1125 Positive upper density. We define the density of a set D inside a set U as dens U (D) = card(D∩U ) card(U ) . A set D ⊆ A <ω has positive upper density if lim sup n→∞ dens A n (D) > 0

Lemma 2 . 6 (

 26 RCA 0 ). Suppose D ⊆ A <ω has positive upper density, and E ⊔ F = D. Then either E or F has positive upper density.

  1). Fix any b ∈ A, any OVW-line S ⊆ A <ω with |S| = N n-1 and S(0) ⊆ I. Clearly, w n [b] = bσ n ∈ J and S(1) • w n [b] ⊆ I (since A ≤Nn-1+1 • σ n ⊆ J). Therefore, S(0) and S(1) • w n [b] are not X-homogeneous for the same color. Thus σ n satisfies (3.1).

  , and let Y = X • h. Note that by choice of (σ n ) n∈ω , dom h = A <ω . By Theorem 3.3, there is an OVW-line T ⊆ A <ω , a letter b ∈ A, and a color i ∈ C such that T (0) and T (1)•b are both Y -homogeneous for color i. Let S ⊆ J be the OVW-line obtained by taking the image of T by h. In particular, S(0) = h(T (0)) and S(1) • w M [b] = h(T (1) • b) and |S| = N M -1 , where M = |T | + 1. By definition of h and Y , S(0) and S(1) • w M [b] are both X-homogeneous for color i. This contradicts (3.1).

5 ,

 5 Proposition 7.5]. For a set D ⊆ A <ω , a finite OVW-line S, let D S = {σ : S(1) • σ ⊆ D}.

Theorem 4 . 3 ([ 5 ,

 435 Proposition 7.5], RCA). For all k ∈ N and alphabet A of size k, for any δ > 0, there exists N 0 = N 0 (k, δ) such that for any n ∈ ω, there exists N 1 = N 1 (k, n, δ) such that the following is true. For any L 0 < L 1 ⊆ N with |L 0 | > N 0 and |L 1 | > N 1 , and for any D with dens A r (D) > δ for all r ∈ L = L 0 ∪ L 1 , there exists an OVW-line S ⊆ D with L(S) ⊆ L 0 , and a set L ′ ⊆ L 1 such that:

Lemma 4 . 4 (

 44 RCA). Let k and alphabet A of size k. For every positive upper density set D ⊆ A <ω , there is an OVW-line S, a positive upper density set D ⊆ A <ω such that S(0) ⊆ D and S(1) • D ⊆ D.

Proof of Theorem 4 . 1 .

 41 It is similar to the proof of Theorem 3.1 mutatis mutandis, using Lemma 4.4 instead of Lemma 3.6 and positive upper density instead of piecewise syndeticity. □ As explained in Remark 3.7, although the proofs of Theorem 4.3 and of Lemma 4.4 are over RCA, the proof of Theorem 4.1 holds in ACA 0 with restricted induction. 5. A proof of the Higher-Order Carlson-Simpson Lemma in ACA + 0

6 .

 6 A proof of the Open Dual Ramsey theorem in ACA + 0

  3 the universal triangle-free graph, or the triangle-free Henson graph. Given integers k, ℓ ∈ ω, structures A, B and C we write C -→ (A) B k,ℓ for the following statement: Definition 7.1. C -→ (A) B k,ℓ : For any partition C 0 ∪ ... ∪ C k-1 of the embeddings of B in A there is an embedding f : C → A such that all the embeddings of B in f (C) intersect at most ℓ many C i 's.

Lemma 7 . 5 (

 75 RCA 0 ). Let W be an ω-variable word. Then for every u, v∈ {0} <ω,1 , uEv iff W [u]EW [v]. In particular, ({W [u] : u ∈ {0} <ω,1 }, E) is the universal triangle-free graph. Proof. Say |u| < |v|. Then |W [u]| < |W [v]|. The passing number property is preserved: v(|u|) = x 0 iff W [v](|W [u]|) = x 0 .

  [u], L = {χ(φ) : T ⊆ Â≤2 n +n-1 and F ∼ =φ û[T ]}.Let S ⊆ Â<ω so that W [S] = φ(F ); which means |S| = n. By (7.1), there is a u ∈ {0} <ω,2 n +n-1 andT ⊆ Â≤2 n +n-1 such that u[T ] = S. Let û = W [u] ∈ {0} <ω,2 n +n-1 . Clearly, F ∼ =φ û[T ]. So χ(φ) ∈ {χ(φ) : T ⊆ Â≤2 n +n-1 and F ∼ =φ û[T ]} = L.The last equality follows by homogeneity of χ on {W [u] : u ∈ {0} <ω,2 n +n-1 } ∋ û. Thus we are done. □ Corollary 7.9 (ACA + 0 ). The triangle-free Henson graph admits finite big Ramsey degrees.Proof. Immediate by Theorem 7.8 and Theorem 5.1. □

  meaning that W is a solution to our instance of CSL n (k, ℓ). □ Thanks to our new analysis of the Carlson-Simpson lemma, we prove that the Combinatorial Dual Ramsey theorem holds in ACA + 0 . It follows that the open and Baire versions of the Dual Ramsey theorem also hold in ACA + 0 , which is a dramatical improvement from the previous bound of Π1 1 -CA 0 . Big Ramsey degree of the universal triangle-free graph using variable wordsOur second application comes from Structural Ramsey Theory. We consider graphs as relational structures and denote by H

	Corollary 6.4. For all n ≥ 2, ACA + 0 ⊢ ∀ℓODRT n (ℓ)
	7.

The name "Carlson-Simpson Lemma" is sometimes used to refer to the Ordered Variable Word theorem in the literature of combinatorics.

Acknowledgement

The authors are thankful to Natasha Dobrinen, Jan Hubička and Keita Yokoyama for interesting comments and discussions. The authors are also thankful for the anonymous referee for improvement suggestions. Angles d'Auriac and Patey are partially supported by grant ANR "ACTC" #ANR-19-CE48-0012-01. Lu Liu is supported by NSFC of Hunan Province with grant number 2022JJ30676.