907: Base Theory Proposals for Third Order RM/1

[Harvey Friedman]

Practically any system that is reasonably natural, T, is fair game in
the sense that one can propose to do Reverse Math over T. For example,
there is reverse math over ZF. This is a lot older than the standard
RM.

RCA0 serves a clear foundational purpose with the standard RM and
there is the issue however of weakening RCA0 in order to accommodate
considerably more foundational phenomena. A large amount of
mathematics is already provable in RCA0 and so is not treated in RM
(except perhaps proving it in RCA0), and thus the foundational purpose
of using weaker base theories than RCA0. This is connected with the
SRM = strict reverse mathematics initiative.

On the other hand there is quite a lot of mathematics that is stated
in third order terms, most notably continuous or partial continuous
functions or "essentially" partially continuous functions on Polish
spaces. A broader class is the partial arithmetic functions on Polish
spaces. This is an arguably considerably more robust class than the
"essentially" partially continuous functions on Polish spaces.

At present there are no systems for third order mathematics without
presentations - unrestricted third order mathematics - that have been
accepted as appropriate the way RCA0 has been for second order
mathematics and for at least one good version of partial continuous
functions on Polish spaces.

There are some good reasons for this lack of appropriate third order
base theories. For when one thinks of appropriate third order base
theories, one has a natural model or models in mind for the third
order objects that are basic enough to be regarded as essential like
RCA0. And these models are so clear that they immediately suggest that
one might as well simply use presentations instead of introducing a
third order sort.

In fact the reason that RM comfortably stays second order since I
introduced it over 50 years ago is that it can't be first order
because using presentations there is not workable for enough
mathematics, and because using presentations at level three is
actually quite workable.I have even proposed branches of RM staying
second order like "recursively presented RM" or "arithmetically
presented RM" or "Baire class alpha presented RM" or "Borel presented
RM" and so forth.

The main reason I have an interest in third order base theories for RM
is because of the SRM = strict reverse mathematics initiative, which
is to, paradoxically, strive to eliminate base theories altogether!
But the point is to take mathematics as it is presented, and of course
mathematicians talk about continuous functions from R into R all the
time with talking about presentations, although often they find
presents highly relevant especially when considering computational
aspects. Increasingly mathematics is moving towards the computational
in large part because of how much more powerful the computational has
become.

The point of this posting is to explore some possibilities for
extended base theories that may at least fill some of the role for
unrestricted third order mathematics that RCA0 does.

Here we discuss a particular proposed base theory for third order RM.
It is particularly clean but it does push us up from RCA0 to ACA0.
Foundationally significant base theories at the level of RCA0 that are
third order are much more delicate because one needs to manipulate
third order maps whose domain is not necessarily a nice space like
N^N, and the way that continuity is actually used in a lot of analysis
where one has "essentially" continuous - with singularities - needs
some careful investigation.

PROPOSAL ACA0[3]. This should be a conservative extension of ACA0. In
addition to the usual sorts N,POW(N), the third sort is for partial
functions from POW(N) into POW(N). We have the expected axioms for
defining subsets of N and partial functions from POW(N) into POW(N) by
relative arithmeticity, and induction takes the form of induction for
subsets of N.

In this first posting, I omit all of the details for ACA0[3] - partly
because of awaiting some feedback for the suitability and interest of
ACA0[3] as a base theory. SInce the intended model is the rather
robust full POW(N) with the partial functions from POW(N) into POW(N)
that are arithmetic with parameters from POW(N), it seems like there
is really only one decent full blown formalization of ACA0[3], as
conservative over ACA0.

So can we get strength out of simple third order mathematical
statements over ACA[3]? Certainly. Here is perhaps the most basic.

THEOREM A. Every bounded function from R into R has a least upper bound.

What about A + ACA0[3]? This proves Pi-1-1-CA0.

Now we don't get equivalence with Pi-1-CA0. Just equal logical
strength, or mutual interpretability. However, if we use arithmetic
presentations, then without parameters we get equivalence with
parameterless Pi-1-1-CA0. If we use arithmetic presentations with
second order parameters, we get equivalence with Pi-1-1-CA0.

Here is my conclusion.

I AM PREPARED TO BELIEVE THAT RM over base theory ACA[3] could be a
good idea for third order RM, despite that it lives >= ACA_0, cutting
out considerable phenomena.

QUEStiON 1. What can we say about various third order statements in
mathematics when added to ACA0[3] in terms of
i. Their second order consequences.
ii. Their logical strengths.
iii. Their mutual derivability between each other?

QUESTiON 2. What is the relationship between this reverse math over
ACA0[3] and the corresponding ordinary reverse math using arithmetic
type presentations?

QUESTION 3. How should we weaken ACA0[3] to a conservative extension
of RCA0 in such a way as to allow very basic manipulations of
"essentially" partial continuous functions that actually arise with
real frequency in analysis?

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

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

Harvey Friedman