$\Pi^0_4$ conservation of a Carlson-Simpson lemma for 1-variable words

Abstract

Carlson and Simpson proved that for every finite coloring of the 1-variable words over a finite alphabet~$A$, there is an infinite $\omega$-variable word on which all the 1-variable words are monochromatic. This statement for $\ell$-colorings, written $\mathsf{CSL}^1_\ell$, is known to be strictly weaker than $\mathsf{ACA}_0$. We prove that $\mathsf{RCA}_0 + \mathsf{CSL}^1_2$ is a $\forall \Pi^0_4$-conservative extension of $\mathsf{RCA}_0 + \mathsf{B}Sigma_2$. Among its consequences, it implies that neither the indivisibility of the universal triangle-free Henson graph for 2-colorings, nor the tree theorem for pairs and two colors, imply $\Sigma^0_2$-induction. This answers a question of Chong, Li, Wang and Yang.