A simple proof and some difficult examples for Hindman's theorem (Q424579)

The author gives a new, simplified proof of Hindman's theorem that formalizes in the system \(\mathsf{ACA}^+\). This is slightly weaker than the best known upper bound \(\mathsf{ACA}^+_0\) (note the subscript 0 which indicates that induction is restricted to \(\Sigma^0_1\) formulas) on the strength of Hindman's theorem, see [\textit{A. R. Blass}, \textit{J. L. Hirst} and \textit{S. G. Simpson}, ``Logical analysis of some theorems of combinatorics and topological dynamics'', Contemp. Math. 65, 125--156 (1987; Zbl 0652.03040)]. Moreover, the author introduces a technique to construct instances of Hindman's theorem which have computationally difficult solutions. He uses this technique to show that parts of his new proof are optimal. Also, he constructs an instance which has no \(\Sigma_2\) solutions. This improves the best known lower bound which was \(\Delta_2\). This research is connected to the long-standing open problem to determine the precise strength, in the sense of reverse mathematics, of Hindman's theorem.