We investigate the provability or nonprovability of certain ordinary mathematical theorems within certain weak subsystems of second order arithmetic. Specifically, we consider the Cauchy/Peano existence theorem for solutions of ordinary differential equations, in the context of the formal system RCA 0 whose principal axioms are ▵ 0 1 comprehension and Σ 0 1 induction. Our main result is that, over RCA 0 , the Cauchy/Peano Theorem is provably equivalent to weak Konig's lemma, i.e. the statement that every infinite {0, 1}-tree (...) has a path. We also show that, over RCA 0 , the Ascoli lemma is provably equivalent to arithmetical comprehension, as is Osgood's theorem on the existence of maximum solutions. At the end of the paper we digress to relate our results to degrees of unsolvability and to computable analysis. (shrink)

We prove that every countable non-standard model of WKL0 has a proper initial part isomorphic to itself. This theorem enables us to carry out non-standard arguments over WKL0.

Within a weak subsystem of second-order arithmetic , that is -conservative over , we reformulate Kreisel's proof of the Second Incompleteness Theorem and Boolos' proof of the First Incompleteness Theorem.

Within a weak subsystem of second‐order arithmetic WKL0, we develop basic part of non‐standard analysis up to the Peano existence theorem.

In this paper, we show within RCA 0 that weak Konig's lemma is necessary and sufficient to prove that any (separable) compact group has a Haar measure. Within WKL 0 , a Haar measure is constructed by a non-standard method based on a fact that every countable non-standard model of WKL 0 has a proper initial part isomorphic to itself [10].