Reverse-engineering Reverse Mathematics

An important open problem in Reverse Mathematics (Montalban, 2011 [16]; Simpson, 2009 [25]) is the reduction of the first-order strength of the base theory from I Sigma(1) to I Delta(0) + exp. The system ERNA, a version of Nonstandard Analysis based on the system I Delta(0) + exp, provides a partial solution to this problem. Indeed, weak Konig's lemma and many of its equivalent formulations from Reverse Mathematics can be 'pushed down' into ERNA, while preserving the equivalences, but at the price of replacing equality with 'approximate to' i.e. infinitesimal proximity (Sanders, 2011 (19]). The logical principle corresponding to weak Konig's lemma is the universal transfer principle from Nonstandard Analysis. Here, we consider the intermediate and mean value theorem and their uniform generalizations. We show that ERNA's Reverse Mathematics mirrors the situation in classical Reverse Mathematics. This further supports our claim from Sanders (2011) [19] that the Reverse Mathematics of ERNA plus universal transfer is a copy up to infinitesimals of that of WKL0. We discuss some of the philosophical implications of our results. (C) 2012 Elsevier B.V. All rights reserved.