Descriptions of sets and the Axiom of Choice

There is a strange pathology that occurs when looking deeply at such questions. This pathology is summarized by the following motto: If you do restrict only to things that must exist, then the Axiom of Choice is likely true. This is a very general motto and it applies to many contexts even outside set theory. Note, however, that it is just a motto and not an actual theorem. Before going into the case of set theory, let me talk a bit about constructive analysis where this pathology takes an interesting form. In the very early days of intuitionism, Brouwer introduced a bunch of so-called continuity principles. One such principle can be formulated as follows. Suppose $A(f,n)$ is a statement where $f$ stands for a function from $\mathbb{N}$ to $\mathbb{N}$ (i.e., an element of Baire space ${}^{\mathbb{N}}\mathbb{N}$) and $n$ stands for an element of $\mathbb{N}$. If $(\forall f \in {}^{\mathbb{N}}\mathbb{N})(\exists n \in \mathbb{N})A(f,n)$, then there is a continuous function $\nu:{}^{\mathbb{N}}\mathbb{N}\to\mathbb{N}$ such that $(\forall f \in {}^{\mathbb{N}}\mathbb{N})A(f,\nu(f))$ holds. Note that this is actually a variant of the Axiom of Choice, except that it is stronger since the selector $\nu$ is required to be continuous. A majority of systems of constructive analysis satisfy Brouwer's continuity principles, and hence a very strong form of the Axiom of Choice. You may say: "But this doesn't make sense! What if $A(f,n)$ is the graph of a discontinuous function, like characteristic function of the singleton $\{f_0\}$ for some fixed $f_0 \in {}^{\mathbb{N}}\mathbb{N}$?" Well, this is the magic of constructive systems, you can't prove that $(\forall f \in {}^{\mathbb{N}}\mathbb{N})(f = f_0 \lor f \neq f_0)$ since the Law of Excluded Middle is not constructive. Thus, you cannot prove that $(\forall f \in {}^{\mathbb{N}}\mathbb{N})(\exists n \in \mathbb{N})A(f,n)$ for your particular choice of $A(f,n)$. There is a very thought provoking moral here: It is wrong to say that the Axiom of Choice is nonconstructive! In fact, some very strong forms of the Axiom of Choice are essential components of many systems of constructive mathematics. Note, however, that existence in constructive systems is very strong. There are very strict requirements for being a collection of nonempty sets, so it is not entirely surprising that choice functions exist since there is a lot of implicit information packed in the constructive notion of "nonempty". Now let's stop this digression and come back to set theory. The first thing to ask is: what exactly are these sets which must exist? (I'll come back to "provable sets" in a bit.) One possible answer are the elements of the minimal model of ZF, i.e., the smallest level $L_\alpha$ of the constructible hierarchy that satisfies ZF. (Note that $\alpha = \mathrm{Ord}$ is a possibility here.) But then $L_\alpha$ is a model of $V = L$, therefore the Axiom of Choice is true! Maybe that's not the answer you had in mind, but it is very likely that the same thing happens with whatever you believe sets that must exist actually are... Why is this? Well, there is one simple recipe for this in the case of set theory. Sets that must exist all have descriptions since it is very hard to justify the existence of something that you can't even describe. While sets may not be wellordered, descriptions of sets certainly are. So, instead of searching for a particular set, search for a description of that set. This usually gives a very nice global choice function for the universe that consists only of sets that must exist (whatever that means). But you said "sets that we can prove to exist" while I keep rambling about "sets that must exist", why is that? Well, the notion of "provable sets" is very hard to make sense of and it is unlikely to mean what you think. The reason why it is hard to make sense of this is that "provable" is a syntactic notion and "sets" is a semantic one. Still, there is a way to make some sense of provable sets. It's not easy, and the answers to http://mathoverflow.net/questions/10413/definable-collections-without-definable-members-in-zf actually come to the conclusion that this really only makes sense when one assumes V = OD, which implies the Axiom of Choice for the reasons I explained above...