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

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 \cdots \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 }_4^0$-conservative over~${\mathsf{RCA}}_0+\mathsf{B}{\Sigma }_2^0$. 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.

arXiv comment19 pages