908: Base Theory Proposals for Third Order RM/2

[Sam Sanders]

Dear FOM,

Harvey Friedman wrote the following:

> 1. THIRD ORDER RM COMPLIMENTS RM - NO RADICAL FOUNDATIONAL ADVANCE OR UPHEAVAL
> 
> I expect properly done foundational third order RM to be an
> interesting compliment to existing RM and very closely tied to it.

I agree.  In case of Kohlenbach’s higher-order RM, there is even a technical device 
that reflects this observation:  

Troelstra's ECF translation, which replaces third-order and higher objects by… RM-codes.  

We have the following result:

In case RCA_0^omega proves the sentence A, then (second-order) RCA_0 proves [A]_ECF. 

(details can be found in Kohlenbach’s “higher-order RM”, in RM20010).

So any result in Kohlenbach’s HRM can be “pushed down” to second-order RM by ECF.  


> The
> logical strengths arising out of third order RM, when done with base
> theories properly reflecting the practice of the abstract parts of
> mathematical analysis are expected to be normal, and correspond to
> what is obtained in RM using appropriately presented third order
> objects (presentations being first or second order as usual). This is
> what I see in Sander's
> https://cs.nyu.edu/pipermail/fom/2021-October/022902.html

I will provide an example, involving the ECF translation:  

One can prove that Dini’s theorem for nets is equivalent to the Heine-Borel theorem for uncountable coverings.  

Apply ECF, and out rolls the well-known equivalence between (original) Dini’s theorem for sequences and Heine-Borel for countable coverings.  

> An interesting addition to the RM enterprise, but not in any way any
> kind of radical foundational advance or radical foundational upheaval

Harvey, you are right (even more than you know: see below).  

> as is suggested by writings and voice recordings by some.


But sometimes you have to make some noise to get people to listen.  
You of all people would understand.  So after my noise, please listen:

> I can imagine a rich range of some relative provability and relative
> unprovability results between interesting third order mathematical
> statements over appropriate third order base theories,] that are not
> simply routine versions of what we normally do in RM with lightfaced
> and boldfaced arithmetic presentations.

Now that I have your attention, here is the state-of-the art:  

in second-order arithmetic/RM, one measures strength based on (second-order) comprehension axioms, or statements
implied by the latter.  There is really only ONE scale.  

in third-order arithmetic, one needs TWO independent scales:

1) comprehension functionals (2E, S_k^2, …), which are third-order functionals deciding the truth of certain formula classes (not allowing third-order parameters and beyond)

2) fragments of the “neighbourhood function principle”, a version of AC involving continuous choice functions (and allowing for third-order parameters).  

Note that Kleene’s 3E, which implies full Z_2, proves both 1) and 2) when the latter is restricted to quantifiers over Baire space.  


As a basic example, we have seen that NIN (there is no injection from R to N) is not provable from 1).  

I have dramatised this by saying “NIN is hard to prove (in terms of conventional comprehension”.  This remains
true, but we also have the following: 

Very weak fragments of 2) readily prove NIN (say at the level of WKL_0).  


So here is the deal: if we accept 2) as a reasonable scale, different and independent from conventional comprehension, 
then NIN becomes weak again.  

> In particular, I still have not seen any *interesting* reversal
> phenomena that one obtains by using unrestricted third order that
> isn't closely tied to an ordinary second order RM reversal phenomena
> that differs only by using first or second order presentations of the
> third order objects in question. When one does such *interesting*
> reversals of a third order statement, one builds a second order (or
> first order) presentation of a third order object and then does
> regular RM to the result.


> Of course, this presentation procedure will not work if the third
> order statement gains its strength from third order objects with no
> reasonable second order presentation. However, then the reversal
> concerns statements which gain their power from third order objects
> outside the normal realm of objects of mathematical interest, e.g.,
> outside Borel measurable third order objects. This is associated with
> the reversal being mundane and uninteresting (as far as mathematical
> analysis is concerned) such as reversing the mere existence of
> characteristic functionals for second or third order quantification.
> 
> This pattern I just outlined appears to reflect exactly what is going
> on in the results stated in
> https://cs.nyu.edu/pipermail/fom/2021-October/022902.html by Sanders.

