Hindman's theorem: an ultrafilter argument in second order arithmetic
Henry Towsner · Journal of Symbolic Logic · 2011
Abstract Hindman's Theorem is a prototypical example of a combinatorial theorem with a proof that uses the topology of the ultrafilters. We show how the methods of this proof, including topological arguments about ultrafilters, can be translated into second order arithmetic.