The axiom of choice has a reputation as being a nefarious actor in set theory, the source of all sorts of horrible1, nonconstructive things. For example, to quote wikipedia:
The axiom of choice proves the existence ... objects that are proved to exist, but which cannot be explicitly constructed
However, the more I've learned about the subject, the further this popular description seems to be from the truth. For example, the axiom of choice is a consequence of the axiom of constructibility — logically, one must already accept the possible existence of nonconstructible sets before one can even entertain the idea of denying choice!
So, choice is clearly not the origin of nonconstructible things, although it does help such horrors to propagate.
Furthermore, in many constructive approaches to mathematics, the axiom of choice is a theorem — often a trivial one. For example:
- In the propositions-as-types approach to doing logic in type theory, the assertion $\forall x \in X: \exists y \in x$ is literally a choice function on $X$
- In the theory of computation, (the analog of) global choice is baked into the foundations (e.g. as the graded lexicographic order on strings). Furthermore, it is heavily used in the very basics of the subject (e.g. "iterate over all strings").
So, this leaves me with a question: how did the axiom of choice get the reputation it has? Were people simply wrong a century ago but the attitudes born from that time still persist? Is there some subtlety that gets lost in the popular account that does warrant criticism? Something else?
1: I do not actually find such things horrible.