Higher-order Reverse Mathematics: a two-dimensional analogy

[Sam Sanders]

Dear FOM,

Contemplating the recent FOM discussion with Harvey Friedman, I can now 
provide a more precise description of higher-order Reverse Mathematics (RM), 
by way of Christmas present to FOM say.   I will provide an interesting analogy
based on the Axiom of Choice (AC) and ZFC.  


First, I should start with the caveat that the picture I paint below will probably
emerge regardless of one’s base theory (assuming the latter implies good-old RCA_0).
In particular, whether one uses Kohlenbach’s RCA_0^omega, or Friedman’s system(s),
the world will look the same qua third-order phenomena.  


Secondly, anyone with basic knowledge of set theory knows that given a theorem T
provable in ZFC, there is an immediate ache to show that T either implies some
fragment of AC, or is provable in ZF alone.  Hence, we have a “two-dimensional”
classification based on the following questions:

1) which fragment (if any) of AC is needed to prove T?

2) which fragment of ZF (potentially plus AC) is needed to prove T?

H. Herlich’s recent book on AC contains many equivalences involving fragments of AC
over ZF and fragments of the latter.  


Thirdly, my main point today is that higher-order RM involves the same kind of "two-dimensional”
picture, even if we only work in the language of third-order arithmetic.  In particular, given a 
third-order theorem T of ordinary mathematics, there is a two-dimensional classification based
on the following questions:

3) which fragment of conventional comprehension is needed to prove T?

4) which fragment of the Neighbourhood Function Principle (NFP) -if any- is needed to prove T?

Regarding 3), “conventional” comprehension is based on the usual formula classes: arithmetic, Sigma_1^1, … 
where only second-order parameters are allowed.  This can be given by second-order comprehension
or discontinuous “comprehension” functionals, like Kleene’s \exists^2 or Suslin’s functional S^2.

Regarding 4),  the NFP principle may be found in e.g. in Troelstra & van Dalen and has the following properties:

a) NFP is provable in ZF (and much weaker systems, namely already from Kleene’s \exists^3),

b) NFP is a fragment of AC involving *continuous* choice functions,

c) NFP can be viewed as a “more constructive” version of (unconventional) comprehension,

d) Fragments of NFP follow from many thms of ordinary mathematics.

There is a clear analogy between 1) and 2) on one hand, and 3) and 4) on the other hand.  
In particular, weak fragments of NFP are not provable from conventional comprehension 
(and vice versa) unless one goes all the way up to \exists^3 (which implies full SOA). 

In conclusion, I should point out that the coding practise of second-order RM unfortunately erases
the distinction made by 3) and 4).  This is why I push so hard for higher-order RM and third-order 
arithmetic: the two-dimensional picture of ordinary math is a reality that should not be denied or 
“coded away".  

Best,

Sam

PS: Perhaps some will use the above analogy to claim that third-order arithmetic is set theoretical
in nature.  I of course do not agree, but I do explicitly welcome this kind of discussion.