907: Base Theory Proposals for Third Order RM/1

[Sam Sanders]

Dear FOM,

Harvey Friedman wrote the following:

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

I completely agree that large parts of mathematical analysis are truly
third-order in nature (and should be studied as such).  

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

So Ulrich Kohlenbach has an interesting approach in his book 
(applied proof theory) via the “tilde function”.  The latter is
primitive recursive (of low complexity) and reduces e.g.
quantifying over [0,1] or R to quantifying over Baire space.  

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

Note that e.g. Ulrich Kohlenbach’s RCA_0^omega has a very natural 
canonical model, as does type theory: Kleene’s second model, also
called the “ECF model” by Troelstra, I believe.  

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

This depends on your definition of “workable”.  While I agree coding
works for e.g. continuous functions, it is already far removed from the
“epsilon-delta” definition… at least upon first inspection.    

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

I do share this desire:  the current approach (using RCA_0^omega) 
has some oddities, though perhaps these can be eliminated.  

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

I both agree and disagree here:  let us take functions of bounded variation (BV for short)
as example.  As it happens, I have recently trawled the literature of approximating
BV functions.  There exist very explicit/elementary formulas for approximating BV-functions

*at any point of continuity of a given BV function*.

So nothing is said about what happens at points of discontinuity, and the latter seems 
to be the bread and butter, if not the very point, of third-order arithmetic.  

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

I agree.  

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

So I take it that one can define a discontinuous function from e.g. 2^N to N in your system?

Then Kleene’s 2E (aka \exists^2) would suffice.  The system you are talking about
sounds like RCA_0^3 (RCA_0^omega restricted to third-order) plus 2E.  

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

As I have mentioned before, A was first proved (for functions from intervals to intervals) by Darboux in 1875 (see [1]).  

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

Indeed, the proof is probably similar to the proof Dag Normann and I have (published).  

> Now we don't get equivalence with Pi-1-CA0. 

That would be impossible: no second-order sentence (provable in Z_2) proves Theorem A.  

Working over say RCA_0^3, one can however get interesting equivalences for A based on the following:

1) A version of Feferman’s projection axiom Proj1 from [2], called “BOOT” in [3].

2) Convergence theorems for montone nets in [0,1] or 2^N.

3)….

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

Here is a cheap trick to get the overall strength of the base theory down:  since we work 
over classical logic, we may at all times invoke the statement

“there is a discontinuous functions on R”

OR

“all functions on R are continuous”

In the first case, one has access to Kleene’s 2E and presumably ACA_0[3], making 
the proof relatively easy.  

In the second case, all function on R are continuous, and one can use (essentially)
the usual second-order proof.  

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

In the case of RCA_0^omega + 2E, there exists a proof translation due to Kreuzer (see [4]).  
That RCA_0^omega + 2E is conservative over ACA_0 was also (first?) proved by Hunter (see [5]).

I would think that your system ACA0[3] is similarly conservative over ACA_0.  

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

See the above trick (perhaps).

Best,

Sam

PS: Here are the references

[1] G. Darboux, Memoire sur les fonctions discontinues, Annales scientifiques de l’E ́cole Normale Sup ́erieure 2e s ́erie, 4 (1875), 57–112.


[2] S. Feferman, How a Little Bit goes a Long Way: Predicative Foundations of Analysis, 2013, 

unpublished notes from 1977-1981 with updated introduction, https://math.stanford.edu/ ~feferman/papers/pfa(1).pdf.


[3] S. Sanders, Plato and the foundations of mathematics, Submitted, arxiv: https://arxiv.org/ abs/1908.05676 (2019), pp. 40.


[4] A. Kreuzer,  Measure theory and higher order arithmetic, Proc. Amer. Math. Soc. 143 (2015), no. 12, 5411–5425.

[5] J.  Hunter, Higher-order reverse topology, ProQuest LLC, Ann Arbor, MI, 2008. Thesis (Ph.D.)–The University of Wisconsin - Madison.