I know that the Axiom of Choice implies Excluded Middle, but I haven't been able to find any discussion of the other direction.
Does the law of excluded middle imply the axiom of choice?
Here's a stab at a proof, but I'm not sure if it's correct:
AC says that there is always a function f that can take a set $X$ with $\geq 1$ elements and chooses for each $x \in X$ whether $x \in A$ or $x \in B$ (exclusive).
For any $x \in X$, let P be the proposition that $x \in A \land \neg (x \in B)$ and let Q be the proposition that $x \in B \land \neg (x \in A)$.
By LEM, $P \vee \neg P$ and $Q \vee \neg Q$. So there are the following cases:
- $P \land Q$ . Therefore $x \in A \land \neg (x \in A)$. Contradiction.
- $P \land \neg Q$. Therefore $f(x) \in A \land \neg (f(x) \in B)$.
- $\neg P \land Q$. Thefore $f(x) \in B \land \neg (f(x) \in A)$.
- $\neg P \land \neg Q$. Therefore $x \in B \land \neg (x \in B)$. Contradiction.
The axiom of choice states that given a family of non-empty sets, there is a function mapping each of those sets to an element of the set. The idea is to be able to move from $\forall a\in A\exists x(x\in a)$ to $\exists f\forall a\in A(f(a)\in a)$.
What you're talking about is existential instantiation, i.e. if $X$ is not empty, then we can "name" an element of it. There is also no $A$ and $B$ involved (and in your statement there is no information about them either). People sometimes mistake EI to be an instance of $\sf AC$, but that is not the case.
And of course, we know that LEM does not imply $\sf AC$, since we know that $\sf ZF$ is consistent with $\lnot\sf AC$ while LEM holds.