910: Base Theory Proposals for Third Order RM/4

[Harvey Friedman]

1. Third Order RM Compliments RM - no radical foundational advance or
upheaval - #2
2. ACA0[3] at level of ACA - experimental - #2
3. Some Third Order Reverse Math - RM[3] - #3
4. Claims of High Logical Strength - here
5. Mathematical generation of RCA0[3] - COMBINATORIAL RM[3] - next posting

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. Here I will focus on the dubious claims of logical strength.
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. 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. I doubt whether there is
any appropriate base theory used at all for this.

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.

ACA0[3] is a good base theory for revealing high logical strength when
there really is legitimately high logical strength. As I mentioned
earlier

TWO SIDED UNIFORMIZATION. Every symmetric subset of K x K contains or
is disjoint from a continuous function from K into K.

has over ACA0[3] logical strength roughly Zermelo set theory with its
infinitely many iterations of the power set axiom.

I want to close with a discussion of the relationship between ACA0 and
ACA0[3] and bold faced arithmetic presented forms of third order
sentences. Let phi be a third order sentence (in the language of
ACA0[3]). We write #(phi) for the result of interpreting the third
order partial functions in phi as bold faced arithmetic functions.
Looking at this carefully,  a bold faced arithmetic presentation needs
some explanation for careful proof theoretic analysis here. A bold
faced arithmetic presentation of partial f:POW(N) into POW(N) is a 2nd
order parameter together with a natural number k giving the level of
arithmetic. Then we evaluate f based on the k-th Turing jump of the
argument and the parameter. We may get more undefinedness for f this
way than we really should unless we are in the stronger system ACA'
which uses "for all x,n, the n-th Turing Jump of x exists" as an
axiom. But we can still stay in ACA0 with the following trick. In
ACA0, by a bold faced arithmetic presentation we mean a 2nd order
parameter together with a natural number k given the level of
arithmeticity WHERE for all x, the k-th Turing jump of x exists. Since
ACA0 has no trouble proving that such numbers k are closed  under
successor, we then really do  have an interpretation of ACA0[3] in
ACA0 this way. So this proves

THEOREM 2. ACA0[3] and ACA0 prove the same second order sentences and
are mutually interpretable. Let phi be a third order sentence. ACA0[3]
+ phi and ACA0 + #(phi) prove the same second order sentences and are
mutually interpretable.

##########################################

My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 910th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-899 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1
908: Base Theory Proposals for Third Order RM/2
909: Base Theory Proposals for Third Order RM/3