does the mean value theorem implicitly assume the axiom of choice? in real analysis, including some of the theory of transcendental numbers, the mean value theorem is an essential tool. I was wondering if its dependence on the existential quantifier, $\exists$, at least in some cases, means that the axiom of choice is necessary, since this quantifier merely affirms the existence of an otherwise non-specified real number. my apologies for the naivety of this question. I would appreciate a simple explanation from someone who feels more confident of axiomatics than I am. this would help me to gain the orientation requisite to thinking more clearly about the role of the axiom of choice in analysis.
thank you
 A: Posting this as an answer so that the question isn't left unanswered.
Using the existential quantifier doesn't in itself imply using the axiom of choice. To use the axiom of choice, one makes infinitely many arbitrary choices. This doesn't happen in standard proofs of the mean value theorem.
If you're interested in an introduction to axiomatic set theory, Roitman's Introduction to Modern Set Theory is available online freely and legally.
A: As Ayman Hourieh writes, using just one existential quantifier does not require the axiom of choice. The axiom of choice is used when we have an infinite family of sets, and we want to choose an element from each one.
To the question in your comment, there are many many weakenings of the axiom of choice. Some of them do not look like the axiom of choice at all, but are considered as weakenings nonetheless. But let us focus on the axiom of choice per se, "If $F$ is a family of non-empty sets such that $\varphi$, then there is a choice function for $F$". Here $\varphi$ is a parameter which may or may not limit $F$. We can do some on several key variables:


*

*The size of $F$. For example, we may want to limit ourselves to countable families, and this would be the axiom of countable choice.

*The size of the elements of $F$. For example we may want to require that the size of each set in $F$ is exactly $3$, or that it is finite, or smaller than the size of $\Bbb R$ (whatever it may be).

*The origin of $F$. Recall that every family of sets is really just a subset of some power set (i.e. the power set of $\bigcup F$). We may want to impose a limit on that. For example we may want to say that we can choose from families of sets of real numbers.
Then we can combine these three, for example "Every countable family of countable sets of real numbers admits a choice function". We can tweak with all these parameters and obtain different statements which may or may not imply one another (for example, being able to choose from any family of countable sets does not imply that we may choose from any countable family of sets).
Finally, to help you understand the role of the axiom of choice in classical analysis, let me point out that in general the axiom of countable choice is sufficient to prove all the results, and if one limits themselves to $\Bbb R$ (rather than arbitrary [separable] metric spaces) then sometimes even less is needed. Continuity and the Axiom of Choice is a striking example of where the axiom of choice subtly enters classical analysis.
