Hindman's Theorem

A famous and important Ramsey-type result is Hindman's theorem:

For any coloring of $\mathbb{N}$ with finitely many colors, there exists an infinite set $H\subseteq\mathbb{N}$ such that all sums of finite subsets of H have the same color.

Hindman's theorem is well known to be closely related to the Auslander/Ellis theorem in topological dynamics:

For every state x in a compact dynamical system, there exists a state y which is proximal to x and uniformly recurrent.

(A compact dynamical system consists of a compact metric space X and a continuous function $T:X\to X$. A state $x\in X$ is said to be uniformly recurrent if for all $\epsilon>0$ there exists msuch that for all n there exists k<m such that $d(T^{n+k}x,x)<\epsilon$. Two states $x,y\in X$ are said to be proximal if for all $\epsilon>0$ there exist infinitely many n such that $d(T^nx,T^ny)<\epsilon$.)

There has been a great deal of interest in the constructive or effective aspect of Hindman's theorem and the Auslander/Ellis theorem. Some of the known proofs are highly set-theoretical and cannot even be formalized in second-order arithmetic. For an extensive discussion, including several proofs of Hindman's theorem, see [12].

I conjecture that Hindman's theorem and the Auslander/Ellis theorem are equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$. The known partial results in this direction are in Blass/Hirst/Simpson [3]. There we showed that Hindman's theorem and the Auslander/Ellis theorem are provable in $\mathsf{ACA}_0^{+}$, which consists of $\mathsf{ACA}_0$ plus ``for all $A\subseteq\mathbb{N}$, the $\omega$th Turing jump $A^{(\omega)}$ of A exists''. The proof of Hindman's theorem in $\mathsf{ACA}_0^{+}$ involves a delicate effectivization of Hindman's original proof. We also obtained a reversal by showing that Hindman's theorem implies $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$. The problem here is to close the gap between $\mathsf{ACA}_0$ and $\mathsf{ACA}_0^{+}$.