Hindman’s theorem: an ultrafilter argument in second order arithmetic. (English) Zbl 1214.03046

Hindman’s theorem states that for any finite coloring of the natural numbers there is an infinite sequence of numbers all of whose finite sums have the same color. Like many statements of infinite combinatorics, Hindman’s theorem can be proved by a direct combinatorial argument or by proving the existence of a certain type of ultrafilter. This paper formalizes the Galvin-Glazer ultrafilter proof of Hindman’s theorem in second-order arithmetic. This requires careful reformulation of the proof to avoid the use of higher-order objects. The resulting proof can be carried out in the subsystem \(\Pi^1_1\)-TR\(_0\). This is currently the best known upper bound on the strength of an ultrafilter proof of Hindman’s theorem, but is well above the ACA\(_0^+\) upper bound on an analysis of a combinatorial proof of Hindman’s theorem by A. R. Blass, J. L. Hirst, and S. G. Simpson [Contemp. Math. 65, 125–156 (1987; Zbl 0652.03040)].


03F35 Second- and higher-order arithmetic and fragments
03B30 Foundations of classical theories (including reverse mathematics)


Zbl 0652.03040
Full Text: DOI arXiv


[1] DOI: 10.1090/S0002-9904-1977-14316-4 · Zbl 0355.54005
[2] DOI: 10.1090/conm/065/891245
[3] DOI: 10.1016/0097-3165(74)90103-4 · Zbl 0289.05009
[4] DOI: 10.1007/s001530050095 · Zbl 0909.03040
[5] Lectures on topological dynamics (1969) · Zbl 0193.51502
[6] Subsystems of second order arithmetic (1999) · Zbl 0909.03048
[7] Algebra in the Stone-Čech compactification 27 (1998) · Zbl 0918.22001
[8] Journal of Combinatorial Theory, Series A 17 pp 1– (1974)
[9] Hindmari’s theorem, ultrafilters, and reverse mathematics 69 pp 65– (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.