Here we disagree however:

over weak systems, presumably your ACA0[3], one proves that NIN is equivalent to 

"there is no Borel function from R to Q that is an injection”

Here, a “Borel function” is just a function that is Borel (via the usual definition).

Sure, the function does not have a presentation, but that is the point of studying third-order arithmetic. 


> Nevertheless, I would like to see interesting implications and non
> implications between third order statements arising in mathematical
> analysis, and also like in usual RM, information arising from the
> passage of one third order object to another. Probably the real
> interest in third order RM is going to be more along those lines,
> rather than anything new about logical strengths not fully reflected
> with the usual first and second order presentations in ordinary RM. .
> 
> 2. ACA0[3] AT LEVEL OF ACA0 - experimental
> 
> I am beginning to think of ACA0[3] as a credible and clarifying base
> theory for third order RM. Not necessarily the best idea, that remains
> to be seen. But a good idea. I think of ACA0[3] as a kind of robust
> setup that may readily lend itself to robust investigations into
> relative provability of third order statements from abstract analysis.
> And obviously for non relative provability, ACA[3] being a bit strong
> and robust is an advanage.

So having exists^2 (aka Kleene’s 2E, aka a discontinuous function)
in the base theory does make things much easier.  

> 
> So accordingly I give a careful axiomatization of ACA0[3]. Obviously
> there is something lost by living on top of ACA0, while it is not yet
> clear what a base theory at say the level of RCA0 should be in detail.
> But at least there is a well defined project of looking at just how
> minimalistic we can be for a third order base theory so that we
> actually DERIVE ACA0[3] from the most basic mathematical statements we
> can find. And where the boundaries are. This is the point of section 4
> in the next posting. And this kind of study discussed in 3 is highly
> relevant to the SRM enterprise.
> 
> The kind of mathematics being targeted by third order RM can be
> roughly described as in these categories from the AMS Classification:
> 
> Measure and Integration, Abstract harmonic analysis, Integral
> transforms, operational calculus, Functional analysis.

Note that my results apply to e.g. Riemann integrable functions, 
which are arguably more basic than e.g. the Lebesgue integral.  

> 
> Many of the topics in analysis in that classification scheme are close
> enough to computation and continuity, or "essential" continuity, that
> third order RM would not be logically relevant, with mathematicians
> welcoming the usual RM presentations or already using it themselves.

See my response to 907: while approximation results exist for functions
of bounded variation, these only apply to points of continuity.  

> Things like elaborations on moduli of continuity. That is a main
> reason why current RM has not felt compelled to even bring in third
> order objects - because presentations are so natural and friendly in
> many contexts..

I agree with “because…”, but that is not the whole story:  over they years, people
have honed their techniques on recursion theory/Turing machines.

The third-order approach seems to require techniques from higher-order
computability theory (I have previously mentioned Gandy selection) and
this is a whole different beast.  

People stick with what they know.  This is also part of the story.  

> The standard interpretation of ACA0[3] sets the partial functions from
> POW(N) into POW(N) to be the arithmetic ones with parameters from
> POW(N), which from the descriptive set theory point of view, are just
> the partial functions from POW(N) into POW(N) of Baire class < omega,
> with domain a set of Baire class < omega. These partial functions are
> closed under composition, a very nice thing to have.
> 
> ACA0[3] appears to be READY MADE for formalization of order 3
> mathematics, with only rather innocent coding apparatus needed. 

So based on your posting 907, I take it that ACA0[3] proves the 
existence of a discontinuous function (say on 2^N).  This would have
to be, otherwise Theorem A from 907 would not yield Pi11CA0.

Best,

Sam