\input zb-basic
\input zb-ioport
\iteman{io-port 06040394}
\itemau{Towsner, Henry}
\itemti{A simple proof and some difficult examples for Hindman's theorem.}
\itemso{Notre Dame J. Formal Logic 53, No. 1, 53-65 (2012).}
\itemab
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 [{\it A. Blass}, {\it J. Hirst} and {\it S. 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 open problem to determine the precises strength, in the sense of reverse mathematics, of Hindman's theorem.
\itemrv{Alexander Kreuzer (Lyon)}
\itemcc{}
\itemut{Hindman's theorem; reverse mathematics; Ramsey theory}
\itemli{doi:10.1215/00294527-1626518 euclid:ndjfl/1336586237}
\end