The first-order part of the Ordered Variable Word theorem

Introduction

In 1984, Carlson and Simpson [3] proved a dual form of Ramsey’s theorem, using as a combinatorial core a partition theorem about variable words, now known as the Ordered Variable Word theorem for words. A word over a finite alphabet $A$ is a finite sequence $a_0 \cdots a_{n-1}$ of elements of $A$. We denote by $A^{<\omega}$ the set of words over $A$. An ordered $\omega$-variable sequence over $A$ is an infinite sequence over the alphabet $A \sqcup\{x_0, x_1, \ldots\}$ such that each variable kind appears at least once, and such that for each $i \in\mathbb{N}$, the last occurrence of $x_i$ appears before the first occurrence of $x_{i+1}$. Given an ordered $\omega$-variable sequence $W$ and a word $u = a_0 \cdots a_{n-1}$, $W[u]$ denotes the word obtained from $W$ by replacing every occurrence of $x_i$ with $a_i$, and cutting before the first occurrence of $x_n$.

We denote by $\mathrm{OVW}^{0}$, standing for Ordered Variable Word theorem, the statement of Theorem 1.1. Carlson [2] later proved a higher-order generalization of $\mathrm{OVW}^{0}$ to colorings of finite-dimensional ordered variable words. The Ordered Variable Word theorem belongs to a family of tree partition theorems [7, 27] with applications in Structural Ramsey Theory [9, 19, 29]$.

From a meta-mathematical viewpoint, the Ordered Variable Word theorem was extensively studied in reverse mathematics and computability theory [26, 10, 24, 1, 22]. Recently, Liu and Patey [25] made significant advances in the understanding of the computability-theoretic features of the Ordered Variable Word theorem, and proved the following weakly low basis theorem:

By an isomorphism theorem for weak König’s lemma [13], there is a correspondence between $\Pi^1_1$-conservation theorems over $\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$ and proving formalized weakly low basis theorems over $\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$. In this article, we formalize Theorem 1.2 over $\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$, and deduce the following main theorem:

This improves a theorem by Le Houér​​ou and Patey [22] who proved that $\mathrm{RCA}_0+\mathrm{OVW}^{0}$ is $\forall\Pi^0_4$-conservative over $\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$, where a formula is $\forall\Pi^0_4$ iff it is of the form $\forall X\varphi(X)$ for a $\Pi^0_4$-formula $\varphi$. Note that this conservation is sharp, as $\mathrm{OVW}^{0}$ restricted to unary alphabet is the infinite pigeonhole principle ($\mathrm{RT}^1$), which is equivalent to $\mathrm{B}\Sigma^0_2$ over $\mathrm{RCA}_0$ (see Hirst [17 Theorem 6.4]).

Tree theorem for singletons

One can see the Ordered Variable Word theorem as a tree partition theorem as follows: Given a finite alphabet $A$ and an ordered $\omega$-variable sequence $W$ over $A$, letting $T_W=\{W[u]:u\in A^{<\omega}\}$, $(A^{<\omega},\preceq)$ and $(T_W,\preceq)$ are tree-isomorphic, with witness map $u\mapsto W[u]$. The Ordered Variable Word theorem is therefore a generalization of the tree theorem of Chubb, Hirst, and McNicholl [7]. The tree theorem for singletons ($\mathrm{TT}^1$) states that for every $\ell\ge1$ and every coloring $f:2^{<\omega}\to\ell$, there is an infinite $f$-monochromatic set $S\subseteq2^{<\omega}$ such that $(S,\preceq)$ and $(2^{<\omega},\preceq)$ are tree-isomorphic.

The first-order part of the tree theorem for singletons was a long-standing open question. Corduan, Groszek and Mileti [8] proved that $\mathrm{TT}^1$ is not provable over $\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$. Chong, Wang and Yang [6] proved that $\mathrm{RCA}_0+\mathrm{TT}^1$ is $\forall\Pi^0_3$-conservative over $\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$ and Chong, Li, Wang and Yang [4] proved that $\mathrm{RCA}_0+\mathrm{TT}^1+\mathrm{P}\Sigma^0_1$ is $\Pi^1_1$-conservative over $\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2+\mathrm{P}\Sigma^0_1$, where $\mathrm{P}\Sigma^0_1$ is equivalent to the principle of the totality of Ackermann’s function (see Kreuzer and Yokoyama [21]).

Proof. By Main Theorem 1.3, it suffices to prove that $\mathrm{RCA}_0 \vdash\mathrm{OVW}^0 \to\mathrm{TT}^1$. Let $f : 2^{<\omega} \to k$ be an instance of $\mathrm{TT}^1$. By $\mathrm{OVW}^0$, there is an ordered $\omega$-variable sequence $W$ over $A = \{0,1\}$ such that the set $\{W[u] : u \in A^{<\omega}\}$ is $f$-monochromatic. Note that $\{W[u] : u \in A^{<\omega}\}$ is a $\mathrm{TT}^1$-solution to $f$. $\square$

Together with the recent proof by Hwang [20] that Ramsey’s theorem for pairs and two colors ($\mathrm{RT}^2_2$) is a $\Pi^1_1$-conservative extension of $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$, this can be considered as one more argument towards the robustness of the levels of the inductive hierarchy for capturing the first-order parts of natural second-order statements.

