910: Base Theory Proposals for Third Order RM/4

[Sam Sanders]

Dear FOM,

Harvey Friedman wrote the following:

> We have postponed topic 5, which was numbered topic 4 previously, as
> we have come across https://arxiv.org/pdf/1711.08939.pdf Here are
> dubious claims of logical strength as well as claims of radical
> foundational advances and upheaval.

That is a strong claim, Harvey.  

I would say Dag and I did play the drama card a little bit, and we would write that paper differently now. 

In particularly, we now understand what is going on (see my answer to your 908, involving the two scales).  

Note that the AMS and JML reviewer of that paper saw nothing wrong with our claims however...

> Here I will focus on the dubious claims of logical strength.

As I have mentioned before, we do not claim any logical strength here: 

we even state this in our paper, namely that e.g. Cousin’s lemma when added to RCA_0^omega yields a conservative extension of WKL_0.    

we DO claim that the items (i) - (ix) are hard to prove in terms of conventional comprehension, similar to your Theorem 3.1 from 909:

no third-order functional S_k^2 (which can decide Pi_k^1-formulas) can prove (i) - (ix).

The same holds for the combination of all S_k^2, which we call Z_2^omega.  

However, we now know there is an alternative scale (based on the neighbourhood function principle) that has weak fragments 
that do prove e.g. Cousin’s lemma.  

(there are even nice equivalences here)

> They list nine theorem (groups):
> 
> (i)  Cousin lemma: any open cover of [0, 1] has a finite sub-cover ([15]).
> (ii)  Lindel ̈of lemma: any open cover of R has a countable sub-cover ([50]).
> (iii)  Besicovitsch and Vitali covering lemmas as in e.g. [1, §2].
> (iv)  Basic properties of the gauge integral ([6]), like uniqueness,
> Hake’s theorem,
> and extension of the Riemann integral.
> (v)  Neighbourhood Function Principle NFP ([96, p. 215]).
> (vi)  The existence of Lebesgue numbers for any open cover ([32]).
> (vii)  The Banach-Alaoglu theorem for any open cover ([91, X.2.4],
> [11, p. 140]).
> (viii)  The Heine-Young and Lusin-Young theorems, the tile theorem [38, 104],
> and the latter’s generalisation due to Rademacher ([74, p. 190]).
> (ix)  The Bolzano-Weierstrass, Dini, and Arzela` theorems for nets ([43, 58]).
> 
> And claim high logical strength for these, beyond Z_2.

No, we claim that these are hard to prove, see above.  

> You have to
> wade thru an enormous amount of material before you even get to what
> base theory is being used to interpret Z_2.

We work in Kohlenbach’s higher-order RM, as clearly stated.  

> I doubt whether there is
> any appropriate base theory used at all for this.

So RCA_0^omega works well for us.  

> I looked at Cousin Lemma, Lindelof Lemma and Vitali covering Lemma.
> For bold faced arithmetic presentations it is obvious how to prove all
> of these using Pi11-CA0, and this works even for Borel presentations.
> It then follows that
> 
> THEOREM 1. ACA0]3] + covering (all three) is interpretable in Pi11-CA0.
> 
> Thus no unusual logical strength appears to be inherent in these
> covering Lemmas. An interesting question seems to be to calculate the
> logical strength of ACA0[3] + covering (all three). We just have this
> upper bound of Pi11-CA0.
> 
> It would be helpful to see a good clean clear description of all of
> the axioms in some reasonable base theory whereby these covering
> Lemmas achieve unusual logical strength.

So take Kohlenbach’s RCA_0^omega and throw away all the fourth order stuff (which is minimal anyway).

Call this RCA_0^3.  This system’s only third-order “sins” are: primitive recursion (no more than RCA_0 can prove) and extensionaly for third-order functionals.

Call “ACA_0^3” the system RCA_0^3 plus the existence of a discontinuous function.  ACA_0^3 a conservative extension of ACA_0.

Note that ACA_0^3 plus “the Lindeloef lemma for Baire space” proves Pi11-CA_0.  

Best,

Sam