Mean value theorem and the axiom of choice
Solution 1:
Yes, this is an interesting technical point that is often overlooked. As written, Spivak is postulating the existence of the function that to each (positive, sufficiently small) $h$ assigns the value $\alpha_h$. On the face of it, this is an application of the axiom of choice, because the set of numbers $\tau$ between $a$ and $a+h$ such that $\displaystyle \frac{f(a+h)-f(a)}h=f'(\tau)$ does not need to be a singleton, or open, or closed, or any reasonably shaped set, so the problem of assigning to each such $h$ a specific such number $\tau$ requires infinitely many choices in what does not appear to be a straightforward definable manner.
One technical remark is that, using techniques of descriptive set theory, we can eliminate this use of choice since for $\eta>0$ small enough, the relation $$\{(h,\tau):0<|h|<\eta\mbox{ and }\frac{f(a+h)-f(a)}h=f'(\tau)\}$$ is Borel, and therefore admits what we call a co-analytic uniformization, provably in Zermelo-Fraenkel set theory without the axiom of choice. (This means that we can actually prove, without choice, the existence of a function $a_h$ as in Spivak's argument.)
That said, both this statement and its proof are definitely beyond the level of Spivak's textbook. Fortunately, in order to formalize what he does, we can proceed in a more elementary manner:
Let $L=\lim_{x\to a}f'(x)$, the limit whose existence is granted by assumption. For any $\epsilon>0$ there is a $\delta>0$ such that for any $\tau$, if $0\ne \tau$ and $|\tau|<\delta$, then $|f'(a+\tau)-L|<\epsilon$. It is enough to prove that $$ \left|\frac{f(a+h)-f(a)}h - L\right|<\epsilon $$ for any $h$ with $0\ne h$ and $|h|<\delta$. Since $\epsilon$ is arbitrary, this indeed shows that $f'(a)$ exists and equals $L$.
Now, given such an $h$, we know that there is a $\rho$ in the open interval with endpoints $a$ and $a+h$ such that $\displaystyle \frac{f(a+h)-f(a)}h=f'(\rho)$. There may in fact be many possible choices for $\rho$, but we do not need to choose any (that is, we do not need to assert the existence of the function $a_h$). Simply note that for any such $\rho$, we have $0<|\rho-a|<\delta$, and so indeed $$ \left|\frac{f(a+h)-f(a)}h - L\right|<\epsilon, $$ as needed.
A similar issue appears in (advanced) analysis, in the theory of the derivative, when studying Neugebauer's theorem that characterizes when a function is a derivative in terms of properties of a companion function playing the role of $a_h$ above. Without appealing to the descriptive set theoretic result mentioned above, Neugebauer's theorem appears to need more choice than the standard fragment usually assumed in analysis (dependent choices). I have not found any texts dealing with Neugebauer's theorem that address (or even appear aware of) this technicality.
Solution 2:
The Mean Value Theorem is a consequence of Rolle's Theorem, which says that if $f$ is continuous on $[a,b]$ and differentiable on $(a,b)$, and $f(a)=f(b)$, then there exists $c \in (a,b)$ such that $f'(c)=0$. This is proven by letting $c$ be a point where $f$ attains its global minimum or maximum on $(a,b)$; such a point must have $f'(c) = 0$.
To avoid having to make a choice here, you can specify $c$ uniquely as:
$$c = \sup\{x \in (a,b) | f \text{ attains its global minimum or maximum at } x\}$$
Then $f$ attains its global minimum or maximum at $c$, by continuity. (See [1] below for what to do if $c=b$.)
Armed with this version of Rolle's Theorem, you can use it to prove a similar non-choice version of the Mean Value Theorem. You can then use this theorem in your proof.
[1] It can happen that this supremum is equal to $b$, which we don't want. In this case:
if $f(b)$ is a global minimum but not a global maximum, let $c = \sup\{x \in (a,b) | f \text{ attains its global maximum at } x\}$;
if $f(b)$ is a global maximum but not a global minimum, let $c = \sup\{x \in (a,b) | f \text{ attains its global minimum at } x\}$;
if $f(b)$ is both a global minimum and a global maximum, then $f$ is consant, so we can choose $c=\frac12(a+b)$.
Solution 3:
I don't think $\alpha_h$ being a choice function has much to do with what the author is talking about. He is recommending the reader to try to prove that $$ \lim_{h\to0}f'(\alpha_h) = \lim_{x\to a}f'(x) $$ What the left side means is: $$ \lim_{h\to0}f'(\alpha_h) = c \iff \forall\epsilon,\exists\delta>0\mid|h|<\delta \Rightarrow|f'(\alpha_h)-c|<\epsilon \tag{1} $$ And the right side means: $$ \lim_{x\to a}f'(x) = c \iff \forall\epsilon,\exists\delta>0\mid|x-a|<\delta \Rightarrow|f'(x)-c|<\epsilon \tag{2} $$ You know that $(2)$ is true, so you have to prove that $(2)\Rightarrow (1)$.
First remember that $\alpha_h\in (a,a+h)$. So $0<\alpha_h-a<h$ and $|\alpha_h-a|<|h|$. Now just pick $x=\alpha_h$. You know that for any $\epsilon,h>0$, the following is true: $$ \exists\delta>0\mid|\alpha_h-a|<\delta\Rightarrow|f'(\alpha_h)-c|<\epsilon \tag{3} $$ You also know that $|h|<\delta\Rightarrow|\alpha_h-a|<\delta$. So it is also true that: $$ \exists\delta>0\mid|h|<\delta\Rightarrow|\alpha_h-a|\Rightarrow|f'(\alpha_h)-c|<\epsilon \tag{4} $$ Which shows that $(1)$ is true. Note that we arrived at the same limit $c$.