Note that Dzhafarov, Solomon and Yokoyama [12] defined a semantic notion of first-order part of a Weihrauch problem $P$, corresponding to the strongest Weihrauch problem whose solutions range over $\mathbb{N}$, and which is reducible to $P$. Dzhafarov, Solomon and Valenti [11] proved that the Weihrauch first-order part of $\mathrm{TT}^1$ and $\mathrm{RT}^1$ coincide.

Prerequisites

Before proving our main theorem, we recall some fundamental concepts of weak arithmetics which will be used in the proof, and fix some notation for variable words.

Weak theories

Let $\mathrm{PA}^{-}$ be the axioms of a discrete ordered commutative semiring and exp be the statement of the totality of the exponential.

We are in particular interested in the schemata $I\Sigma^0_n$ and $I\Pi^0_n$ corresponding to $\Sigma^0_n$ and $\Pi^0_n$-formulas, respectively. The induction scheme can be extended to $\Delta^0_n$-predicates as follows:

The least induction scheme for $\Gamma$-formulas ($\mathrm{L}\Gamma$) informally says for every $\Gamma$-formula $\varphi$, if $\varphi(x)$ holds for some $x$, then there is a least such $x$. The least induction scheme for $\Delta^0_n$-predicates ($\mathrm{L}\Delta^0_n$) is defined accordingly. The following collection (or bounding) principle plays an important role in weak arithmetic:

The following table summarizes the hierarchy of bounding and induction principles over $\mathrm{PA}^{-}+I\Delta^{0}_{0}+\exp$. See Paris and Kirby [28] for a reference:

Induction	Collection	Least principle
:	:	:
$\mathrm{I}\Sigma^{0}_{2}\equiv\mathrm{I}\Pi^{0}_{2}$	:	$\mathrm{L}\Pi^{0}_{2}\equiv\mathrm{L}\Sigma^{0}_{2}$
$\mathrm{I}\Delta^{0}_{2}$	$\mathrm{B}\Sigma^{0}_{2}\equiv\mathrm{B}\Pi^{0}_{1}$	$\mathrm{L}\Delta^{0}_{2}$
$\mathrm{I}\Sigma^{0}_{1}\equiv\mathrm{I}\Pi^{0}_{1}$	:	$\mathrm{L}\Pi^{0}_{1}\equiv\mathrm{L}\Sigma^{0}_{1}$
$\mathrm{I}\Delta^{0}_{1}$	$\mathrm{B}\Sigma^{0}_{1}\equiv\mathrm{B}\Pi^{0}_{0}$	$\mathrm{L}\Delta^{0}_{1}$

Thanks to the correspondence between computability and definability, the computable sets are exactly the ones which are definable by a $\Delta_{1}$-predicate. The following scheme is therefore known as recursive comprehension scheme:

The base theory of reverse mathematics is $\mathrm{RCA}_{0}$, standing for Recursive Comprehension Axiom, defined as $\mathrm{PA}^{-}+\Delta^{0}_{1}$-CA+$I\Sigma^{0}_{1}$. More recently, Simpson and Smith [31] defined a weaker theory, $\mathrm{RCA}^{*}_{0}$, which consists of $\mathrm{PA}^{-}+\Delta^{0}_{1}$-CA+$I\Delta^{0}_{1}+\exp$. In particular, $\mathrm{RCA}^{*}_{0}\vdash\mathrm{B}\Sigma^{0}_{1}$. The $\mathrm{RCA}_{0}$-provably total computable functions are exactly the primitive recursive ones, while the $\mathrm{RCA}^{*}_{0}$-provably total computable functions are the elementary recursive ones.

Models of arithmetic

Structures in second-order arithmetic are of the form

where $M$ is the first-order part, $\mathcal{S}\subseteq\mathcal{P}(M)$ is the second-order part, $0,1\in M$, $+,\cdot:M^{2}\to M$ are binary operators and $<\subseteq M^{2}$ is a binary relation. We shall abbreviate it with $(M,\mathcal{S})$. Given a structure $\mathcal{M}=(M,\mathcal{S})$, we will not assume in general that a set $X\subseteq M$ belongs to $\mathcal{S}$.

Fix a primitive recursive Gödel numbering $\langle\cdot\rangle$ of mathematical objects. A mathematical object is $M$-coded if its Gödel number belongs to $M$.

Given a structure $\mathcal{M} = (M,\mathcal{S}) \models\mathrm{PA}^{-} + \mathrm{I}\Delta^{0}_{0} + \mathrm{exp}$, the $\mathrm{I}\Sigma^{0}_{n}$ (resp. $\mathrm{I}\Pi^{0}_{n}$, $\mathrm{I}\Delta^{0}_{n}$) scheme is equivalent to the statement “Every $\Sigma^{0}_{n}$-definable (resp. $\Pi^{0}_{n}$-definable, $\Delta^{0}_{n}$-definable) set is $\mathcal{M}$-regular” (see Hájek and Pudlák [15 Chapter 2]).

The notion of $\omega$-extension should not be confused with that of $\omega$-model. In particular, $\mathcal{M}_0$ need not be the standard integers. Given a structure $\mathcal{M} = (M,\mathcal{S})$ and a set $G \subseteq M$, we denote by $\mathcal{M}[G]$ the $\omega$-extension of $\mathcal{M}$ whose second-order part consists of all $\Delta^{1}_{1}(\mathcal{S},G)$-definable sets.

