Propositions equivalent to the completeness of the real numbers

Question

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? :-)

Answer 1

Since the article I was looking for doesn't seem to exist, I decided to write one myself; the current draft can be found at http://jamespropp.org/reverse.pdf .

Comments are welcome!

Answer 2

EDIT: I noticed that I misunderstood the question after posting the answer, so this is not a answer to the question. I am leaving it here just in case it might be interesting to others.

---

This is studied in bounded reverse math by people like Fernando Ferreira and colleagues.

The base theory BTFA [Fer'94] is a two sorted theory version of Sam Buss's bounded arithmetic theory $S^1_2(\alpha)$ [Bus85, ch. 9] plus bounded collection/replacement for $\Sigma^b_\infty $ formulas ($B\Sigma^b_\infty$) plus a form of comprehension axiom for $\Delta_1$ sets ($\nabla^b_1CA$):

$$\forall x (\forall z \ \varphi(x,z) \leftrightarrow \exists y \ \psi(x,y)) \Rightarrow \exists Z \ \forall x \ (x \in Z \leftrightarrow \exists y \ \psi(x,y))$$

where $\varphi$ and $\psi$ are respectively $\Pi^b_1$ and $\Sigma^b_1$ formulas. This is a modification of Simpson's axiom in his book [Sim'09]. Because of its special form the first order part is conservative over $S^1_2$ and is incapable of using the full power of comprehension for $\Delta_1$ sets. On the other hand, the second order part of the smallest model of the theory is $\Delta_1$ sets.

In [FF'02, thm. 4], a version of the Intermediate Value Theorem is proven in BTFA. Some caution is needed here in formalizing the IVT. Also the proof is not constructive (either there is a rational number which is the root of the function or we can continue a process getting arbitrary close to a root. Deciding that a given rational number is not a root of the function is not decidable and this is required since we need to stop the process of dividing the current interval into two halves if we reach a root, i.e. we need this assumption so we have $f(m)<0 \ \lor \ f(m)>0$ where $m$ is the rational mid-point of the current interval). As far as I remember WKL is not provable in BTFA. See also [FF'05] and [FF'08].

---

References:

1. Fernando Ferreira, "A feasible theory for analysis", The Journal of Symbolic Logic 59, 1001-1011, 1994.

2. António Fernandes and Fernando Ferreira, "Groundwork for weak analysis", The Journal of Symbolic Logic 67, pp. 557-578, 2002.

3. António Fernandes and Fernando Ferreira, "Basic applications of weak König's lemma in feasible analysis", in "Reverse Mathematics 2001", edited by Stephen Simpson. Lecture Notes on Logic (Association for Symbolic Logic), vol. 21, pp. 175-188 (A K Peters, 2005).

4. Fernando Ferreira and Gilda Ferreira, "The Riemann integral in weak systems of analysis", Journal of Universal Computer Science, 14, no. 6, pp. 908-937 (2008).

5. Samuel R. Buss, "Bounded Arithmetic", Bibliopolis, Revision of 1985 Ph.D. thesis.

6. Stephen G. Simpson, "Subsystems of Second Order Arithmetic", Second Edition, Perspectives in Logic, Association for Symbolic Logic, Cambridge University Press, 2009.

Answer 3

Let $R$ be an Archimedean ordered field, and $S$ a non-trivial ultrapower extension of $R$. Then $R$ is complete if and only if $S$ admits a standard part; namely, every limited element of $S$ is infinitely close to an element of $R$. Here an element of $S$ is limited if it is between two elements of $R$. Two elements of $S$ are infinitely close if the difference is an infinitesimal, and an infinitesimal is between $-r$ and $r$ for every positive element $r\in R$.

A similar construction can be carried out in SPOT without ultrafilters.