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)

Extrapolating from the work of Mahlo , one can prove that given any pair of countable closed totally bounded subsets of complete separable metric spaces, one subset can be homeomorphically embedded in the other. This sort of topological comparability is reminiscent of the statements concerning comparability of well orderings which Friedman has shown to be equivalent to ATR0 over the weak base system RCA0. The main result of this paper states that topological comparability is also equivalent to ATR0. In Section (...) 1, the pertinent subsystems of second-order arithmetic and results on well orderings are reviewed. Sections 2 and 3 overview the encoding of metric spaces and homeomorphisms in second-order arithmetic. Section 4 contains a proof of the topological comparability result in ATR0. Section 5 contains the reversal, a derivation of ATR0 from the topological comparability result. In Section 6, additional information about the structure of the embeddings is obtained, culminating in an application to closed subsets of the real numbers. (shrink)

Two countable well orderings are weakly comparable if there is an order preserving injection of one into the other. We say the well orderings are strongly comparable if the injection is an isomorphism between one ordering and an initial segment of the other. In [5], Friedman announced that the statement “any two countable well orderings are strongly comparable” is equivalent to ATR 0 . Simpson provides a detailed proof of this result in Chapter 5 of [13]. More recently, Friedman has (...) proved that the statement “any two countable well orderings are weakly comparable” is equivalent to ATR 0 . The main goal of this paper is to give a detailed exposition of this result. (shrink)