The taming of the Reverse Mathematics zoo

TL;DR

This paper demonstrates that the exceptional theorems in Reverse Mathematics, known as the zoo, unify under the Big Five classification when considering their uniform versions, revealing a hidden computational aspect of Nonstandard Analysis.

Contribution

It shows that all uniform versions of zoo-theorems fall into the arithmetical comprehension category, simplifying the classification of these exceptional theorems.

Findings

Uniform zoo-theorems fall into the Big Five category of arithmetical comprehension.

A novel algorithm $rak{RS}$ translates proofs in Nonstandard Analysis to standard equivalences.

Explicit functional conversions establish the computational equivalence between principles.

Abstract

Reverse Mathematics is a program in the foundations of mathematics. Its results give rise to an elegant classification of theorems of ordinary mathematics based on computability. In particular, the majority of these theorems fall into only five categories of which the associated logical systems are dubbed `the Big Five'. Recently, a lot of effort has been directed towards finding \emph{exceptional} theorems, i.e.\ which fall outside the Big Five categories. The so-called Reverse Mathematics zoo is a collection of such exceptional theorems (and their relations). In this paper, we show that the uniform versions of the zoo-theorems, i.e. where a functional computes the objects stated to exist, all fall in the third Big Five category arithmetical comprehension, inside Kohlenbach's higher-order Reverse Mathematics. In other words, the zoo seems to disappear at the uniform level. Our classification applies to all theorems whose objects exhibit little structure, a notion we conjecture to be connected to Montalban's notion robustness. Surprisingly, our methodology reveals a hitherto unknown `computational' aspect of Nonstandard Analysis: We shall formulate an algorithm $\mathfrak{RS}$ which takes as input the proof of a specific equivalence in Nelson's internal set theory, and outputs the proof of the desired equivalence (not involving Nonstandard Analysis) between the uniform zoo principle and arithmetical comprehension. Moreover, the equivalences thus proved are even explicit, i.e. a term from the language converts the functional from one uniform principle into the functional from the other one and vice versa.