909: Base Theory Proposals for Third Order RM/3

[Harvey Friedman]

TYPO: I wrote in https://cs.nyu.edu/pipermail/fom/2021-October/022931.html

THEOREM 2.1. RCA0[3] proves the same second order sentences as ACA0.
 RCA0[3] is finitely axiomatizable.

RCA0[3] should be ACA0[3], both places.

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] - here
4. Mathematical generation of RCA0[3] - COMBINATORIAL RM[3] - next posting

3. SOME THIRD ORDER REVERSE MATHEMATICS - RM[3]

We use RM[3] for "third order reverse mathematics".

In https://cs.nyu.edu/pipermail/fom/2021-October/022920.html there are
no interesting examples of unusual logical strengths at all. Only the
strength ATR_0 is mentioned from the Jordan decomposition theorem
(about functions of bounded variation). Not unusual for usual RM.
Presumably for continuous functions the Jordan decomposition theorem
is much weaker, like ACA_0?

NOTE: I found this: https://arxiv.org/pdf/1704.00931.pdf which treats
the continuous case.

NOTE: I have been able to see how to get ATR_0 out of Jordan
decomposition as claimed in
https://cs.nyu.edu/pipermail/fom/2021-October/022920.html It is the
same RM method of presentations - see SUP below. It seems open how to
get Pi-1-1-CA0 from Jordan decomposition.

Actually I would have superficially thought that this so called
"explosion" as Sanders is calling it, which is totally normal in
ordinary RM, would be even higher to Pi-1-1-CA0. I say this because an
even more fundamental rudimentary theorem has such an explosion to
Pi-1-1-CA0:

SUP. Every function from R into [0,1] has a supremum.

NOTE: I am not sure what "Darboux supremum theorem" is referred to in
https://cs.nyu.edu/pipermail/fom/2021-October/022920.html and may well
be SUP above.

THEOREM 3.1. ACA0[3] + SUP proves the same second order sentences as Pi-1-1-CA0.

Proof: ACA0[3] + SUP proves Pi-1-1-CA0 by using a presentation(!) of
some function from R into [0,1]. Specifically boldfaced arithmetic
presentations. This is totally normal RM fare. So every theorem of
Pi-1-1-CA0 is a theorem of ACA-[3] + SUP. Now let phi be a second
order sentence provable in ACA0[3] + SUP. We have the obvious
interpretation of ACA0[3] + SUP in Pi-1-1-CA0 that preserves second
order sentences. First and second order objects are unchanged and the
third order objects are interpreted as bold faced arithmetic
operations which is easily handled in Pi-1-1-CA0. Under this
interpretation, SUP is provable in PI-1-1-CA0. Hence the
interpretation of phi is provable in Pi-1-1-CA0. Hence phi is provable
in Pii-1-1-CA0. QED

Notice that the essence of this conservative extension result, Theorem
3.1, is just plain old ordinary RM, using presentations of third order
objects.

I expect that all of the "explosions" touted in
https://cs.nyu.edu/pipermail/fom/2021-October/022902.html behave this
way, and are not only totally compatible with usual RM, but usual RM
ideas and methods are exactly what is involved in proving the
corresponding conservation results. The exception is the ones
involving 'Suslin's functional" which obviously has no bold faced
arithmetic presentation. These results involving Suslin's functional
is totally uninteresting and irrelevant for a foundationally oriented
RM investigation of real analysis.

Of course there is a subject we can call Reverse Set Theory of a
totally different character. Going way back there is the reverse
mathematics over base theory ZF focusing on variants of the axiom of
choice.

CONJECTURE. For every one of the analysis statements in
https://cs.nyu.edu/pipermail/fom/2021-October/022902.html Theorem 3.1
holds. There is total compatibility with usual RM and the usual RM
methods are exactly what is used to prove conservation.

QUESTION 1. Does Jordan decomposition prove Pi-1-1-CA0 over ACA0[3]?
In RM, what is the status of bold faced arithmetically presented
Jordan decomposition? I see it implies ATR0 and that is implicit in
Normann/Sanders, and it is clear that it is proved in Pi-1-1-CA0. So
at present there seems to be a gap. Totally normal for RM.

QUESTION 2. What can we say about the relationship between Jordan
decomposition and SUP over ACA0[3]? Does SUP imply Jordan
decomposition over ACA0[3]?

NOTE: Just because SUP implies Pi11-CA0 and within ordinary RM
Pi11-CA0 proves presented Jordan decomposition, does NOT mean that SUp
implies Jordan decomposition over ACA[3]. THUS we are beginning to see
early indications of an interesting third order RM that isn't slavish
straightforward lifting of second order RM to third order RM.

THEOREM 3.2. There is no second order sentence which implies SUP over ACA0[3].

In connection with SUP, there is a natural second order sentence which
is behind the strength of SUP and is naturally used to establish this.
Furthermore, it is purely combinatorial.

LEFTMOST. Every tree of finite sequences from N with an infinite path
has a leftmost infinite path.

THEOREM 3.3. Leftmost is provably equivaelnt to Pi-1-1-CA0 over RCA0 in RM.

(I believe this result is due to me at the very beginning of my
discovery and dissemination of RM. Haven't looked at historical
documents lately).

The  unusual strength cited from the Suslin functional and other brute
force characteristic functionals is entirely expected and not
mathematically or foundationally interesting - in contrast to the
Jordan decomposition theorem which is mathematically interesting.
HOWEVER, because of the SRM project, I would be interested in seeing
what can be done in extremely minimalistic third order settings - or
any settings for that matter - and see section 4.

Second order RM does have logical strengths going all the way through
Z_2 and even all the way through significant initial segments of the
cumulative hierarchy well past Russell type theory and Z = Zermelo set
theory.

Most famously, there has been a lot of work recently on the reverse
mathematics of Borel Determinacy and its fragments. For bold faced
arithmetic sets this goes up through Ruseell type theory. It has been
extensively studied with much weaker fragments going through Z_2.

I gave purely descriptive set theoretic forms of BD and showed their
equivalence over appropriate base theories in RM. There are a few
forms of this. Here is one. Let K be the Cantor space of infinite
sequences from {0,1}.

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

Of course, we can adapt this to RM[3].

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

This implies usual BD over ACA0[3]. In fact, ATR0 + BD and ACA[3] +
Two Sided Uniformization prove the same second order sentences.

A possibly interesting question immediately arises: Does Two Sided
Unif imply SUP over ACA0[3]?

There is also my Borel Diagonalization and my

Unary Borel Functions and Second Order Arithmetic, Advances in Math.,
Vol. 50, No. 2, November 1983, pp. 155-159
Selection for Borel relations, in: Logic Colloquium 01, ed. J
Krajicek, Lecture Notes in Logic, volume 20, ASL, 2005, 151-169.

All of these things can be viewed with Borel replaced by arbitrary
third order, in the context of ACA0[3].

QUESTION. What are the prospects for interesting new third order
reversals where the mathematical essence is not already present in the
usual second order RM?

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

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 909th 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

Harvey Friedman