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

  • $\begingroup$ My omission of the Archimedean axiom from the base theory was intentional. Indeed, one way to show that various theorems of calculus do NOT imply completeness is to show that they are satisfied by non-Archimedean totally ordered fields. $\endgroup$ Apr 19, 2011 at 21:29
  • $\begingroup$ This reference might help: math.hawaii.edu/~tom/mathfiles/rolle_Illinois.pdf Of course you can also look for more recent articles that cite it. $\endgroup$ Apr 20, 2011 at 0:37
  • $\begingroup$ T. W. Körner, A Companion to Analysis discusses some of this. $\endgroup$
    – lhf
    Apr 20, 2011 at 10:34
  • 2
    $\begingroup$ This question is difficult to answer because it is too vague. First, there are two different axioms of completeness for the reals: Cauchy completeness and Dedekind completeness. I suspect you mean the latter, but this is not clear from the question. Second, the base theory you describe is unclear. What kind of comprehension axioms does your "naïve set-theory" comprise? Are the (optional!) natural numbers distinguished elements of the field or are they a separate sort? How are functions coded in this theory? $\endgroup$ Jul 15, 2011 at 15:19
  • 1
    $\begingroup$ François is correct in surmising that when I wrote "completeness" I meant "Dedekind completeness". As for what base theory I am presupposing, François answered this question very convincingly in the thread mathoverflow.net/questions/71344/… : it's second-order logic with standard semantics. $\endgroup$ Jul 27, 2011 at 14:37

2 Answers 2


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!

  • 1
    $\begingroup$ Very interesting! What would be wonderful is a chart with arrows giving the implications between the various properties. $\endgroup$ Jul 26, 2011 at 19:30
  • $\begingroup$ I am having trouble in understand the exact theory that you are working in. It seems to me like a modification of the theory RCF (the theory of real closed fields which is complete for the first order properties of real numbers in the language of ordered fields), it would be nice to state the exact language and axioms of the theory in one place. $\endgroup$
    – Kaveh
    Jul 26, 2011 at 20:08
  • $\begingroup$ You may also want to check the first volume of "Constructivism in Mathematics" by van Dalen and Troelstra where they develop a theory for elementary analysis and discuss the equivalence/non-equivalence of various analytical principles and definition (constructively). $\endgroup$
    – Kaveh
    Jul 26, 2011 at 20:11
  • $\begingroup$ I'll look into van Dalen Troelstra; thanks for the reference. Meanwhile, can you give me more information about the completeness of the theory RCF? This might resolve the issue about provability that I didn't know how to address at the bottom of page 2 and the top of page 3. $\endgroup$ Jul 26, 2011 at 21:59
  • $\begingroup$ The language of RCF is the language of ordered rings. The axioms are the axioms for an ordered field plus axioms stating that every polynomial of odd degree has a root (IIRC). The theory is complete in the sense that for any true first order sentence in this language, either RCF proves it or RCF proves its negation. You can find more about RCF in model theory books like David Marker's. $\endgroup$
    – Kaveh
    Jul 27, 2011 at 0:22

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].


  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.

  • $\begingroup$ This is a good answer, Kaveh. You should undelete it. There is also interesting work of Phuong Nguyen and Stephen Cook in this area that might be useful. $\endgroup$ Jul 16, 2011 at 6:40
  • $\begingroup$ I deleted my answer since these theories still satisfy "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." $\endgroup$
    – Kaveh
    Jul 27, 2011 at 11:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.