Descriptions of sets and the Axiom of Choice If we specifically do not assume the Axiom of Choice, are all the sets that we can prove to exist specified by some finite formula? (All the other Zermelo-Frankel set theory axioms seem constructive to me, so I want to say yes, but I'm not sure.) If not, what's an example of such a set?
A slightly related questions: in a previous question I had about the Axiom of Choice, some of the answerers mentioned the distinction between a function and "a function you can name". Assuming the Axiom of Choice is basically assuming the existence of a function you can't name; are there examples of unnameable functions if we don't assume the Axiom of Choice? (Again, I want to say no, but I want to make sure.)
 A: I believe that your first mistake is that the ZF theory is a lot less constructive then it seems. The axiom of choice in particular.
The answer to your first question is no. If something can be proved to exist, then you can write a formula defining the class of all sets which has this property. From this, however, you cannot say that every such set is definable. You cannot even have a canonical represntative which you can always use explicitly.
Here are some examples of sets that we cannot prove from ZF, or even ZF+Not AC:


*

*Andreas Blass proved in [1] that in ZF assuming that every vector space has a basis implies the axiom of choice, as a result if we assume that the axiom of choice does not hold then we can only tell that in our universe there is a vector space without a basis. We cannot actually define it, or even know over which field it is.

*When asserted, the axiom of choice tells us that every cardinal is an $\aleph$-number, and we have definable representative sets for each $\aleph$. That is there is a class function $C$ such that $C(X)=|X|$ and $C(X)=C(Y)\iff |X|=|Y|$. Such function may not be definable with the absence of choice. However, it may be definable depending on the universe. [2, Theorem 11.3]

*Assuming the axiom of choice itself does not hold, there are restricted versions of it (and there are many different ones) which are independent from one another, each asserting the existence of some sets that you cannot really define otherwise. Unless you specify exactly how much of the axiom of choice is violated there may be some choice hidden in your universe and you cannot prove that. [2, Chapter 8]

*In continuation from the last example, a universe of ZFC is in particular a universe of ZF without choice. If only specifying ZF, without an additional assumption that AC does not hold, it is possible that your universe is actually L, for example.
As for the second question, following from the first, we have that it is yes.
For example, take amorphous sets. These are infinite sets which cannot be written as a disjoint union of two infinite sets. Their existences violates the axiom of choice in a very strong way, as the axiom of choice implies that every infinite set can be written as a disjoint union of two parts equinumerous to the original set.
Suppose $A$ is an amorphous set. Then $A\in V$, and for some $\alpha$ we have that $A\in V_\alpha$ ($V_\alpha$ and $V$ are the von Neumann hierarchy).
It can be shown that the minimal $\alpha$ is a successor ordinal. Therefore for some $\beta$ we have $A\in V_{\beta+1}=\mathcal P(V_\beta)$. This means that there exists a partial function from $V_\beta$ bijective with this crazy set. Where does that happen in the hierarchy? How does the function look like? No one knows. It cannot be in the first $\beta=\omega$ levels, since in there everything is definably well ordered, but we cannot tell much more than that.
Of course that the axiom of choice, by definition, asserts that there are functions which exist and we cannot prove their existence otherwise. However as above shows, in its absence there are also functions which we cannot describe.

Bibliography:


*

*Blass A. Existence of bases implies the axiom of choice, (Axiomatic Set Theory (ed. J. E. Baumgartner, D. A. Martin, and S. Shelah) Contemp. Math. 31 (1984) 31-34).

*Jech T. The Axiom of Choice, North-Holland (1973).
A: 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 this MO question 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...
