A computable analysis of variable words theorems

TL;DR

This paper investigates the computability and reverse mathematical strength of the Carlson-Simpson lemma related to variable words, establishing its properties within formal systems and connecting it to the finite union theorem.

Contribution

It provides a detailed computability-theoretic analysis of the variable words theorems and proves the Ordered Variable word for binary strings in ACA0, advancing understanding of their logical strength.

Findings

Proved the Ordered Variable word for binary strings in ACA0.

Analyzed the reverse mathematical strength of the Carlson-Simpson lemma.

Connected the lemma to the finite union theorem in the context of reverse mathematics.

Abstract

The Carlson-Simpson lemma is a combinatorial statement occurring in the proof of the Dual Ramsey theorem. Formulated in terms of variable words, it informally asserts that given any finite coloring of the strings, there is an infinite sequence with infinitely many variables such that for every valuation, some specific set of initial segments is homogeneous. Friedman, Simpson, and Montalban asked about its reverse mathematical strength. We study the computability-theoretic properties and the reverse mathematics of this statement, and relate it to the finite union theorem. In particular, we prove the Ordered Variable word for binary strings in ACA0.