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:
- 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.)
- The mean value theorem for polynomials of degree $n$ can be expressed as a first-order formula.
- This formula is true in the real closed field $\mathbb{R}$.
- 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.)
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.