[FOM] concerning reverse mathematics

[Harvey Friedman]

Sam Sanders quoting Simpson's book:

"For a theorem T of ordinary mathematics, we have the following with
few exceptions:
Either T is provable in RCA_0 or RCA_0 proves that T is equivalent to
another one
of the big five systems."

There is at least one major category of statements that do not fit in.
These are wqo statements, which are Pi-1-1. E.g., Kruskal's Theorem,
graph minor theorem, Hilbert's basis theorem (appropriately
formalized), etcetera. These are equivalent over RCA_0 to the well
orderedness of familiar ordinal notations (in the case of GMT, the
exact ordinal has not been determined, but has been determined for the
important restriction to graphs of finite tree width). Furthermore,
adjustments of natural numerical parameters give RCA_0 inequivalent
versions, corresponding to different ordinal notations.

When I set up RM, I presented these five systems, but also some others
in light of the approach to real analysis I was looking at at the
time. These include principles of what is called hyperarithmetic
analysis. According to my memory, In recent years, these too have come
up in RM investigations by Neeman and Montalban.

RM is nowhere near complete, and a great amount of very interesting
things awaits us here. One small corner: countable group theory.

But the long range (philosophical, foundational) future of RM is in
SRM = strict reverse mathematics, where there is no base theory. This
should provide major insights into the vast amount of mathematics that
is provable in RCA_0. I have one paper on this, in LC06, and another
planned.

As far as the quoted statement is concerned, one can do some rigorous
investigations of a statistical kind. We can go through some major
journals of mathematics and classify claims according to

1. Not readily formalizable in the language of RM. Otherwise:
2. Provable in RCA_0.
3. Provable in WKL_0, but not in RCA_0.
4. Provable in ACA_0., but not in WKL_0.
5 Provable in ATR_0, but not in ACA_0.
6. Provable in Pi-1-1-CA_0., but not in ATR_0.
7. Provably equivalent to WKL_0.
8. Provably equivalent to ACA_0.
9. Provably equivalent to ATR_0.

Harvey Friedman