892: Remarks on Reverse Mathematics/2 / Ghost of departed quantities

[Sam Sanders]

Dear Harvey,

> In this posting I want to focus on how to handle third order objects in RM.

I am happy to hear, and will give you my honest-to-God thoughts.  For those who
want the short version:

While the Lebesgue integral and measure readily confront us with statements 
that stretch the limits of ZF(C), the same holds for the Riemann integral and 
ordinary mathematics/SOA.  

Actually, one does not need the Riemann integral: functions of bounded
variation already pose the same challenge.  And the latter are “very” close
to continuous.  

> HANDLING THIRD ORDER OBJECTS IN REVERSE MATHEMATICS
> 
> Third order objects arise in RM most commonly when dealing with F:R
> into R. More generally, R can be a Polish space.
> 
> Here are several ways to go about this.
> 
> 1. Require them to be continuous or piecewise continuous and use
> coding by neighborhood conditions. This is the standard way that third
> order objects are now dealt with in RM. Base theory RCA_0.

See previous email: even this is problematic (somewhat) in that it can
change logical strength (from ACA_0 to RCA_0). 

As an example, the Tietze extension theorem for separably closed sets 
is equivalent to ACA_0.  In [1], I show that the “actual” strength of this 
theorem is due to fact that it implies the following:

for an RM-code f, defined on a separably closed set C, there is third-order 
g: R -> R that equals f on C.  

The previous is actually equivalent to ACA_0 and the aforementioned
version of Tietze.  Note that g need not be continuous.  

Hence, in the absence of ACA_0, there are RM-codes that are not denoted by
any third-order objects!

And what are these codes for third-order objects that do not denote third-order objects?

Should we perhaps call them the ghosts of departed third-order quantities?

(I do not take credit for formulating the last sentence)

> 2. Treat them as another sort not tied to second order objects. I.e.,
> in terms of some sort of third order RM.

This is a good approach, but the second-order and third-order worlds 
are intimately connected:  if all reals are recursive (RCA_0 has such a model), 
then all R-> R functions must be continuous.  

In fact, I claim in [1] that this observation is the cause of many coding problems:

if all reals are recursive, then there can still be codes for discontinuous functions.  
By contrast, there cannot be any discontinuous functions.  In other words, third
-order and second-order objects are intimately connected, while the codes need
not be.  


> 3. Treat them as Baire class 2 functions. These are treated as
> explicitly Baire class 2 meaning that one has a double sequence of
> continuous functions given as in 1. Base theory ACA_0.
> 4. It is natural to consider Baire class n functions, n >= 1, in
> method 3. Base theory ACA_0 and ACA' for Baire class n's all at once.
> ACA' is for all n the n-th Turing jump of any set exists.
> 5. Treat them as Borel functions with the usual Borel coding scheme
> for basically Baire class alpha,  a countable ordinal. Base theory
> ATR_0.

Sure, but:  the following statement requires a lot of (convential) comprehension to prove
in that one is at the level of full SOA:

“Not all third-order functions on R are Baire 2"

Admittedly, this is based on the Baire characterisation thm rather than the definition you propose.  
The following is however equally hard to prove:

“A third-order function of bounded variation on [0,1] can be represented by an RM code for a Baire class 1 function”

where the “RM code” means a sequence of continuous functions (given by RM-codes or not).  

> IMPORTANT POINT: 3,4,5 can be presented WITHOUT using continuous
> functions. Instead one can use trivial non problematic functions with
> even rational data. So any issues with the coding of continuous
> functions and the coding of sequences of continuous functions can be
> bypassed for 3,4,5. This also suggests the use of sequences of finite
> objects to present continuous functions in 1.
> 
> I regard 2 as a problematic idea, unless one bears down and seriously
> uses the SRM perspective - see posting #891. The vast bulk of third
> order mathematical constructions are based on fundamentally sequential
> processes.

