Denote Zermelo Fraenkel set theory without choice by ZF. Is the following true: In ZF, every definable non empty class A has a definable member; i.e. for every class $A = \lbrace x : \phi(x)\rbrace$ for which ZF proves "A is non empty", there is a class $a = \lbrace x : \psi(x)\rbrace$ such that ZF proves "a belongs to A"?

1$\begingroup$ Writing "id est" is really really pedantic. $\endgroup$– Harry GindiJan 1 '10 at 23:57

3$\begingroup$ @HarryGindi: Why? $\endgroup$– Ramiro de la VegaMar 12 '15 at 18:57
Update. (June, 2017) François Dorais and I have completed a paper that ultimately grew out of this questions and several followup questions.
F. G. Dorais and J. D. Hamkins, When does every definable nonempty set have a definable element? (arχiv:1706.07285)
Abstract. The assertion that every definable set has a definable element is equivalent over ZF to the principle $V=\newcommand\HOD{\text{HOD}}\HOD$, and indeed, we prove, so is the assertion merely that every $\Pi_2$definable set has an ordinaldefinable element. Meanwhile, every model of ZFC has a forcing extension satisfying $V\neq\HOD$ in which every $\Sigma_2$definable set has an ordinaldefinable element. Similar results hold for $\HOD(\mathbb{R})$ and $\HOD(\text{Ord}^\omega)$ and other natural instances of $\HOD(X)$.Read more at the blog post.
Click on the history to see the original answer. Related questions and answers appear at:

$\begingroup$ I need a class A such that ZF proves "A is non empty" and for every class b, ZF doesn't prove "b is in A". Does the difference V \ OD qualify as such a class A? Similarly can ZF prove that the set of Cohen reals over L is nonempty  I'd confess that I've never seen forcing extensions over a class? Probably I'm missing something but it would be great if you can explicitly write the class A. Thanks a lot $\endgroup$– AshutoshJan 2 '10 at 0:05

$\begingroup$ Well, VOD might be empty, and it is in the pointwise definable models. But there is a way to get around this difficulty, and I'll edit my answer above to explain it. Similarly, it is consistent that there are no Lgeneric Cohen reals. $\endgroup$ Jan 2 '10 at 0:31

3$\begingroup$ For ZFC, I know a particularly nice formula for which this fails: A = set of all well orderings of reals. A is non empty but ZFC doesn't prove that A has a definable member. This example, however, depends on axiom of choice. $\endgroup$– AshutoshJan 2 '10 at 2:16

1$\begingroup$ I noticed that your argument for ZF + property (A) > AC gives a nice characterization of the theories that satisfy property (A): If T is any consistent extension of ZF then, T has property (A) iff T proves V = HOD. $\endgroup$– AshutoshJan 2 '10 at 19:19

1$\begingroup$ I see! So the property IS firstorder expressible (contrary to what I had said in my first bullet point), and is just equivalent to V=HOD. That is, if a model satisfies V=HOD, then there is a definable wellordering of the universe, so every nonempty definable set will have a definable element (the least one), and conversely, if the model does not have V=HOD, then the set of minimal rank sets not in OD is definable, but has no definable element. $\endgroup$ Jan 2 '10 at 19:44
There is a nice modeltheoretic interpretation of the property you state, which I will call property (A).
By a theory of sets, I mean any theory $T$ with an extensional relation ${\in}$.
Fact 1. If $T$ is a theory of sets with property (A) then so does every extension of $T$.
Fact 2. If $T$ is a complete theory of sets with property (A) then $T$ has a unique prime model.
Fact 3. If $T$ is a complete theory of sets with a wellfounded prime model then $T$ has property (A).
The fact that ZF does not have property (A) follows from Fact 1 and the (simpler) observation that ZFC does not have property (A). However, Facts 2 and 3 give nice ways of finding extensions of ZF which do have property (A).
Without loss of generality, $T$ has enough closed terms so that if $T$ proves that the formula $\phi(x)$ has a unique solution then $T \vdash \phi(c)$ for some closed term $c$. (Otherwise, add a new constant $c$ for each such formula $\phi(x)$ together with the defining axiom $\phi(c)$. This is a conservative extension of $T$ with the desired property.) If $M$ is any model of $T$, then let $K_M$ be the substructure of $M$ whose ground set consists of all interpretations of the closed terms. Note that $K_M$ is completely determined by the complete theory of $M$.
Observe that if $\theta(z)$ is any formula, then $\psi(x) \equiv \forall z(z \in x \leftrightarrow \theta(z))$ has at most one solution by extensionality. Therefore, $T$ proves that $\phi(x) \equiv \psi(x) \lor (\forall z\lnot\psi(z) \land x = c_0)$ has exactly one solution (where $c_0$ is any fixed closed term). So there is a constant $c$ such that, in any model of $T$, if $\{z : \theta(z)\}$ is a set then $c = \{z:\theta(z)\}$. Of course, we always have $c = \{z:z\in c\}$. So in any model $M$ of $T$ the constants $c$ are precisely all the (parameterfree) instances of comprehension which exist in $M$.
In view of this, property (A) can be formulated as:
(A) For every formula $\phi(x)$, if $T \vdash \exists x\phi(x)$ then $T \vdash \phi(c)$ for some constant $c$.
Replacing $\phi(x)$ with $\phi(x) \lor \forall z\lnot\phi(z)$, we see that property (A) implies the seemingly stronger statement:
(A') For every formula $\phi(x)$ there is a constant $c$ such that $T \vdash \exists x \phi(x) \leftrightarrow \phi(c)$.
This reformulation of property (A) immediately implies Fact 1. By the TarskiVaught Test, property (A') says that if $M$ is any model of $T$ then the substructure $K_M$ of $M$ is an elementary submodel of $M$. Therefore, $K_M$ is the necessarily unique prime model of the complete theory of $M$, which establishes Fact 2.
For Fact 3, suppose that $T$ is complete and that $M$ is a wellfounded prime model of $T$. I will show that $M = K_M$, which immediately implies that $T$ has property (A). For the sake of contradiction, suppose that $M \neq K_M$. Since $M$ is wellfounded, there is an $a \in M \setminus K_M$ such that $a \subseteq K_M$. Since $M$ is prime, $a$ realizes a principal type $\phi(x)$. If $b$ also realizes $\phi(x)$, then $b \cap K_M = a$ since all elements of $K_M$ are definable. Therefore, $\phi(x)$ must imply $\forall z(\phi(z) \rightarrow x \subseteq z)$ over $T$. This means that $T$ proves that $\phi(x)$ has a unique solution, which contradicts the fact that $a \notin K_M$.
To partly answer Joel's comment whether wellfoundedness can be eliminated from Fact 3, Ali Enayat [Models of set theory with definable ordinals Arch. Math. Logic 44 (2005), 363385. MR2140616] has shown that for a completion $T$ of $ZF$ the following three properties are equivalent:
 $T \vdash V = OD$.
 $T$ has a unique Paris model up to isomorphism.
 $T$ has a prime model.
A Paris model is a model where every ordinal is firstorder definable. This is slightly weaker than property (A), but it is equivalent when $T \vdash V = OD$.


1$\begingroup$ By the way, I noticed that property (A) implies the Axiom of Choicesee the edit to my answer. A question: Do you need the prime model to be wellfounded in (3)? $\endgroup$ Jan 2 '10 at 14:49

$\begingroup$ I suspect that Fact 3 is false assuming only extensionality and not wellfoundedness. I don't know what happens when one assumes much more than just extensionality, like ZF. $\endgroup$ Jan 2 '10 at 19:40