A structure $\mathcal{M} = (M,\mathcal{S})$ is topped by a set $Y \in\mathcal{S}$ if $\mathcal{S}$ is the collection of all $\Delta^{1}_{1}(Y)$-definable sets.

For a structure $\mathcal{M} = (M,\mathcal{S})$, a set $X \subseteq M$ is $\mathcal{M}$-bounded if there is some $b \in M$ such that for every $x \in X$, $x < b$. Otherwise, $X$ is $\mathcal{M}$-unbounded. In models of $\mathrm{RCA}^{*}_{0}$, some sets might be unbounded, but have finite cardinality. The statement “Every unbounded set is in bijection with $\mathbb{N}$” is actually equivalent to $\Sigma^{0}_{1}$-induction. We can therefore use indistinctly infinite and unbounded in models of $\mathrm{RCA}_{0}$.

Formal computability theory

In what follows, fix a structure $\mathcal{M} = (M,\mathcal{S}) \models\mathrm{RCA}^{*}_{0}$.

Turing reducibility is robust in models of $\mathrm{RCA}^{*}_{0}$. In particular, it is transitive. Fix a universal $\Sigma^{0}_{1}$-formula $\varphi(X,e)$.

If $X \leq_T Y$ with $Y' \in\mathcal{S}$, then $X' \in\mathcal{S}$ and $X' \leq_T Y'$. Moreover $Y \leq_T Y'$ and $Y' \not\leq_T Y$.

Weak König’s lemma

A tree is a subset $T \subseteq\mathbb{N}^{<\omega}$ which is closed under prefix. A binary tree is a tree $T \subseteq2^{<\omega}$. A path through a tree $T$ is a sequence $P \in\mathbb{N}^{\mathbb{N}}$ such that every initial segment belongs to $T$. We write $[T]$ for the (possibly empty) collection of all paths through $T$.

We shall write $\mathrm{WKL}_{0}^{*}$ and $\mathrm{WKL}_{0}$ for the theories $\mathrm{RCA}_{0}^{*}+\mathrm{WKL}$ and $\mathrm{RCA}_{0}+\mathrm{WKL}$, respectively. Simpson and Smith [31] proved the following theorem:

