[FOM] The Big Five in a discontinuous world (jww Dag Normann)

[Sam Sanders]

Dear FOM-members,

Many of you were there in the early days of Reverse Mathematics (RM), or have followed the
extensive discussions on RM on this very list.  I believe I can therefore assume everyone knows 
about the “Big Five” systems of RM, the representation of continuous objects via codes in RM, etc.

As suggested by the subject, I wish to discuss the linear ordering of the Big Five of RM as follows:

			RCA_0 <- WKL_0 <- ACA_0 <- ATR_0 <- Pi_1^1-CA_0  			(*)

in a higher-order setting where discontinuous functionals occur.  Now, Ulrich Kohlenbach has 
introduced “higher-order RM” (See the “RM2001” volume) with base theory RCA_0^omega.  
The latter involves all finite types, in contrast to RCA_0, which only involves types zero and one.  

The richer language of higher-order RM allows one to formulate the following higher-order versions of ACA_0, 
ATR_0 and WKL_0: (Recall that WKL_0 states that any countable open cover of Cantor space has a finite sub-cover.)  

1) 2E is the higher-order version of ACA_0, and constitutes the prototypical *discontinuous* type two functional.

2) UATR is the higher-order version of ATR_0 where a functional outputs the result of iterating an 
    arithmetical formula along a countable well-ordering.  

3) THETA computes a finite sub-cover of Cantor space, i.e. for any g of type two, THETA computes (f_1, …., f_k) such that 
    the neighbourhoods defined from f_i restricted to g(f_i) (for i at most k) cover Cantor space.

Note that Tait’s fan functional can compute the values of THETA for *continuous* g, i.e. THETA is essentially
the former generalised to *discontinuous* inputs.  THETA is also robust in the usual sense of RM,
and RCA_0^\omega + THETA is a conservative extension of WKL_0. 

Nonetheless, one obtains the following equivalence:

		RCA_0^\omega + THETA   	proves the equivalence 		2E <-> UATR.  		(**)

Similar to (**), THETA guarantees that the higher-order versions of Pi_1^1-CA_0 and Pi_2^1-CA_0 are equivalent.

Hence, higher-order RM is fundamentally different from second-order RM.  The cause, in my opinion, is that we cannot 
talk about discontinuous objects in SOSOA.  However, we know that math gets very strange when we restrict ourselves 
to certain (even natural) classes of objects, like in Russian style recursive math.  Simpson even motivates RM based on this 
observation.  Hence, it seems we *should* have discontinuous functionals around, but then (**) and its ilk are unavoidable.  

In conclusion, (**) suggests that the picture (*) breaks down badly when going beyond second-order arithmetic, 
especially when considering discontinuous objects.   What the ramifications are of this observation, I leave to the
collective wisdom of the FOM to decide.  

Best,

Sam