Effectiveness of Hindman's theorem for bounded sums

TL;DR

This paper investigates the logical strength of restricted versions of Hindman's Theorem with bounded sums and colors, revealing their non-provability in certain base systems and their implications for computability and reverse mathematics.

Contribution

It establishes the non-provability of specific bounded sum versions of Hindman's Theorem in RCA_0 and shows their equivalence to stronger systems like ACA_0 and SRT^2_2.

Findings

Existence of a computable 2-coloring with no infinite monochromatic sum set

HT^{ extless=2}_2 implies SRT^2_2 in RCA_0

HT^{ extless=3}_3 has solutions computing 0'

Abstract

We consider the strength and effective content of restricted versions of Hindman's Theorem in which the number of colors is specified and the length of the sums has a specified finite bound. Let $\mathsf{HT}^{\leq n}_k$ denote the assertion that for each $k$-coloring $c$ of $\mathbb{N}$ there is an infinite set $X \subseteq \mathbb{N}$ such that all sums $\sum_{x \in F} x$ for $F \subseteq X$ and $0 < |F| \leq n$ have the same color. We prove that there is a computable $2$-coloring $c$ of $\mathbb{N}$ such that there is no infinite computable set $X$ such that all nonempty sums of at most $2$ elements of $X$ have the same color. It follows that $\mathsf{HT}^{\leq 2}_2$ is not provable in $\mathsf{RCA}_0$ and in fact we show that it implies $\mathsf{SRT}^2_2$ in $\mathsf{RCA}_0$. We also show that there is a computable instance of $\mathsf{HT}^{\leq 3}_3$ with all solutions computing $0'$. The proof of this result shows that $\mathsf{HT}^{\leq 3}_3$ implies $\mathsf{ACA}_0$ in $\mathsf{RCA}_0$.