We shall also need the following formalized low basis theorem. Note that since $\mathcal{M}\models\mathrm{B}\Sigma_{2}^{0}$, then $\mathcal{M}[Y']\models\mathrm{RCA}_{0}^{*}$, so the notion of Turing reducibility is still robust.

Recall that given an index of a co-$X$-c.e. tree $T$, one can computably obtain an index of a primitive $X$-recursive infinite tree $S$ such that if $[T]\ne\varnothing$, then $[S]=[T]$. Let $(T_n)_{n\in\mathbb{N}}$ be an effective listing of all $X$-primitive recursive infinite binary trees.

Weak König’s lemma can actually prove the existence of paths through a larger family of finitely branching trees: the ones for which one can uniformly bound the maximum label at every level. A tree $T\subseteq\mathbb{N}^{<\omega}$ is $g$-bounded for some function $g:\mathbb{N}\to\mathbb{N}$ if for every $\sigma\in T$ and $x<|\sigma|$, $\sigma(x)<g(x)$.

Variable words

We shall adopt the same notation conventions as [25] for variable words, that we now recall. Those definitions have to be understood in the formal setting. In particular, $\omega$ will be interpreted by $M$ rather than $\omega$ in a structure $\mathcal{M}=(M,S)$.

A finite or infinite word over a finite alphabet $A$ is a map $w:\alpha\to A$ for some $\alpha\leq\omega$. We write $|w|$ for its length $\alpha$. Given $\beta\leq\omega$, an ordered $\beta$-variable word over $A$ is a word $w$ over the alphabet $A\sqcup\{x_i:i<\beta\}$ where each $x_i$ appears at least once, and the last occurrence of $x_i$ appears before the first occurrence of $x_{i+1}$. We write $A^{\alpha,\beta}_{<}$ and $A^{<\alpha,\beta}_{<}$ for the sets of all ordered $\beta$-variable word of length $\alpha$, and smaller than $\alpha$, respectively. Given $\gamma\leq\beta\leq\omega$, a $\beta$-variable word $w$ over $A$ and a $\gamma$-variable word $u$ of length $|u|\leq\beta$, we write $w[u]$ for the $\gamma$-variable word over $A$ where each occurrence of $x_j$ is replaced with $u(j)$, and cut before the first occurrence of $x_{|u|}$. If $|u|=\beta$, then $|w[u]|=|w|$.

Given ordered variable words $u$ and $v$, when doing the concatenation $u\cdot v$, we will always assume that the variable kinds of $u$ and $v$ are from disjoint spaces, so that there is no variable kind clash. Given $\gamma\leq\beta\leq\omega$ and an ordered $\beta$-variable word $w$, we let $\operatorname{OSub}^{\gamma}_{A}(w)$ be the set of all ordered $\gamma$-variable words generated by $w$, that is,

Most of the time, the alphabet $A$ will be clear from context, and we shall simply write $\operatorname{OSub}^{\gamma}(w)$ for $\operatorname{OSub}^{\gamma}_{A}(w)$. Let

Note that $\operatorname{OSub}(w)$ includes in particular $\operatorname{OSub}^{0}(w)$, that is, the set of words generated by $w$. We write $\operatorname{WSub}(w)$ for $\operatorname{OSub}^{0}(w)$. Last, we define

The sets $\operatorname{OSub}^{\gamma,=}(w)$, $\operatorname{OSub}^{\gamma,*}(w)$, $\operatorname{WSub}^{=}(w)$ and $\operatorname{WSub}^{*}(w)$ are defined accordingly.

Conservation theorem

The goal of this section is to prove the following one-step extension theorem.

Before proving Proposition 3.1, let us deduce the $\Pi^1_1$-conservation theorem from it. First, by Simpson and Smith [31], one can always find a set $P$ satisfying the hypothesis of Proposition 3.1. We therefore deduce the following corollary:

Proof. Let $\mathcal{M}'=(M,\Delta_2\text{-}\operatorname{Def}(Y,M))$. Since $\mathcal{M}\models\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$, then $\mathcal{M}'\models\mathrm{RCA}^*_0$. Let $T\subseteq2^{<M}$ be a $\Delta_2(Y)$-definable infinite tree such that for every path $P\in[T]$, $P\gg Y'$. In particular, $T\in\mathcal{M}'$, so by Proposition 2.11, there is a set $P\subseteq M$ with $P\gg Y'$ such that $\mathcal{M}'[P]\models\mathrm{RCA}^*_0$. By Proposition 3.1, there is an ordered $M$-variable sequence $W$ over $A$ such that $\operatorname{WSub}^*(W)$ is $f$-monochromatic and $P\geq_T(W\oplus Y)'$. Since $\mathcal{M}'[P]\models\mathrm{RCA}^*_0$, then by Lemma 2.10, $\mathcal{M}[W]\models\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$. □

Iterating Corollary 3.2, one obtains the following $\omega$-extension theorem:

Proof. Using Corollary 3.2, construct a countable sequence of structures $\mathcal{M}=\mathcal{M}_0,\mathcal{M}_1,\mathcal{M}_2,\ldots$ such that for every $n\in\omega$,

(1) $\mathcal{M}_{n+1}=(M,\mathcal{S}_{n+1})$ is a topped model $\omega$-extending $\mathcal{M}_n$;

(2) $\mathcal{M}_{n+1}\models\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2$;

(3) For every $M$-bounded alphabet $A$, every $\ell\in M$ and every coloring $f:A^{<M}\to\ell$ in $\mathcal{S}_n$, there is some $k\in\omega$ and some ordered $M$-variable sequence $W$ over $A$ such that $\operatorname{WSub}^*(W)$ is $f$-monochromatic and $W\in\mathcal{S}_k$.

Then $\mathcal{M}_\infty=(M,\bigcup_n\mathcal{S}_n)$ is an $\omega$-extension of $\mathcal{M}$ such that $\mathcal{M}_\infty\models\mathrm{RCA}_0+\mathrm{B}\Sigma^0_2+\mathrm{OVW}^0$. □

We can now prove the main theorem:

Proof. Suppose that $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2 \nvdash\forall X\varphi(X)$ for some arithmetic formula $\varphi$. By the completeness theorem for Henkin models and the downward Löwenheim–Skolem theorem, there is a countable model $\mathcal{M}_0 = (M, \mathcal{S}_0) \models\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2 + \exists X\neg\varphi(X)$. Let $X \in\mathcal{S}_0$ be such that $\mathcal{M}_0 \models\neg\varphi(X)$ and $\mathcal{M}_1 = (M, \Delta^0_1\text{-}\operatorname{Def}(X,M))$. Then $\mathcal{M}_1$ is a countable model $\mathcal{M}_1 \models\mathrm{RCA}_0 \wedge\mathrm{B}\Sigma^0_2 \wedge\neg\varphi(X)$ which is topped by $X$. By Proposition 3.3, there is an $\omega$-extension $\mathcal{M}_2 = (M, \mathcal{S}_2)$ of $\mathcal{M}_1$ such that $\mathcal{M}_2 \models\mathrm{RCA}_0 + \mathrm{OVW}^0$. Since $\mathcal{S}_2 \supseteq\mathcal{S}_1$, then $X \in\mathcal{S}_2$, and since $\varphi$ is arithmetic, $\mathcal{M}_2 \models\neg\varphi(X)$, so $\mathrm{RCA}_0 + \mathrm{OVW}^0 \nvdash\forall X\varphi(X)$.

We now turn to the proof of Proposition 3.1. In what follows, fix a countable model $\mathcal{M} = (M,\mathcal{S})$ topped by a set $Y \in\mathcal{S}$, fix an $M$-bounded alphabet $A$, some number of colors $\ell\in M$, a set $P \gg Y'$ and a coloring $f : A^{<M} \to\ell$ in $\mathcal{S}$ as in the hypothesis of Proposition 3.1.

As in [25], we will design a notion of forcing such that any sufficiently generic filter produces an infinite, finitely branching tree $T$. Every infinite path through $T$ is an ordered $M$-variable word $W$ over $A$ which is $f$-monochromatic at infinitely many levels, that is, such that for infinitely many $n \in M$, $W[A^n] = \{W[u] : u \in A^n\}$ is $f$-monochromatic. Then, an application of the infinite pigeonhole principle (which holds over $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$) yields an $\mathrm{OVW}^0$-solution.

Then, we will construct a $Y'$-computable 1-generic decreasing sequence of forcing conditions, so that every path through the generic tree is $\mathrm{GL}_1$. The construction being internal, the main difficulty is to simultaneously decide the jump on initial segments of the generic set, using the technique of Shore blocking.

The notion of forcing being Mathias-like, with infinite reservoirs, we first fix a Scott ideal to which belong the reservoirs. By Proposition 2.12 and Lemma 2.14, there is a set $Q = \bigoplus_{a \in M} X_a$ such that $(Q \oplus Y)' \leq_T Y'$ and $Q$ codes the Scott ideal $\{X_a : a \in M\}$.

Notion of forcing

The following notion of $\mathbb{P}$-branch is a coded representation of the corresponding notion in [25].

As noted in [25], if $(v,b) \leq(u,a)$, we do not have in general $v \in\operatorname{OSub}^{*}(u \cdot X_a)$. One easily checks that $\mathbb{P}$-branch extension is transitive, and that if $(v,b) \leq(u,a)$, then $[v,b] \subseteq[u,a]$. Note that the extension relation is $\Pi_{1}(Q)$: $W' \in\operatorname{OSub}^{M}(W)$ is $\Pi_{1}(W \oplus W')$.

