Assuming 𝖢𝖧, Hindman [ht1] 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.
@article{1080938825,
author = {Hirst, Jeffry L.},
title = {Hindman's theorem, ultrafilters, and reverse mathematics},
journal = {J. Symbolic Logic},
volume = {69},
number = {1},
year = {2004},
pages = { 65-72},
language = {en},
url = {http://dml.mathdoc.fr/item/1080938825}
}
Hirst, Jeffry L. Hindman’s theorem, ultrafilters, and reverse mathematics. J. Symbolic Logic, Tome 69 (2004) no. 1, pp. 65-72. http://gdmltest.u-ga.fr/item/1080938825/