Pi04 conservation of the Ordered Variable Word theorem
Published:
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_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.
Recommended citation: Q. Le Houérou and L. Levy Patey (2024). "Pi04 conservation of the Ordered Variable Word theorem.".
Download Paper