arXiv.org > math > arXiv:1412.2022
Mathematics > Logic
arXiv:1412.2022 (math)
[Submitted on 5 Dec 2014 (v1), last revised 27 Jul 2015 (this version, v6)]
Title:The taming of the Reverse Mathematics zoo
Authors:Sam Sanders
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.
Subjects: Logic (math.LO)
Cite as: arXiv:1412.2022 [math.LO]
(or arXiv:1412.2022v6 [math.LO] for this version)
From: Sam Sanders [view email]
[v1] Fri, 5 Dec 2014 15:08:36 UTC (38 KB)
[v2] Mon, 8 Dec 2014 08:54:02 UTC (39 KB)
[v3] Sun, 21 Dec 2014 19:21:01 UTC (39 KB)
[v4] Thu, 12 Feb 2015 11:42:47 UTC (43 KB)
[v5] Tue, 24 Feb 2015 17:24:05 UTC (44 KB)
[v6] Mon, 27 Jul 2015 09:43:02 UTC (40 KB)
math.LO