Note: The exact formulation of "real closed field" I'm using is: a real closed field is defined to be an ordered field such that the intermediate value theorem holds for polynomials. Or equivalently, such that if $p \in R[t]$ is a polynomial, and $p(a) p(b) < 0$, then there exists $c$ between $a$ and $b$ such that $p(c) = 0$.

Specifically, the statement would be: if $R$ is a real closed field, $p \in R[t]$ is a polynomial, and $a < b$ with $a, b \in R$, then there exists $c \in R$ such that $a < c < b$ and $p(b) - p(a) = p'(c) (b - a)$.

I think it must be true, by a very abstract and not very illuminating argument:

  1. The first-order theory of real closed fields is complete. (I don't recall the exact proof of this, but I do recall seeing it in a model theory course I took.)
  2. The mean value theorem for polynomials of degree $n$ can be expressed as a first-order formula.
  3. This formula is true in the real closed field $\mathbb{R}$.
  4. Therefore, this formula is true in any real closed field.

First question: Is this indeed a valid argument?

Second question: Assuming it's a valid theorem, is there a more direct proof?

Of course, by the usual proof of the mean value theorem for $\mathbb{R}$, it would be equivalent to prove Rolle's theorem for polynomials. But the proof of the latter over $\mathbb{R}$ is very much tied to topological arguments on $\mathbb{R}$ which I don't see any easy way to generalize to arbitrary real closed fields.

I think I could derive Rolle's theorem from this consequence of the mean value theorem: if $p'(x) > 0$ whenever $a < x < b$, then $p(a) < p(b)$. Then, if $p'(x) > 0$ for all $x \in (a, b)$, that contradicts the hypothesis of Rolle's theorem; if $p'(x) < 0$ for all $x \in (a, b)$, then apply the statement to $-p$ to get a contradiction. Otherwise, either $p'(x) = 0$ for some $x \in (a, b)$ as required; or else, $p'(c_1) > 0$ and $p'(c_2) < 0$ for some $c_1, c_2 \in (a, b)$, and then applying the intermediate value theorem on the polynomial $p'$ would give the desired result. What I'm not sure of is, how I would go about proving this statement either in an arbitrary real closed field. (Or, I would expect this statement "positive derivative implies strictly increasing" to be true in arbitrary ordered fields, not just real closed fields.)

  • 3
    $\begingroup$ Yes, the argument is correct. $\endgroup$ – Rene Schipperus Nov 30 '17 at 0:59
  • $\begingroup$ The argument might be circular in a strict sense depending on your proof that RCF is complete. $\endgroup$ – Dap Nov 30 '17 at 5:40
  • 1
    $\begingroup$ @Dap Do you have a proof of completeness in mind that uses the mean value theorem? The intermediate value theorem for polynomials is closely connected to completeness of RCF (its sometimes taken as part of the axioms), but I'm not aware of the role of the mean value theorem. $\endgroup$ – Alex Kruckman Nov 30 '17 at 18:30
  • $\begingroup$ @AlexKruckman I don’t, I remembered something like MVT being used but as you say it was probably just the more fundamental IVT $\endgroup$ – Dap Nov 30 '17 at 18:38
  • $\begingroup$ @AlexKruckman Updated the question - the axiomatization of RCF that I was using was "ordered field such that the IVT holds for polynomials". $\endgroup$ – Daniel Schepler Nov 30 '17 at 18:48

Repeating the comment of Rene Schipperus: Yes, your argument is correct.

It's also possible to prove the mean value theorem directly, for definable functions in any o-minimal expansion of an ordered ring. Here is a blog post outlining a proof: https://ms.mcmaster.ca/~speisseg/blog/?p=933

In general, it's possible to prove a surprising amount of "tame real analysis" in the abstract model-theoretic context of o-minimality. If you're interested in this, take a look at the book "Tame topology and o-minimal structures" by Lou van den Dries.

  • $\begingroup$ OK, I had to look up on Wikipedia what "o-minimal" meant. Now the question would be why exactly a real closed field would be o-minimal (as the Wikipedia article claims). $\endgroup$ – Daniel Schepler Dec 8 '17 at 18:45
  • $\begingroup$ It's an easy consequence of quantifier elimination for RCF in the language of ordered fields. Every formula in one free variable is equivalent to Boolean combination of polynomial inequalities, each of which defines a finite union of points and intervals. $\endgroup$ – Alex Kruckman Dec 8 '17 at 18:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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