Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations?

Abstract 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 RCA0whose principal axioms are comprehension and induction. Our main result is that, over RCA0, the Cauchy/Peano Theorem is provably equivalent to weak König's lemma, i.e. the statement that every infinite {0, 1}-tree has a path. We also show that, over RCA0, 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.