The denotation of a $\mathbb{P}$-precondition $(I,a)$ is $[I,a] = \bigcup_{v \in I}[v,a]$. As explained in [25], the denotation of a $\mathbb{P}$-branch or of a $\mathbb{P}$-precondition may not contain any ordered $M$-variable word which is $f$-monochromatic at infinitely many levels, but the $f$-matching property ensures that a $\mathbb{P}$-condition contains sufficiently many stems for it to be the case (see [25 Lemma 3.12]).

Transitivity of $\mathbb{P}$-precondition extension is inherited from that of $\mathbb{P}$-branch extension, and if $(J,b) \leq(I,a)$, then $[J,b] \subseteq[I,a]$. Last, it is useful to give an explicit syntactical definition of forcing relation for $\Sigma^{0}_{1}$ and $\Pi^{0}_{1}$-formulas that satisfies “forcing implies truth” property for every (i.e. even non-generic) filters.

Every $\Sigma^{0}_{1}$ formula $\varphi(G)$ can be expressed in normal form as $\exists k\psi(G \mathord{\upharpoonright} k)$, where $\psi(\sigma)$ is a monotonous $\Delta^{0}_{0}$ formula, that is, if $\psi(\sigma)$ and $\sigma\preceq\tau$, then $\psi(\tau)$ holds. We shall always assume that the $\Sigma^{0}_{1}$-formulas are in normal form.

Assuming the $\Sigma^{0}_{1}$-formula $\varphi(G)$ is in Kleene’s normal form, if $(u,a) \Vdash\varphi(G)$ and $(v,b) \leq(u,a)$, then $(v,b) \Vdash\varphi(G)$. Moreover, $\varphi(G)$ holds for every $G \in[u,a]$. The same holds for $\neg\varphi(G)$.

Graham-Rothschild tree

The notion of Graham-Rothschild tree is a fundamental notion in the combinatorics of the Ordered Variable Word theorem. Intuitively, it is an infinite, finitely branching tree whose infinite paths are ordered $\omega$-variable words and such that every level contains “sufficiently many” stems so that the corresponding P-precondition is a P-condition.

It is based on infinite iterations of the Hales-Jewett theorem [16]. This finitary theorem is the bootstrap of a large part of Ramsey theory. The original proof used double induction and yielded a bound $HJ$ growing as fast as the Ackermann function. Shelah [30] gave a new proof yielding primitive recursive bounds:

For simplicity, given a finite alphabet $A$ and some $\ell\ge1$, we might simply write $HJ(A,\ell)$ for $HJ(\operatorname{card} A,\ell)$. Let $(\ell_n)_{n\in\mathbb{N}}$ be inductively defined by

Here, $\operatorname{card} A^{HJ(A,\ell_n),1}$ is the number of ordered $1$-variable words of length $HJ(A,\ell_n)$ over $A$. Then, let $(t_n)_{n\in\mathbb{N}}$ be inductively defined by

The Graham-Rothschild tree for $\ell$-colorings over alphabet $A$ is the tree $\mathcal{T}_{A,\ell}$ whose level $n$ consists of all ordered $n$-variable words $w$ of length $t_n$, such that for every $s<n$, the variable $x_s$ appears only within the positions $[t_s,t_{s+1})$. This tree is partially ordered by the prefix relation. The following property was proven by Liu and Patey [25] over $\mathrm{RCA}_0$.

For the purpose of Shore blocking, we shall be interested in products of GR-trees: Given $d\in M$, let $\mathcal{T}_{A,\ell}^{d}$ be the tree such that the nodes at level $n$ are exactly the $d$-tuples of nodes at level $n$ in $\mathcal{T}_{A,\ell}^{d}$. Any infinite path through $\mathcal{T}_{A,\ell}^{d}$ is a $d$-tuple $\vec{V}=(V_0,\ldots,V_{d-1})$ of ordered $M$-variable words over $A$. Given an ordered variable word $u$, we write $\vec{V}[u]$ for

Deciding formulas simultaneously

We now turn to the heart of the formalized weakly low basis theorem, which is proving the density of the set of conditions deciding a bounded quantity of formulas simultaneously. Iteratively applying the forcing question of Liu and Patey [25] would require too much induction strength. One therefore has to develop some new combinatorics. The following forcing question is essentially [25 Definition 3.16] reformulated to emphasize the fact that it is a question within a branch rather than a precondition:

