The mean value theorem in second order arithmetic (Q2758063)

This article extends the program of reverse mathematics cofounded by \textit{S. G. Simpson} [Subsystems of second order arithmetic, Berlin: Springer (1999; Zbl 0909.03048)]. Working in RCA\(_0\), the authors prove the following version of Rolle's theorem: If \(\Phi\) is a function which is continuous on \([0,1]\), differentiable on \((0,1)\), and satisfies \(\Phi (0) = \Phi (1) = 0\), then there is a \(w \in (0,1)\) such that \(\Phi^\prime (w) = 0\). As an immediate corollary, they obtain a proof in RCA\(_0\) of the mean value theorem. The theorems are based on a pointwise definition of differentiability, rather than asserting the existence of a derivative function. The authors thoughtfully include all the necessary coding information.