The first-order part of the Ordered Variable Word theorem
Abstract
An ordered ω-variable sequence over a finite alphabet~A is an infinite sequence over the extended alphabet A sqcup { x0, x1, … }, where each variable kind appears at least once, and the last occurrence of xi appears before the first occurrence of xi+1. The Ordered Variable Word theorem states that for every finite coloring of the words over a finite alphabet~A, there is an ordered ω-variable sequence~W over~A such that every word induced by substituting variables with letters, and cutting before the first undefined variable, has the same color. In this article, we prove that the Ordered Variable Word theorem is Π11-conservative over RCA0 + BΣ02. It follows that the tree theorem for singletons by Chubb, Hirst, and McNicholl is Π11-conservative over RCA0 + BΣ02, answering a long-standing open question. Lemma 3.13 was found by Claude Opus 5.5 (Anthropic).
Related
- Structural conditions on trust-region radius updates. Part I: first-order convergence and complexity
- Wolff Potential and Birkhoff's Ergodic Theorem in Grand Variable Herz Spaces
- Kernel representations of fractional gradient bilinear forms. Part II. Variable coefficients
- Order convergence in ordered vector spaces: compactness, atoms, pervasiveness, and ice cream spaces
- Thermodynamic Formalism Out of Equilibrium Part III: Local Limit Theorem and Statistical Properties
BibTeX
@misc{patey2026firstorder,
title = {{The first-order part of the Ordered Variable Word theorem}},
author = {Ludovic Patey},
howpublished = {HAL},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.27643},
eprint = {2610.27643},
archivePrefix = {arXiv},
url = {https://hal.science/hal-05820552v1},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - The first-order part of the Ordered Variable Word theorem
AU - Ludovic Patey
PY - 2026
DA - 2026/10/19
PB - HAL
DO - 10.48550/arxiv.2610.27643
UR - https://hal.science/hal-05820552v1
AB - An ordered ω-variable sequence over a finite alphabet~A is an infinite sequence over the extended alphabet A sqcup { x_0, x_1, … }, where each variable kind appears at least once, and the last occurrence of x_i appears before the first occurrence of x_i+1. The Ordered Variable Word theorem states that for every finite coloring of the words over a finite alphabet~A, there is an ordered ω-variable sequence~W over~A such that every word induced by substituting variables with letters, and cutting before the first undefined variable, has the same color. In this article, we prove that the Ordered Variable Word theorem is Π^1_1-conservative over RCA_0 + BΣ^0_2. It follows that the tree theorem for singletons by Chubb, Hirst, and McNicholl is Π^1_1-conservative over RCA_0 + BΣ^0_2, answering a long-standing open question. Lemma 3.13 was found by Claude Opus 5.5 (Anthropic).
ER -