897: Remarks on Reverse Mathematics/4

[Sam Sanders]

Dear FOM, 

First a BLANKET CAVEAT: we work over Ulrich Kohlenbach’s base theory RCA_0^omega, i.e. in higher-order RM from the book RM2001.  
Anyone disagreeing with that framework should FIRST point out which axioms of RCA_0^omega are problematic and why.  The system RCA_0^omega
has only got the weakest form of primitive recursion and a weak choice principle needed to guarantee that RM-codes denote 3rd order objects.  

Secondly, Harvey Friedman asked the following question:

> ARE THERE ANY ORDINARY MATHEMATICAL THEOREMS INVOLVING THIRD ORDER
> OBJECTS WITHOUT PRESENTATIONS THAT HAVE ANY INHERENT LOGICAL STRENGTH?

The following third-order statements are *hard* to prove in terms of (conventional) comprehension in that full SOA becomes necessary (full technicals details in a PPS below). 

For conceptual reasons (see PS below), the theorems 1)-6) cannot imply more second-order sentences than say ACA_0 *in isolation*.  However, combining 1) with the existence of a discontinuous function on R (or N^N or 2^N), yields ATR_0, over RCA_0^omega.  Similar ‘explosions’ are listed below.  

0) Darboux’s supremum theorem for any [0,1]-> [0,1] function (1875)

1) Jordan decomposition theorem (1881): a function of bounded variation is the difference of two monotone functions.  

2) A function that is discontinuous everywhere, is not Riemann integrable (1870, Hankel).  

3) Liouville’s uniqueness theorem (1839) for Abel’s integral equation for continuously-differentiable functions and Riemann integrals  

4) Fundamental theorem of calculus: for Riemann integrable functions, integration followed by differentiation cancels out in at least one point in [0,1]. (Darboux, 1875).

5) Many other thms about Riemann integrable, Baire classe 1, semi-continuity, or functions of bounded variation.  

6) The Lindeloef Lemma (1903)


Note that 2) is proved by Hankel immediately after “a continuous function on [0,1] is Riemann integrable”, known from the second-order RM of WKL_0.    
We also note that Euler has mentioned discontinuous functions as early as 1767 (see previous FOM email), while Hilbert-Bernays define many discontinuous
functions in the “Grundlagen”, including Feferman’s mu operator.  Finally,  many equivalences (over RCA_0^omega) exist for theorem 0).  


Thirdly, here are some other ‘explosions', all working over RCA_0^omega.  We note that RCA_0^omega plus “there is a discontinuous function on R” is conservative over ACA_0.  

a) The combination of a discontinuous function on R and the Lindeloef lemma implies Pi_1_^1_CA_0.  

b) The combination of a discontinuous function on R and Darboux’s supremum theorem for any [0,1]-> [0,1] function (1875), implies Pi_1_^1_CA_0.  

c) The combination of a discontinuous function on R and the Jordan decomposition theorem yields ATR_0.  

d) The combination of the Suslin functional and the Jordan decomposition theorem yields Pi_2^1-CA_0.

Regarding d), RCA_0^omega plus the existence of the Suslin functional yields a Pi_3^1-conservative extension of Pi_1^1-CA_0.  

> The examples given thus far attain logical strength only in the
> presence of statements about objects that lie way outside of
> mathematical practice.
> 
> This is in sharp contrast with the situation
> with ordinary RM. 

I tend to disagree, as everything is proved in Kohlenbach’s base theory/higherorder RM, 
which is conservative over RCA_0.  

Which axiom of Kohlenbach’s base theory is problematic (see above caveat)?  See also PS below: theorems 0-6 
are consistent “all functions on R are continuous”, which would seem to go against “thms 0-6 are set theory”.  

Best,

Sam

PS: The theorems 0-6 above do not imply the existence of a discontinuous function on R.  In fact, they are consistent with Brouwer’s thm “all functions on R are continuous”, i.e.
0-6 hold in (or are consistent with) the canonical model of type theory.  For these reasons, the theorems 0-6 can prove at most ACA_0 in terms of second-order sentences.  
However, there is “hidden strength” in 0-6 as shown by the above ‘explosions’.

PPS: As noted in a previous email, one can define the systems Z_2^omega and Z_2^Omega (note the capital) as follows:

Z_2^omega is RCA_0^omega plus third-order functionals S_k^2 deciding Pi_k^1-formulas (in Kleene normal form).  

Z_2^Omega is RCA_0^Omega plus Kleene’s fourth order \exists^3 aka 3E.  

These are BOTH conservative over Z_2 for second-order sentences. HOWEVER  Z_2^omega cannot prove 0-6, while Z_2^Omega can prove all of 0-6.  

This is how “full SOA becomes necessary”. We note that Kleene’s \exists^3 is essentially Hilbert and Bernay’s “nu functional” from the Grundlagen.