Hindman's theorem, ultrafilters, and reverse mathematics
Jeffry L. Hirst · Journal of Symbolic Logic · 2004
Abstract Assuming CH. Hindman [2] showed that the existence of certain ultrafilters on the power set of the natural numbers is equivalent to Hindman's Theorem. Adapting this work to a countable setting formalized in RCA0, this article proves the equivalence of the existence of certain ultrafilters on countable Boolean algebras and an iterated form of Hindman's Theorem, which is closely related to Milliken's Theorem. A computable restriction of Hindman's Theorem follows as a corollary.