Recall that $\mathcal{T}_{A,k}$ is the Graham-Rothschild tree for $k$-colorings over alphabet $A$ (see § 4.2).

The following $\Sigma^0_1$-extension lemma is an immediate adaptation of [25 Lemma 3.19]. The main difference is that one allows the formulas to depend on the stem $v$. Note that this difference is only presentational since one can define $\varphi(G) := \varphi_{G\upharpoonright t}(G)$ where $t$ is the common length of all elements in $J$.

Proof. By $\mathrm{B}\Sigma^0_1(X_a \oplus Y)$, there is a common level witness $n$ for all $v \in J$. Note that the forcing questions are monotonic in their level witnesses, so they still hold for a simultaneous witness. Moreover, the map $(I,a,J) \mapsto n$ is in $\Delta_1(Q \oplus Y)$, hence $\Delta_1(Y')$.

Let $m$ be the position of the first occurrence of $x_{t_n}$ in $X_a$ (where $t_n$ is the length of all the nodes at level $n$ in $\mathcal{T}_{A,\ell\cdot\operatorname{card} I}$). One can find $Q \oplus Y$-computably some $M$-finite set $K$ of all $v \cdot X_a[\hat{u}]$ such that either

1. $v \in J$, $\hat{u} \in\operatorname{OSub}(u)$ for some $u$ at level $n$ of $\mathcal{T}_{A,\ell\cdot\operatorname{card} I}$ and $\varphi_v(v \cdot X_a[\hat{u}])$;

or

2. $v \in I \setminus J$ and $\hat{u} \in A^{t_n}$.

Moreover, one can $Q \oplus Y$-computably find some $b \in M$ such that $X_b = X_a\mathbin{\upharpoonright}\infty$, with the variables renamed accordingly. The verification that $(K,b)$ is the desired extension is exactly the proof of [25 Lemma 3.19] and is formalizable over $\mathrm{RCA}_0$. $\square$

The following $\Pi^0_1$-extension lemma constitutes the new combinatorial content of the article. For this lemma, we need to restrict ourselves to families of $\Sigma^0_1$-formulas $(\varphi_{v,i})_{v\in I, i<r}$ which satisfy some strong structural properties, that is, $\varphi_{v,i}(G) \to\varphi_{v,i+1}(G)$ for every $G$, every $v \in I$ and every $i < r - 1$. We shall then generalize it to arbitrary families in Lemma 3.14 thanks to a counting trick.

Proof. Let $\mathcal{T}^d=\mathcal{T}^d_{A,\ell\cdot\operatorname{card} I}$ be the $d$-product of GR-trees as in the paragraph after Lemma 3.10. Given $\vec{V}=(V_0,\ldots,V_{d-1})\in[\mathcal{T}^d]$, let

Note that $X_a[\vec{V}][u]=X_a[\vec{V}[u]]$ for every finite $u$. Let $\mathcal{C}^\beta$ be the $\Pi^1_1(X_a\oplus Y)$ class of all $\vec{V}\in[\mathcal{T}^d]$ such that

for every $v\in I$ with $\beta(v)>0$.

Furthermore, one can find an index of an $X_a\oplus Y$-primitive recursive tree $\mathcal{T}^d_\beta$ such that $[\mathcal{T}^d_\beta]=\mathcal{C}^\beta$ computably in $(a,d,\beta)$. Here, the forcing relation is natural generalization of Definition 3.8(2). Let

Equivalently, $E(d,\beta)$ holds iff $\mathcal{T}^d_\beta$ has a node at every level, so $E(d,\beta)$ is a $\Pi^1_1(\mathcal{Q}\oplus Y)$ property of $(a,d,\beta)$. Since $\mathcal{M}\models\mathrm{B}\Sigma^0_2$ and $(\mathcal{Q}\oplus Y)'\leq_TY'$, $\mathcal{M}[\mathcal{Q}]\models\mathrm{B}\Sigma^0_2$, so the set

is $M$-regular, and so is the function $g:2+r\cdot\operatorname{card} I\to1+r\cdot\operatorname{card} I$ defined by

Note that $E(d,\mathbf{0})$ holds for every $d\leq1+r\cdot\operatorname{card} I$, where $\mathbf{0}:I\to\{0,\ldots,r\}$ is the constant map $v\mapsto0$. So the function $g$ is well-defined. Moreover, if $E(d,\beta)$ holds, then so does $E(d+1,\beta)$. Indeed, appending any path $V'$ of the Graham-Rothschild tree does not affect the $\Pi^0_1$ forcing relation. It follows that the function $g$ is non-decreasing. By the finite pigeonhole principle (which holds over $\mathrm{RCA}_0$), there is some least $d^*$ such that $g(d^*+1)=g(d^*)$. Let $\beta:I\to\{0,\ldots,r\}$ be such that

and $E(d^*,\beta)$ holds. Let $\vec{V}\in C_{\beta}^{d^*}$ be in the Scott ideal $\{X_c:c\in M\}$ and $b$ be such that $X_b=X_a[\vec{V}]$. Then $(I,b)$ is a $\mathbb{P}$-precondition and is $f$-matching since only the reservoir is restricted. Moreover, Item (1) holds by definition of $C_{\beta}^{d^*}$.

We claim that Item (2) holds. Suppose for the contradiction that $\beta(v)<r$ and $(v,b)\not\Vdash_{\ell\cdot\operatorname{card} I}\varphi_{v,\beta(v)}(G)$ for some $v\in I$. The tree

is $M$-unbounded. Let $V'\in[U]$ in the Scott ideal $\{X_c:c\in M\}$. Then $(v,X_b[V'])\Vdash\neg\varphi_{v,\beta(v)}(G)$. Let $\beta'$ be equal to $\beta$, except that $\beta'(v)=\beta(v)+1\le r$. Note that $(\vec{V},\vec{V}')\in C_{\beta'}^{d^*+1}$, so $E(d^*+1,\beta')$ holds. Moreover, since $g$ is non-decreasing and $d^*$ is the least such that $g(d^*+1)=g(d^*)$, we have $d^*\le r\cdot\operatorname{card} I$, so $d^*+1$ belongs to the domain of $g$. So

contradicting the choice of $d^*$. So Item (2) holds. This completes the proof of the claim.

Last, all the steps of the construction are effective. The table of $E$ and the function $g$ are computed from $M$-finitely many bits of $(Q\oplus Y)'\le_T Y'$. The search for $d^*$ and $\beta$ is bounded. So $b$ and $\beta$ are computed by a $\Delta_1(Y')$ function. This completes the proof of Lemma 3.13. □

We now combine Lemma 3.13 and Lemma 3.12 to prove a simultaneous decision lemma, which is the Shore blocking counterpart of [25 Lemma 3.20].

Proof. For every $v\in I$ and $i\le r$, let $\psi_{v,i}(G)$ be the $\Sigma_1(Y)$-formula

Note that the formulas $(\psi_{v,i})_{v\in I,i<r}$ satisfy the hypothesis of the $\Pi^0_1$-extension lemma (Lemma 3.13), so there is a $\mathbb{P}$-condition $(I,b)\le(I,a)$ and $\beta:I\to\{0,\ldots,r\}$ such that for every $v\in I: (a) if $\beta(v)>0$, then $(v,b)\Vdash\neg\psi_{v,\beta(v)-1}(G)$; (b) if $\beta(v)<r$, then $(v,b)\not\Vdash_{\ell\cdot\operatorname{card} I}\psi_{v,\beta(v)}(G)$.

Let $J=\{v\in I:\beta(v)<r\}$. By (b) and the $\Sigma^{0}_{1}$-extension lemma applied to $(I,b)$, $J$ and $(\psi_{v,\beta(v)})_{v\in J}$, there is some $\mathbb{P}$-condition $(K,c)\leq(I,b)$ such that $\psi_{v,\beta(v)}(\hat{v})$ holds for every $v\in J$ and every $\hat{v}\in K$ extending $v$.

Fix $v\in I$ and $\hat{v}\in K$ extending $v$. Item (1) holds by Definition 3.8(1). By (b), letting $S_{\hat{v}}=\{i<r:\varphi_{v,i}(\hat{v})\}$, $\operatorname{card}S_{\hat{v}}\geq r-\beta(v)$. Moreover, by (a), $\operatorname{card}S_{\hat{v}}\leq r-\beta(v)$, so $\operatorname{card}S_{\hat{v}}=r-\beta(v)$. Suppose for the contradiction that Item (2) fails, that is, suppose that $(\hat{v},c)\not\Vdash\neg\varphi_{v,i}(G)$ for some $i\in r\setminus S_{\hat{v}}$. Then there is some finite $w\in[\hat{v},c]$ such that $\varphi_{v,i}(w)$ holds. Since $\hat{v}\preceq w$, then by monotonicity, $\varphi_{v,j}(w)$ holds for every $j\in S_{\hat{v}}\cup\{i\}$. These are $r-\beta(v)+1$ formulas. In particular, $\beta(v)>0$, and $w\in[v,b]$ contradicts (a).

The effectiveness follows from that of Lemma 3.13 and Lemma 3.12. □

Forcing the requirements

We are going to force two kind of requirements:

• (H) Homogeneity: we want to ensure that for the generic $M$-ordered variable word $G$ will be $f$-monochromatic at $M$-unboundedly many levels;

• (L) Weak lowness: we want to decide initial segments of the jump of $G\oplus Y$ simultaneously for segments of $M$-unbounded length.

Given some $t\in M$, let $\varphi_t(G)$ be the following $\Sigma_{1}(Y)$-formula:

The following lemma is a straightforward adaptation of Liu and Patey [25 Lemma 3.21] which holds over $\mathrm{RCA}_0$:

We can therefore use the simultaneous decision lemma in a very general form to obtain the desired density lemma for homogeneity requirements:

The following density lemma for weak lowness requirements exploits the full power of the simultaneous decision lemma:

Proof. Apply Lemma 3.14 with $\varphi_{v,e}(G) := \Phi_e^{G\oplus Y}(e) \downarrow$ for every $v \in I$.

Proof of Proposition 3.1

We now turn to the proof of Proposition 3.1. Construct the following $Y'$-computable decreasing sequence of $\mathbb{P}$-conditions

by stages as follows. First, $I_0 = \{\epsilon\}$, where $\epsilon$ is the empty sequence, and $X_{a_0}$ is the ordered $M$-variable word $x_0x_1x_2\cdots$. Assume $(I_s,a_s)$ has been defined. Let $r(s) = \max\{s,t(I_s),a_s\}$, where $t(I_s)$ is the common length of the elements of $I_s$. Using Lemma 3.16 and Lemma 3.17, one can $Y'$-computably find a $\mathbb{P}$-condition $(I_{s+1},a_{s+1})$ such that

(1) for every $v \in I_{s+1}$, $(v,a_{s+1}) \Vdash\varphi_{r(s)}(G)$;

(2) for every $v \in I_{s+1}$ and every $e < r(s)$, $(v,a_{s+1})$ decides $\Phi_e^{G\oplus Y}(e)$.

The set $J$ of all stages $s$ such that $(I_s,a_s)$ is defined forms a $\Sigma_1(Y')$ cut in $M$, which might be proper. Note that by $\Pi^0_1$-induction in $\mathcal{M}[Q]$, for every $s < t \in J$, $(I_s,a_s) \ge(I_t,a_t)$.

Proof. If $J = M$, then since $r(s) \ge s$, $R$ is $M$-unbounded. If $J \ne M$, then if $R$ were $M$-bounded, $J$ would be a proper $\Delta_1(Y')$ cut, contradicting the fact that $\mathcal{M}[Y'] \models\mathrm{I}\Delta^0_1$. Last, by (1), $t(I_{s+1}) \ge r(s)$, so $L$ is $M$-unbounded.

Let $\mathbb{T}$ be the downward-closure of $\bigcup_{s\in J} I_s$.

Proof. $\mathbb{T}$ is $M$-unbounded since $L$ is $M$-unbounded. Moreover, by length-homogeneity of the set of stems of a $\mathbb{P}$-precondition and the definition of the $\mathbb{P}$-precondition extension relation, $\mathbb{T}$ is $Y'$-computably bounded and $\Delta_1(Y')$: to know whether some node $w$ belongs to $\mathbb{T}$, search $Y'$-computably for the least stage $s$ such that $t(I_s) \ge|w|$, and check whether $w$ is an initial segment of any element of $I_s$.

Since $\mathcal{M}[P] \models\mathrm{RCA}^{*}_{0}$ and $P \gg Y'$, by Lemma 2.15, $P$ computes an $\mathcal{M}$-infinite path $G \in[\mathbb{T}]$. Note that for every $s$, $G \in[I_s,a_s]$. By (1), there are $\mathcal{M}$-unboundedly many levels $n$ such that $G[A^n] = \{G[v] : v \in A^n\}$ is $f$-monochromatic.

Proof. Given $e \in\mathcal{M}$, to decide whether $\Phi_e^{G \oplus Y}(e) \mathord{\downarrow}$, $P$-computably search for some $s \in J$ such that $r(s) > e$. Let $v \in I_{s+1}$ be such that $v \prec G$. By (2), $\Phi_e^{G \oplus Y}(e) \mathord{\downarrow}$ iff $\Phi_e^{v \oplus Y}(e) \mathord{\downarrow}$. The second part of the claim follows from Lemma 2.10.

By the infinite pigeonhole principle ($\mathrm{RT}^{1}_{\ell}$) which holds over $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$ (see Hirst [17 Theorem 6.4]), there is some color $\ell^* < \ell$ and some $\mathcal{M}$-unbounded set $H = \{h_0 < h_1 < \cdots\} \subseteq\mathcal{M}$ in $\mathcal{M}[G]$ such that $G[A^n]$ is $f$-monochromatic for color $\ell^*$ for every $n \in H$. Let $\widehat{G} = G[V]$ where $V(i) \in A$ if $i \notin H$ and $V(i) = x_t$ if $i = h_t$. Then $\operatorname{WSub}^{*}(\widehat{G})$ is $f$-monochromatic for color $\ell^*$. Moreover, $(\widehat{G} \oplus Y)' \leq_T (G \oplus Y)' \leq_T P$. This completes the proof of Proposition 3.1.

Open questions

The Ordered Variable Word theorem can be weakened to allow the variable kind to be interleaved, and occur infinitely often. This is known as the Carlson-Simpson Lemma CSL. Its zero-dimensional version (CSL$^0$) is an immediate consequence of OVW$^0$, and is therefore $\Pi^1_1$-conservative over $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$.

The one-dimensional version for $\ell$ colors, CSL$^1_\ell$, is a generalization of the tree theorem for pairs and $\ell$ colors ($\mathrm{TT}^2_\ell$), which itself generalizes Ramsey’s theorem for pairs and $\ell$ colors ($\mathrm{RT}^2_\ell$). Hwang [20] proved that $\mathrm{RCA}_0 + \mathrm{RT}^2_2$ is a $\Pi^1_1$-conservative extension of $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$, and Le Houér​ou and Patey [18] proved that $\mathrm{RCA}_0 + \mathrm{CSL}^1_2$ is a $\forall\Pi^0_4$-conservative extension of $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$.

Question 4.1. Is $\mathrm{RCA}_0 + \mathrm{CSL}^1_2$ $\Pi^1_1$-conservative over $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$?

Question 4.2. Is $\mathrm{RCA}_0 + \mathrm{TT}^2_2$ $\Pi^1_1$-conservative over $\mathrm{RCA}_0 + \mathrm{B}\Sigma^0_2$?

AI disclaimer

The original idea of formalizing the weakly low basis theorem for OVW$^0$ from Liu and Patey [25] using the techniques of Le Houér​ou, Patey and Yokoyama [23] came from the author. Claude Opus 5.5 (Anthropic) was used to prove the $\Pi^0_1$-extension lemma (Lemma 3.13) which is a core lemma in the proof. The proof was completely rewritten by the author for clarity.