Reverse-Mathematical Strength of Hindman's Theorem

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Work in second-order arithmetic over $\mathsf{RCA}_0$, the base theory with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction. The strength of a principle means which subsystems prove it and which subsystems it implies over that base; equivalence requires both implications. Here $\mathsf{ACA}_0$ adds comprehension for all arithmetical formulas. For a set $X$, its Turing jump $X'$ codes which oracle computations with oracle $X$ halt; $X^{(\omega)}=\bigoplus_{n\geq0}X^{(n)}$ joins all finite jumps. The theory $\mathsf{ACA}_0^+$ is $\mathsf{RCA}_0+\forall X\,\exists X^{(\omega)}$. Hindman’s theorem $\mathsf{HT}$ says that, for every finite colouring of $\mathbb N$, some infinite $A\subseteq\mathbb N$ has all nonempty finite sums of distinct members of $A$ of one colour.

Statement recorded in the supplied source.

Is $\mathsf{HT}$ equivalent to $\mathsf{ACA}_0^+$, equivalent to $\mathsf{ACA}_0$, or strictly between these two theories? [S2]

Short English statement

Does Hindman’s finite-sums theorem require exactly arithmetic comprehension, exactly the existence of all finite jumps joined together, or a strength strictly between them?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500109 (AMR-074-0109). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Antonio Montalbán, Open Questions in Reverse Mathematics, author preprint dated 17 August 2010, Question 9, printed p. 5. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.