Choice function on $\mathcal P (\mathbb R) \setminus \{ \emptyset\}$ When I was first learning about the axiom of choice, a very helpful and fun exercise was to try to find a rule that maps every nonempty subset of $\mathbb R$ to one of its members.  No matter how hard you try, it was impossible to find one.  (If you try the same for the nonempty subsets of $\mathbb N$, it is pretty easy, just take the smallest member of each set.)
My first question is, has it been proved in some formal way that such a choice function cannot be completely described with a finite number of symbols? (I think this is equivalent to  the undecidability of the existence of a choice function on  $\mathcal P (\mathbb R) \setminus \{ \emptyset \}$ in ZF.)
Another question is, in ZF with the negation of AC, is it provable that there exists no choice function on $\mathcal P (\mathbb R) \setminus \{ \emptyset \}$ ?  (My guess is negative.)
 A: If there is a definable wellordering of $\mathbb{R}$, then every real number is ordinal definable. Conversely, if every real number is ordinal definable, then there is a definable wellordering of $\mathbb{R}$. Thus the assumption that there is a definable wellordering of $\mathbb{R}$ is equivalent to $\mathbb{R} \subseteq \mathrm{OD}$.
This assumption is completely independent of AC in the sense that all four combinations AC + $\mathbb{R} \subseteq \mathrm{OD}$, AC + $\mathbb{R} \not\subseteq \mathrm{OD}$, ¬AC + $\mathbb{R} \subseteq \mathrm{OD}$, ¬AC + $\mathbb{R} \not\subseteq \mathrm{OD}$ are relatively consistent with ZF! The details of this are somewhat involved, see Thomas J. Jech's The Axiom of Choice for an introduction to the various methods to prove independence from ZF.
A: In Kunen's book on set theory, he leads one through an exercise where one creates a model of ZF (assuming ZF is consistent) in which the power set of the natural numbers is not well orderable.  Since one can prove that the power set of the naturals is in bijective correspondence with the reals, in this model, the real numbers cannot be well orderable.
(I don't have Kunen at home with me now, and it's been a year or two since I even glanced at the relevant section.  If I remember, I'll update the reference next time I have a copy of the book nearby).
However, there can (I think, but I'm not positive) be models where choice fails and the reals are well orderable.  Note that choice refers to ALL sets, so one simply needs to rig things to fail at REALLY huge cardinal sizes but have choice work at lower levels.
Finally, there are models where choice functions are definable: Godel's universe $L$.  For example, in $L$, EVERY set is definable.  That is, given a set $X$, there is a first order formula (with parameters) $\phi$ such that $x\in X$ iff $\phi(x)$.  Now, a function from $X$ to $Y$ (including a choice function), is nothing but a special subset of $X\times Y$, and hence will be definable in $L$.
I learned about this last paragraph from assorted posting by Joel David Hamkins over at MO.  For example, see https://mathoverflow.net/questions/23393/set-theory-and-vl
edit I realize that this doesn't seem to address your question directly.  However, it's true that for any set $X$, the powerset of $X$ has a choice function iff $X$ can be well ordered.  See Levy's book "Basic Set Theory" on page 160 for details.
