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

[Harvey Friedman]

Steve, thanks very much for this additional information in this very
interesting corner of Reverse Mathematics.

On Mon, Aug 31, 2015 at 10:55 AM, Stephen G. Simpson <sgslogic at gmail.com> wrote:
> [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.

I said "before Towsner" and was quoting Towsner's 2009 article
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=806B28AAEDE5611117BEF5DE7B25D899?doi=10.1.1.249.1174&rep=rep1&type=pdf

"There are three standard proofs of Hindman’s theorem: Hindman’s
original com- binatorial argument [4], Baumgartner’s streamlined
combinatorial argument [1], and the Galvin-Glazer proof using
ultrafilters (see [3] or [6])."

Then I went on to misquote Towsner about Baumgartner's proof. I guess
I was in my haste misled by  the phrase "Baumgartner's streamlined
combinatorial argument". Thanks for the correction!

> 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.

See my apologies above "Then I went on to misquote ..."

> 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.

Yes, that was clear to me from reading Towsner and other sources. Do
you believe that Hindman's Theorem is provable in ACA_0?
>
> 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^+.

Doesn't Towsner adapt the ultrafilter proof more or less in tact more
or less lower than even Pi11-CA0? What do you think about the
possibility of preserving the ultrafilter proof more or less in tact
working in ACA_0+?
>
There are a number of weakenings and strenghenings of Hindman's
theorem, I think some of them have names like Milliken attached to
them, and I was wondering what the current RM status of them are as
well. Could you help us with this? What is the state of the art?

1. Every finite coloring of N has an infinite S whose <= n sums have
the same color. Here n is a variable.
2. Every finite coloring of N has an infinite S whose <= n sums have
the same color. Here n is a standard integer (scheme).
3. Every finite coloring of N has an infinite S whose n sums have the
same color. Here n is a variable. This is a consequence of Ramsey's
Theorem.
4. Every finite coloring of N has an infinite S whose n sums have the
same color. Here n is a standard integer (scheme). This is a
consequence of Ramsey's Theorem.
5. The obvious Pi02 form of 1.
6. The obvious Pi02 form of 2.
7. The obvious Pi02 form of 3.
8. The obvious Pi02 form of 4.
9. Iterated forms of 1-4. Maybe iterated forms of 5-8??
10. Schusr's Theorem. Every finite coloring of N has an x,y,x+y with
the same color.

Harvey Friedman