[FOM]: Regarding Sander's postings

[Sam Sanders]

Dear FOM,

According to Harvey Friedman, I have made spurious claims.  Harvey’s motivation (in part) is the
INCORRECT observation that my results are due to my stepping outside of the Borel world.  

Why is Harvey’s observation INCORRECT? Because I am working with functions of bounded variation,
which we all know to be Baire class 1.  Let us examine the how and why below.  

> If you examine any of the third order statements Sander's is talking
> about which he claims to reverse to a strong system,

I make no such “reversal" claim. I do claim the following:  


There are third and fourth order conservative extensions of Z_2, called Z_2^omega and Z_2^Omega.  (note the capital)

Z_2^omega is Kohlenbach’s RCA_0^omega plus the existence of S_k^2 for any k.  The functional S_k^2 can decide Pi_k^1-formulas in Kleene normal form.

Z_2^Omega is Kohlenbach’s RCA_0^omega plus the existence of Kleene’s 3E aka \exists^3.  

It is known that Z_2^omega, Z_2^Omega, and Z_2 prove the same second-order sentences.  

And Dag and I have shown:

Z_2^omega cannot prove NIN (=there is no injection from [0,1] to N)

Z_2^Omega can prove  NIN.

Hence, it takes crazy much comprehension to prove NIN, namely at the level of Z_2. 
Admittedly, NIN is about arbitrary third-order objects.   But that is not necessary:

Indeed NIN is equivalent to NIN_BV over Kohlenbach’s RCA_0^omega (or much weaker systems), 
where NIN_BV expresses 

“There is no injection from [0,1] to Q that has bounded variation"

We note that “bounded variation” is a class very close to the continuous.  
We can replace “bounded variation” by “Borel” or “upper semi-continuous”, and probably much more.  
We can prove similar results for *bijections*.  


On a historical note, Kleene’s \exists^3 is present in Hilbert-Bernay’s Grundlagen (namely in the “main" system H from Supplement IV) .  

The functionals S_k^2 are essentially the restrictions to Pi_k^1, as defined by Sieg-Fefferman.  

Z_2 is then a further restriction, which cannot be found in the HB-Grundlagen.  

> you will find
> that the base theory being used does not constitute a legitimate base
> theory for the proper conception of reverse mathematics.

Then enlighten FOM why my base theory would be illegitimate:

As you can see, I use “vanilla” RCA_0^omega, i.e. Kohlenbach’s base theory from RM2001.

It has a weak form of primitive recursion (the R_0 recursor from Godel’s T)
and “quantifier-free axiom of choice for numbers”.  One cannot do without 
those if one wants \Delta_1^0-comprehension.  

Moreover, RCA_0^omega and RCA_0 prove the same second-order sentences.
There is even a proof translation: if RCA_0^omega proves A, then RCA_0 proves [A]_ECF, 
where the ECF-translation replaces all third-order and higher objects by… RM-codes.

This is of course based on Kleene’s second model, the canonical model of type theory, 
as I am told.  So what is problematic about these things.  
> 
> 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".

So B is RCA_0^omega with all the connections to RCA_0 noted above.  

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

And how is RCA_0^omega deficient in that department, any more than RCA_0 ?

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

again: Explain!  

> I am not aware of any errors in any claims I made in those postings
> Sanders is referring to.

I did not claim any errors.  

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

Once more with feeling:  NIN is hard to prove as noted above. 
NIN is implied by 

“There is a function not in Baire class 2”.  

Hence, the “coded" world you wish to study is consistent with 

“All functions are Baire class 2"


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

Luckily I do not step outside of the Borel world: I stay firmly within Baire
class 1 with my functions of bounded variation.  

Best,

Sam