The most common framework for classical Reverse Mathematics is no doubt second-order arithmetic. Kohlenbach has formulated a higher-order framework (See his RM2001 paper), and recent results by Normann-Sanders (arxiv link) suggest that very basic higher-order theorems (like ‘the unit interval is open-cover compact’) *fall* far outside of the Big Five, and do not even fit the linear order of the Godel hierarchy.

I am soliciting suggestions for similarly promising (but as basic as possible) topics to be studied in the higher-order framework.

To give the reader an idea: the following topics have been studied by Normann-Sanders, and behave as mentioned above (i.e. fall outside of the Godel hierarchy).

- open cover (aka Heine-Borel) compactness of the unit interval (including uncountable covers).
- Other covering lemmas, including Vitali’s, and related properties, like Lebesgue numbers (including uncountable covers).
- The Lindeloef property of $\mathbb{R}$.
- paracompactness of the unit interval (including uncountable covers).
- basic properties of the gauge integral (uniqueness, extension of Lebesgue and Riemann integrals,..).
- basic properties of the Lebesgue integral, formulated as a restricted gauge integral.
- basic properties of the Lebesgue integral, formulated with Kreuzer’s $\lambda^3$.
- Egorov and Lusin theorem for both formulations of the Lebesgue integral.
- The neighbourhood function principle (NFP) from intuitionistic mathematics.
- Urysohn’s identity for the unit interval.
- Uniform statements like: “A continuous function F on [0,1] has a modulus of uniform continuity AND the latter only depends on a modulus of continuity of F”.