Kohlenbach's higher-order Reverse Mathematics

[Sam Sanders]

Dear FOM,

I have been getting some off-line emails on higher-order Reverse Mathematics, 
with both positive and negative reactions.  One thing is universal among these 
reactions, namely that there seems to be some confusion here.  

To alleviate this confusion, I will review the base theory of  high-order Reverse Mathematics, 
called RCA_0^omega, and provide a motivation for its axioms.  As we will see, this system 
only introduces the following kind of higher-order objects:

* third-order objects that are somehow represented/present in RCA_0 already, namely
functions obtained by primitive recursion and RM codes for continuous functions.  

* fourth-order objects and beyond that provide the most rudimentary language to talk
about higher types (namely projection of pairs and application of functionals).  

In this way, RCA_0^omega is on par with RCA_0, just boasting a richer language. 


First some history of higher-order RM: 

Kohlenbach introduces higher-order RM in his RM2001 paper.  Montalban mentions 
higher-order RM as a ‘wide open’ field in his “open problems in RM” paper in the BSL.  
In this light, I would expect higher-order RM to have the official blessing of the (second-order) 
RM community.  


Secondly, we get down to brass tacks:  

The language of RCA_0^omega includes all finite types: type 0 (1st order) for natural
numbers, type 1 (2nd order) for elements of Baire space, type 2 (3rd order), type 3 (fourth order), et cetera.

Experience bares out that one rarely uses type 3 or beyond, while type 2 is used a lot. 
Presumably, this was the motivation behind Noah Schweber’s approach, which we will 
not discuss here beyond saying that it is essentially the restriction to type 2 of higher-order RM.  


The following axioms of RCA_0^omega need no motivation, I would say, as
they are included in RCA_0 (in the second-order language):

a) Axioms expressing that N with the usual constants forms an orderer semi-ring

b) The induction axiom for quantifier-free formulas.

c) Primitive recursion for N-> N functions (as available in RCA_0) defined via a third-order “recursor" constant.  


The following axiom expresses that equal inputs yield equal outputs for third-order and higher objects. 
According to U. Kohlenbach, one cannot do mainstream math without this axiom.  

d) The axiom of extensionality for functionals of finite types


The following axioms define “projection for pairs” and “function application”:  

e) The defining axioms for the Sigma and Pi combinators, aka K and S combinators.  

These combinators allow us to do lambda-abstraction, a convenient book-keeping device in this context (and nothing more).  


The following axiom is needed to make sure RM-codes for continuous functions on N^N actually denote (continuous) third-order functions.   

f) QF-AC^{1,0}:  for quantifier-free A, if (forall f^1)(exists n^0)A(f,n), then there is G^2 with (forall f^1)A(f, G(f))

And that is all folks!


Two important observations

*)  items c) and f) introduce third-order objects, but only those that are somehow represented in RCA_0 already, namely
functions obtained by primitive recursion and RM codes for continuous functions.  

*) item e) introduces fourth-order objects and beyond.  These are however utterly basic: K is a projection operator for pairs
and S is a application/evaluation operator that essentially just returns f(x) on input f and x (if the types are correct).  


I do not wish to be a nuisance to anyone, but I do have the following request:

Let anyone who does not approve of this union (the axioms of RCA_0^omega), speak now or forever hold their peace!

For those that would speak up, please provide some arguments why the axioms a) - f) are not acceptable (in contrast to
the associated axioms of RCA_0 if applicable).  

Best,

Sam