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.
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."