909: Base Theory Proposals for Third Order RM/3

[Sam Sanders]

Dear FOM, 

> We use RM[3] for "third order reverse mathematics".
> 
> In https://cs.nyu.edu/pipermail/fom/2021-October/022920.html there are
> no interesting examples of unusual logical strengths at all. Only the
> strength ATR_0 is mentioned from the Jordan decomposition theorem
> (about functions of bounded variation). Not unusual for usual RM.
> Presumably for continuous functions the Jordan decomposition theorem
> is much weaker, like ACA_0?

I have previously mentioned that the Jordan decomposition theorem
yields Pi_2^1-CA_0 when combined with RCA_0^omega + (S_2^2)

The system RCA_0^omega + (S_2^2) is a Pi_3^1-conservative extension
of Pi11-CA_0.    The functional S_2^2 is called the “Suslin functional”.

In the context of ordinal analysis, people talk about “abys” and “chasm”
and “dwarfing” when comparing Pi11 and Pi12 comprehension.  

The point is also that the combination of these systems becomes
much stronger than the individual constituents (for drama, we called
this “explosions").  

> NOTE: I found this: https://arxiv.org/pdf/1704.00931.pdf which treats
> the continuous case.
> 
> NOTE: I have been able to see how to get ATR_0 out of Jordan
> decomposition as claimed in
> https://cs.nyu.edu/pipermail/fom/2021-October/022920.html It is the
> same RM method of presentations - see SUP below. It seems open how to
> get Pi-1-1-CA0 from Jordan decomposition.

I do not think that is possible in light of very recent results by Dag Normann.

> Actually I would have superficially thought that this so called
> "explosion" as Sanders is calling it, which is totally normal in
> ordinary RM, would be even higher to Pi-1-1-CA0. I say this because an
> even more fundamental rudimentary theorem has such an explosion to
> Pi-1-1-CA0:
> 
> SUP. Every function from R into [0,1] has a supremum.

This has been proved in 1875 by Darboux (for domain restricted to intervals).  

> 
> NOTE: I am not sure what "Darboux supremum theorem" is referred to in
> https://cs.nyu.edu/pipermail/fom/2021-October/022920.html and may well
> be SUP above.

Indeed.  


> THEOREM 3.1. ACA0[3] + SUP proves the same second order sentences as Pi-1-1-CA0.
> 
> Proof: ACA0[3] + SUP proves Pi-1-1-CA0 by using a presentation(!) of
> some function from R into [0,1]. Specifically boldfaced arithmetic
> presentations. This is totally normal RM fare. So every theorem of
> Pi-1-1-CA0 is a theorem of ACA-[3] + SUP. Now let phi be a second
> order sentence provable in ACA0[3] + SUP. We have the obvious
> interpretation of ACA0[3] + SUP in Pi-1-1-CA0 that preserves second
> order sentences. First and second order objects are unchanged and the
> third order objects are interpreted as bold faced arithmetic
> operations which is easily handled in Pi-1-1-CA0. Under this
> interpretation, SUP is provable in PI-1-1-CA0. Hence the
> interpretation of phi is provable in Pi-1-1-CA0. Hence phi is provable
> in Pii-1-1-CA0. QED
> 
> Notice that the essence of this conservative extension result, Theorem
> 3.1, is just plain old ordinary RM, using presentations of third order
> objects.

Yes, but SUP and the Suslin functional S_2^2 does give you Pi12-CA_0.

And S_3^2 plus SUP yields Pi13-CA_0, and so on.

> I expect that all of the "explosions" touted in
> https://cs.nyu.edu/pipermail/fom/2021-October/022902.html behave this
> way, and are not only totally compatible with usual RM, but usual RM
> ideas and methods are exactly what is involved in proving the
> corresponding conservation results.

Dag Normann and I do have conservation results like that too, for many
of our results (and never did we claim anything else).  

> The exception is the ones
> involving 'Suslin's functional" which obviously has no bold faced
> arithmetic presentation. These results involving Suslin's functional
> is totally uninteresting and irrelevant for a foundationally oriented
> RM investigation of real analysis.

So the Suslin functional plus RCA_0^omega yields a Pi_3^1-conservative
extension of Pi_1^1-CA_0.  This is akin to your Thm 3.1.  

Yet my result is “set theory” and your result is not...


> Of course there is a subject we can call Reverse Set Theory of a
> totally different character. Going way back there is the reverse
> mathematics over base theory ZF focusing on variants of the axiom of
> choice.
> 
> CONJECTURE. For every one of the analysis statements in
> https://cs.nyu.edu/pipermail/fom/2021-October/022902.html Theorem 3.1
> holds. There is total compatibility with usual RM and the usual RM
> methods are exactly what is used to prove conservation.

So the Lindeloef lemma plus a discontinuous function on R yields Pi11-CA_0 (assuming RCA_0^omega).

Is that compatible with what you are saying?

> 
> QUESTION 1. Does Jordan decomposition prove Pi-1-1-CA0 over ACA0[3]?
> In RM, what is the status of bold faced arithmetically presented
> Jordan decomposition? I see it implies ATR0 and that is implicit in
> Normann/Sanders, and it is clear that it is proved in Pi-1-1-CA0. So
> at present there seems to be a gap. Totally normal for RM.
> 
> QUESTION 2. What can we say about the relationship between Jordan
> decomposition and SUP over ACA0[3]? Does SUP imply Jordan
> decomposition over ACA0[3]?
> 
> NOTE: Just because SUP implies Pi11-CA0 and within ordinary RM
> Pi11-CA0 proves presented Jordan decomposition, does NOT mean that SUp
> implies Jordan decomposition over ACA[3]. THUS we are beginning to see
> early indications of an interesting third order RM that isn't slavish
> straightforward lifting of second order RM to third order RM.
> 
> THEOREM 3.2. There is no second order sentence which implies SUP over ACA0[3].

Note that Dag Normann and I have a much stronger result:  no third-order functional S_k^2
can yield SUP (over RCA_0^omega).  

This is also true for a range of statements, like 

“a function of bounded variation on [0,1] has a supremum”

> The  unusual strength cited from the Suslin functional and other brute
> force characteristic functionals is entirely expected and not
> mathematically or foundationally interesting -

Agreed.  Although as I said, Suslin functional is just Pi11-CA_0, really. 

In isolation, this functional behaves, as expected, namely Pi_3^1-conservative over Pi11-CA_0.  Add the Jordan decomposition theorem,
and out comes Pi_2^1-CA_0.  

Best,

Sam