[FOM] response to Harvey's posting on the reverse mathematics of Hindman's Theorem

[Stephen G. Simpson]

[5] Andreas Blass, Jeffry L. Hirst, and Stephen G. Simpson, Logical
     analysis of some theorems of combinatorics and topological
     dynamics, in: [6], 1987, pp. 125-156.

[6] Stephen G. Simpson (editor), Logic and Combinatorics,
     Contemporary Mathematics, Number 65, American Mathematical
     Society, 1987, XI + 394 pages.

According to Harvey, until recently there were three proofs of
Hindman's Theorem. Actually, there were already in 1980 at least four
very different proofs:

  1. Hindman's original complicated combinatorial proof.
  2. Baumgartner's simplified combinatorial proof.
  3. Glazer's elegant proof using ultrafilters.
  4. The Furstenburg-Weiss proof using the Auslander-Ellis Theorem from
       topological dynamics.

Also contrary to what Harvey said, my coauthors and I showed in the
1980s [5] that Hindman's proof works in ACA_0^+ while Baumgartner's
works in Pi^1_2-TI_0.

We also showed [5] that Hindman's Theorem implies ACA_0, and that the
Auslander-Ellis Theorem is provable (via Hindman's Theorem) in
ACA_0^+.   The gap between ACA_0 and ACA_0^+ remains to this day as a
vexing problem in reverse mathematics.

All of this work is relevant to the larger issue of what axioms are
appropriate for mathematics.  At the time or our work in the 1980s, it
appeared that easier proofs of Hindman's Theorem required much
stronger axioms to formalize.  But now, as a result of more recent
work by Hirst and Towsner, the picture is somewhat different.  Hirst
[4] and Towsner [2] exhibited versions of the ultrafilter proof that
work in second-order arithmetic.  And Towsner [1] developed a simple
proof of Hindman's Theorem that works in ACA_0^+.

Stephen G. Simpson
Department of Mathematics
Pennsylvania State University

Research area: foundations of mathematics
Web page: http://www.math.psu.edu/simpson