902: Mathematical L and OD/RM

[Sam Sanders]

Dear FOM,

> What Sanders is talking about can reasonably be called "higher type RM",

Indeed, especially since Ulrich Kohlenbach has called it “higher order RM” (also the name of his RM2001 paper), a name I have used ad nauseam, the FOM would agree. 

> to clearly identify that it is a prima facie specialised math logic study and not meant to have anything like the foundational significance of the usual RM.

Ulrich’s higher-order RM is however mentioned by Montalban in the “open questions in RM” paper published around 2011 in the BSL.  

Why the sudden reaction now after 10 years?

>  So right off the bat, any use of what I call 4th and higher order objects (second order objects are say the reals numbers) for a base theory is prima facie unsuitable for a base theory. 

Here is where we disagree: 4th order objects and higher are just around in higher-order RM with the weakest possible axioms governing them (projection and application), as discussed at length / ad nauseam my previous email.  What is wrong with having the language around with the most basic constructs governing this language?

But let us go along with Harvey Friedman, not in the least because everything I have said also works if we “saw off” the type level at third-order objects, as follows.  

To be absolutely clear: take Kohlenbach's RCA_0^omega and remove all mention of fourth-order and higher in the language and axioms.  Let the resulting system 
be known as RCA_0^3, presumably very similar to Noah Schweber’s system.   

There are two points to be made here:  

1) the explosions from my previous email(s) still go through, and we will revisit a particularly conceptual one,

2) natural models of subsystems of third-order arithmetic satisfying Z_2 still falsify NIN (there is no injection from 2^N to N).  


> Now some case can be made for identifying "third order mathematics" and the need for having some sort of base theory with 3rd order objects present.

See RCA_0^3 above.  

The “explosions” I have mentioned still go through at this level.  For instance, both a) and b) in isolation do not go beyond ACA_0 when combined 
with RCA_0^3, while the combination a) + b) proves ATR_0.  

a) The Jordan decomposition theorem: a function of bounded variation on [0,1] can be written as the difference of two monotone functions 

b) The sign function on R exists (or any discontinuous function on R).  

Moreover, combining a) with the Suslin functional (i.e. higher-order Pi_1^1-CA_0), we obtain Pi_2^1-CA_0.  

The Suslin functional is the third-order object that decides Pi_1^1-formulas (in Kleene normal form).  RCA_0^3 plus the Suslin functional
is Pi_3^1-conservative over Pi_1^1-CA_0.  

> To get serious about this, we would have to examine what kind of very weak third order base theory like principles would be enough to take something like 
> 
> NIN. No injective map from pow(N) into N
> 
> and derive some interesting logical strength.

To the best of my knowledge, one cannot derive any strength from NIN (for rather technical reasons).  

However, NIN is still hard to prove as follows.  Let us start with the observation that many 
natural models of SOSOA (called REC, ARITH, HYP, …) are based on (Turing) computability theoretic 
classes.  Let us now build a natural model of a subsystem of third-order arithmetic that satisfies Z_2,
based on the canonical higher-order extension of Turing machines, namely Kleene’s S1-S9.  

Let S_k^2 be the third-order functional that decides Pi_k^1-formulas (in their Kleene normal form).  
Let RCA_0^3 be as above and define Z_2^3 as RCA_0^3 plus the union of all S_k^2.  As noted
previously, the system Z_2^3 is a conservative extension of Z_2.  

To build the “canonical” model M of Z_2^3, take all objects of order at most three computable (S1-S9)
in some S_k^2.  Then for each element f of Cantor space in M, we can assign a unique/least natural e 
such that  “e is the code for an S1-S9 algorithm to compute f from some S_k^2”.  

Let F be a mapping that to each f of Cantor space in M assigns such e.  Clearly such F exists by the Axiom of
Choice.  By Robin Gandy’s “selection principle”  (called “Gandy selection”), the model M already contains
such F.  Clearly, the latter is an injection from 2^N to N (from the pov of M).  

Hence, a most natural model of Z_2^3 satisfies the negation of NIN, making the latter hard to prove (in terms of conventional comprehension).  

> I would think that any such third order principles of an acceptable base theory like character would have at least a usable interpretation in the Borel functions. If that is the case then NIN adds no strength since NIN is well known to be true in the Borel functions. 

For representations of Borel functions, this would be correct. For “raw” third-order objects that happen to be Borel, not so much:

As noted in previous emails, NIN is equivalent (also over RCA_0^3) to versions of NIN for functions R-> Q of bounded variation, Borel functions, semi-continuous functions…

Best,

Sam