Can anyone point me to a reasonably comprehensive article (or book chapter) explaining which basic theorems of calculus are equivalent to the completeness axiom of the reals and which ones aren't?

Here "equivalent" means equivalent relative to a base system that includes all the ordered field axioms, plus naïve set theory, plus (optionally) the Peano axioms (which one probably needs if one wants to use the natural numbers as an index-set, e.g. in the Nested Intervals Property).

At first I thought reverse mathematics would be the place to look, but a little bit of poking around now leads me to think that reverse mathematics in the usual sense deals with more arcane issues, with base systems that are at once weaker and stronger than what I have in mind: Konig's infinity lemma isn't provable in all of them, but the Intermediate Value Theorem is.

(Stephen Simpson, in his Wikipedia article http://en.m.wikipedia.org/wiki/Reverse_mathematics, writes: "... RCA0 is sufficient to prove a number of classical theorems which, therefore, require only minimal logical strength. These theorems are, in a sense, below the reach of the reverse mathematics enterprise because they are already provable in the base system. The classical theorems provable in RCA0 include: ... Basic properties of the real numbers (the real numbers are an Archimedean ordered field; any nested sequence of closed intervals whose lengths tend to zero has a single point in its intersection; the real numbers are not countable). ... The intermediate value theorem on continuous real functions.".)

So, reverse mathematics may not be the place to turn for answers to questions like "Is the completeness of the reals equivalent to the Mean Value Theorem?" (answer: yes); but I'm sure someone has considered such questions systematically. Perhaps somebody wrote a beautiful Monthly article a few decades ago that explained things so clearly as to make the whole matter seem trivial, with the result that the article was forgotten? :-)

A Companion to Analysisdiscusses some of this. $\endgroup$ – lhf Apr 20 '11 at 10:343more comments