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.

We study the parameterized complexity of the problem to decide whether a given natural number n satisfies a given $\Delta _0$-formula $\varphi (x)$; the parameter is the size of $\varphi $. This parameterization focusses attention on instances where n is large compared to the size of $\varphi $. We show unconditionally that this problem does not belong to the parameterized analogue of $\mathsf {AC}^0$. From this we derive that certain natural upper bounds on the complexity of our parameterized problem imply certain separations of classical complexity classes. This connection is obtained via an analysis of a parameterized halting problem. Some of these upper bounds follow assuming that $I\Delta _0$ proves the MRDP theorem in a certain weak sense.

We prove that if the linear-time and polynomial-time hierarchies coincide, then every model of Π1(ℕ) + ¬Ω1 has a proper end-extension to a model of Π1(ℕ), and so Π1(ℕ) + ¬Ω ⊢ BΣ1. Under an even stronger complexity-theoretic assumption which nevertheless seems hard to disprove using present-day methods, Π1(ℕ) + ¬Exp ⊢ BΣ1. Both assumptions can be modified to versions which make it possible to replace Π1(ℕ) by IΔ0 as the base theory.

We also show that any proof that IΔ0 + ¬Exp does not prove a given finite fragment of BΣ1 has to be “nonrelativizing”, in the sense that it will not work in the presence of an arbitrary oracle.