$\Pi^0_4$ conservation of the Ordered Variable Word theorem

TL;DR

This paper proves that the Ordered Variable Word theorem (a tree partition theorem) is conservative over a weak base system, showing it does not imply the stronger system ACA_0, and thus clarifies its logical strength.

Contribution

It establishes the $oldsymbol{ ext{Pi}}^0_4$-conservation of OVW over RCA_0 plus BΣ^0_2, providing the first such result for a principle not implying ACA_0.

Findings

OVW is $oldsymbol{ ext{Pi}}^0_4$-conservative over RCA_0 + BΣ^0_2

OVW does not imply ACA_0 over RCA_0

First principle with known separation from ACA_0 involving only non-standard models

Abstract

A left-variable word over an alphabet~$A$ is a word over~$A \cup \{\star\}$ whose first letter is the distinguished symbol~$\star$ standing for a placeholder. The Ordered Variable Word theorem ($\mathsf{OVW}$), also known as Carlson-Simpson's theorem, is a tree partition theorem, stating that for every finite alphabet~$A$ and every finite coloring of the words over~$A$, there exists a word $c_0$ and an infinite sequence of left-variable words $w_1, w_2, \dots$ such that $\{ c_0 \cdot w_1[a_1] \cdot \dots \cdot w_k[a_k] : k \in \mathbb{N}, a_1, \dots, a_k \in A \}$ is monochromatic. In this article, we prove that $\mathsf{OVW}$ is $\Pi^0_4$-conservative over~$\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2$. This implies in particular that $\mathsf{OVW}$ does not imply $\mathsf{ACA}_0$ over~$\mathsf{RCA}_0$. This is the first principle for which the only known separation from~$\mathsf{ACA}_0$ involves non-standard models.