I disagree with your observation:  one can represent many third-order objects
in this way, but this requires a lot comprehension.  So the representation is fine,
unless “measuring logical complexity via comprehension” is one’s goal.   

> That does allow for discontinuous objects.

Good!  Some of my favourite objects are discontinuous...

> Baire class 2 is a tremendously large family of third order objects given by sequential
> processes.

Then show me how a function of bounded variation is represented via such a sequence. 
In case you only use (conventional) comprehension, you will have used Kleene’s \exists^3,
while no functional S_k^2 (which decides Pi_k^1-formulas) can do the job.

Thus, we are at the level of SOA.  

> 
> Now look at the following sample of third order statements through the
> lense of 1,3,4,5. This stays within the existing RM framework. Each of
> these third order statements is treated in these four ways, resulting
> in four statements. What is their reverse math?
> 
> There has been enough of an explosion of work in RM lately that
> perhaps a large amount of this has been done.
> 
> A. Every sequence from X misses an element of X. Here X is a Polish
> space (with an appropriate nontriviality condition).

I have no comments here.  

> B. No function from X into Y is injective. Here X is a nontrivial
> Polish space and Y is an appropriately countable space.

See [4] in which we study the uncountability of [0,1] based on injections.

The associated principle NIN (no injection from [0,1] to N) is hard to prove
in that Kleene’s (\exists^3) can do it, but no system based on (S_k^2) can.   

> C. No function from X into Y is bijective. Here X is a nontrivial
> Polish space and Y is an appropriately countable space, but even wider
> contexts may be very interesting.

See [4] in which we study the uncountability of [0,1] based on bijections.  

The associated principle NBI (no bijection from [0,1] to N) is hard to prove
in that Kleene’s (\exists^3) can do it, but no system based on (S_k^2) can.   

Since S_k^2 can decide Pi_k^1-formulas, we are at the level of SOA. 

> D. Every monotone function has at most countably many discontinuities.
> Here use R but maybe some other ordered spaces.

This can be done using Kleene's \exists^2, as shown in [3].

> E. Every function of bounded variation is the difference between two
> monotone functions. (Jordan decomposition thm)

In a nutshell, this thm implies NIN, hence hard to prove.  

We study this thm in [3] in recursion theory.  We mention many thms that imply NIN in [2,3,4].

> F. A function is Riemann integrable if and only if it is continuous
> almost everywhere.

In a nutshell this thm implies NIN.  Here is another simpler thm that implies NIN:

If f:[0,1] -> [0,1] is non-negative and Riemann integrable on [0,1], with integral equal to 0, 
then there is x in [0,1] with f(x)=0.  

> G. A monotone function is differentiable almost everywhere.

Should be possible using Kleene’s \exists^2.  

> H. The union of a sequence of sets of measure zero is of measure 0.

This thm implies NIN and is thus hard to prove, even if we restrict to the Jordan-Peano measure
(which is connected to the Riemann integral).

> I. Countable additivity of Lebesgue measure.

Same as H.  

> So the idea is to admit right off that there are different "brands''
> of third order functions in RM and see how standard third order
> statements fare under the various brands.These brands can be stated in
> fairly robust ways.

In conclusion, while the Lebesgue integral and measure readily confront us
with statements that stretch the limits of ZF(C), the same can be said for the
Riemann integral and ordinary mathematics/SOA.  

Best,

Sam

References

[1] Sam Sanders, Representations and the Foundations of Mathematics, to appear in NDJFL, arxiv: https://arxiv.org/abs/1910.07913

[2] Dag Normann and Sam Sanders, On robust theorems due to Bolzano, Weierstrass, and Cantor in Reverse Mathematics, Submitted, https://arxiv.org/abs/2102.04787

[3] ___, Betwixt Turing and Kleene, Submitted, arxiv: https://arxiv.org/abs/2109.01352

[4] ___, On the uncountability of R, Submitted, arxiv:  https://arxiv.org/abs/2007.07560