Regarding Sander's postings

[Harvey Friedman]

If you examine any of the third order statements Sander's is talking
about which he claims to reverse to a strong system, you will find
that the base theory being used does not constitute a legitimate base
theory for the proper conception of reverse mathematics. That is why I
emphasize the use of SRM (strict reverse mathematics) as the proper
tool for ruling out spurious phenomena not in the spirit of RM that
Sander's is so focused on.

If one designates a base theory B and one is really using only that
base theory, then I have no objection calling what Sander's is doing
"Reverse Math over B". One can also do "Reverse Math over ZF". And in
fact that was being don a long time ago particularly in connection
with equivalents of AxC and various fragments of AxC.

The kind of base theory of third order and higher mathematics is much
too heavy to properly represent any kind of essential mathematical
practice,. Of course, the gap between base theories and actual
mathematical practice is already present in ordinary RM. However, in
ordinary RM this gap isn't so serious (for a number of reasons) and
actually can be fixed by what we already know and are developing in
SRM. It is already clear that this can be fixed through things like
the formal derivation of bounded induction from actual mathematical
statements of the most essential kind.

As I have emphasized, there is a major project which is to construct a
finite set of actual mathematical statements which, without a base
theory, have substantial logical strength. And then to subject this to
serious examination.This is already quite tricky for finite
mathematics but well under way, expected to go very well and with
great depth for countable mathematics, and much more involved for
uncountable mathematics, ranging from continuous to Baire classes to
Borel, and not even begun at all for general sets and functions on
Polish spaces. However one must keep in mind the marginal character of
such general kinds of mathematics, used primarily for organizational
and teaching purposes.

I think that if you can make a reasonable attempt to do this, you will
most likely be doing something like "reverse set theory" or "reverse
general topology". It still might be interesting to do this, but it is
widely known that set theory and general topology are, as
***mathematics*** considered marginal subjects that are used as an aid
in the organization of more  erious mathematical areas.

I am not aware of any errors in any claims I made in those postings
Sanders is referring to. For example, regarding NIN. For Borel
presented functions this is provable in ATR0. For Baire class 2
presented functions this is interesting RM of the standard kind, which
I won't go into here. I haven't had the time to look further. This is
standard interesting fare in RM.

SUMMARY. As a rule of thumb, once one goes outside Borel presented
functions, one is into the kind of third order RM for which there is
no appropriate base theory proposed examined and fleshed out, and the
SRM discipline has yet to apply. Without a proper base theory any
claim of high logical strength is spurious.

Harvey Friedman