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