The Axiom of Choice and definability I've seen a lot of relations between the notion of the existence of a definable set with a given property and the necessity of AC is proving that there is a set with the property. For example:


*

*Under ZFC, the reals can be well-ordered, and under ZF, it is consistent that the reals cannot be well-ordered. There is no definable well-order of the reals.

*Under ZFC, there is a Lebesgue-nonmeasurable set, and under ZF, it is consistent that every subset of the reals is Lebesgue-measurable. There is no definable Lebesgue-nonmeasurable set.


How does one formalize or prove this relationship, either in general or for particular cases such as these? It makes some intuitive sense to me that the sets described in the axioms of ZF can all be described via comprehensions (i.e. $\bigcup X=\{x|\exists y\in X:x\in y\}$, $\{a,b\}=\{x|x=a\vee x=b\}$, $f(X)=\{x|\exists y\in X:x=f(y)\}$, and so on), while the choice function described in AC is inherently not definable given only its domain, so facts which are provably dependent on AC must also inherit this nonconstructive nature, but I have no idea how to prove any of that.
 A: In fact ZF also has non-definable sets. All you need is that classical logic holds and that it is a subtheory of ZFC.
Let $\phi(x)$ state that $x$ is a set that is a well ordering of the reals if a well ordering of the reals exists. By excluded middle there is such an $x$, because if there is a well ordering of the reals, we can use that, and if there is no well ordering of the reals  we can take anything (the empty set, say). So we know that $ZF \vdash (\exists x)\phi(x)$.
Suppose that we can define such an $x$. Formally this means that there is a formula $\psi$ such that $ZF \vdash (\exists ! x) \psi(x)$ and $ZF \vdash (\forall x)\psi(x) \rightarrow \phi(x)$. Since ZF is a subtheory of ZF we also have the same for ZFC. That is, $ZFC \vdash (\exists ! x) \psi(x)$ and $ZFC \vdash (\forall x)\psi(x) \rightarrow \phi(x)$. But ZFC proves that there is a well ordering of the reals, so in ZFC, $\phi(x)$ is logically equivalent to the statement that $x$ is a well ordering of the reals. Therefore $\psi$ must define in ZFC a well ordering of the reals and we get a contradiction.
So any classical subtheory of ZFC has "undefinable sets," but like Asaf Karagila says, there are extensions of ZFC where every set is definable. The axiom $V = OD$ is sufficient to do this (which is implied by the axiom $V = L$ that Asaf mentioned). The idea behind this is that you construct sets in a well behaved way and the "definition" of, say, the well ordering of the reals would be "the first well ordering of the reals that is constructed."
A: Here is how I would formalise the notion of definability.
Definition. Let $\phi\left(x\right)$ be a formula in the language of set theory (with the unique free variable $x$), and let $\mathsf T$ be a set of sentences in the language of set theory (usually $\mathsf{T=ZF}$ or $\mathsf{T=ZFC}$). We say $\phi\left(x\right)$ defines a set in $\mathsf T$ iff
$$
\mathsf T\vdash\exists !x\phi\left(x\right).
$$
Here, $\exists !x\phi\left(x\right)$ is an abbreviation for a formula meaning "there is a unique $x$ such that $\phi\left(x\right)$".
Example. The formula $\forall y\left(y\notin x\right)$ defines a set in $\mathsf{ZFC}$.
Definition. First note that if $\phi\left(x\right)$ defines a set in $\mathsf T$, then by adding some constant symbol $c$ to our language and the axiom $\phi\left(c\right)$ to $\mathsf T$, we obtain a conservative extension of $\mathsf T$. I will then say that $c$ is a constant term for $\mathsf T$ and that $\phi\left(x\right)$ defines $c$ in $\mathsf T$.
Example. The formula $\forall y\left(y\notin x\right)$ defines $\emptyset$ in $\mathsf{ZFC}$. Similarly, if $c$ is a constant term for $\mathsf{ZFC}$ then so are $\bigcup c$, $\mathcal P\left(c\right)$ and $\left\{x\in c:\psi\left(x\right)\right\}$. This allows us to use $\emptyset$, $\bigcup$, $\mathcal P$ and set-builder notation as we normally would when working in $\mathsf{ZFC}$.
Here is how I would try to describe the difference between Choice and the other set-building axioms in this setup. First consider any set-building axiom of $\mathsf{ZF}$, i.e. anything except Extensionality or Foundation. It is an exercise to see that the axiom can be written in the form $\forall y_1,\dots,y_n\exists x\varphi\left(x,y_1,\dots,y_n\right)$, where $\mathsf{ZF}\vdash\forall y_1,\dots,y_n\exists !x\varphi\left(x,y_1,\dots,y_n\right)$ (note the "!" here). (Technically, Infinity is not of this form in its usual formulation, but it can be replaced an axiom defining $\omega$ in $\mathsf{ZF}$.) Hence if $c_1,\dots,c_n$ are constant terms for $\mathsf{ZF}$, then $\varphi\left(x,c_1,\dots,c_n\right)$ defines a set in $\mathsf{ZF}$. However, if $\mathsf{ZF}$ is replaced by $\mathsf{ZFC}$, then this argument clearly breaks down.
I think it is in this sense that definability corresponds to not needing the axiom of choice. However, one might also try to formalise this idea as follows.
Conjecture. If $\phi\left(x\right)$ defines a set in $\mathsf{ZFC}$, then $\phi\left(x\right)$ defines a set in $\mathsf{ZF}$.
One could also interpret this as saying that "the axiom of choice does not help with uniqueness proofs". However, it is false (assuming that $\mathsf{ZF}$ is consistent).
Counterexample. Let $\phi\left(x\right)$ be the formula meaning "$x$ is an initial ordinal (i.e. well-orderable cardinal), and for every infinite set $y$ there is an injection $x\to y$". Clearly $\mathsf{ZF}\vdash\left(\exists x\phi\left(x\right)\right)\Leftrightarrow\phi\left(\omega\right)$, and $\mathsf{ZFC}\vdash\phi\left(\omega\right)$. But (providing we formalise the notion of "infinite set" appropriately, and assuming that $\mathsf{ZF}$ is consistent), $\mathsf{ZF}\not\vdash\phi\left(\omega\right)$. Hence $\phi\left(x\right)$ defines $\omega$ in $\mathsf{ZFC}$ but does not define a set in $\mathsf{ZF}$.
See also: http://en.wikipedia.org/wiki/Definable_set
