Editing Reverse mathematics (section)

=== Use of higher-order arithmetic ===

A recent strand of ''higher-order'' reverse mathematics research, initiated by [[Ulrich Kohlenbach]] in 2005, focuses on subsystems of [[higher-order arithmetic]].{{sfnp|Kohlenbach|2005}}
Due to the richer language of higher-order arithmetic, the use of representations (aka 'codes') common in second-order arithmetic, is greatly reduced.  
For example, a continuous function on the [[Cantor space]] is just a function that maps binary sequences to binary sequences, and that also satisfies the usual 'epsilon-delta'-definition of continuity.

Higher-order reverse mathematics includes higher-order versions of (second-order) comprehension schemes.  Such a higher-order axiom states the existence of a functional that decides the truth or falsity of formulas of a given complexity. In this context, the complexity of formulas is also measured using the [[arithmetical hierarchy]] and [[analytical hierarchy]].  The higher-order counterparts of the major subsystems of second-order arithmetic generally prove the same second-order sentences (or a large subset) as the original second-order systems.<ref name=k05h08>See {{harvtxt|Kohlenbach|2005}} and {{harvtxt|Hunter|2008}}.</ref>  For instance, the base theory of higher-order reverse mathematics, called {{math|RCA{{su|p=''&omega;''|b=0}}}}, proves the same sentences as RCA<sub>0</sub>, up to language.

As noted in the previous paragraph, second-order comprehension axioms easily generalize to the higher-order framework.  However, theorems expressing the ''[[compactness]]'' of basic spaces behave quite differently in second- and higher-order arithmetic: on one hand, when restricted to countable covers/the language of second-order arithmetic, the compactness of the unit interval is provable in WKL<sub>0</sub> from the next section.  On the other hand, given uncountable covers/the language of higher-order arithmetic, the compactness of the unit interval is only provable from (full) second-order arithmetic.{{sfnp|Normann|Sanders|2018}} Other covering lemmas (e.g. due to [[Lindelöf]], [[Giuseppe Vitali|Vitali]], [[Besicovitch]], etc.) exhibit the same behavior, and many basic properties of the [[gauge integral]] are equivalent to the compactness of the underlying space.