Hindman's Theorem: An Ultrafilter Argument in Second Order Arithmetic

TL;DR

This paper translates the ultrafilter-based proof of Hindman's Theorem into the framework of second order arithmetic, bridging combinatorial topology and formal arithmetic systems.

Contribution

It introduces a novel method to formalize ultrafilter arguments within second order arithmetic, expanding the proof-theoretic analysis of Hindman's Theorem.

Findings

Ultrafilter methods can be formalized in second order arithmetic.

The translation preserves the combinatorial essence of Hindman's Theorem.

This approach enhances understanding of the theorem's proof-theoretic strength.

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.