Return to Answer

This is a really great question, and it connects with many issues in set theory. Some of these other topics are related to alternative readings of the question, where one wants to allow parameters in the definition, or where one is considering only definitions in the projective hierarchy, defining sets of reals.

But let me consider the most direct interpretation of the question, as you have asked it. The answer is that it is independent of ZF, in the sense that some models of set theory will have the desired property, and others will not.

First, there are models of ZFC in which every object in the universe is definable without parameters. This is true in the so-called minimal model of ZFC (the smallest L_α which models ZFC), as well as many other models. Indeed, every countable model of ZFC has an extension to a pointwise definable model. And if every object is definable, then of course it has your desired property that every definable set has definable elements.

Second, there are models without the desired property. Consider the forcing extensions L[G] obtained by adding a Cohen real over the constructible universe L. Now, consider the set of L-generic Cohen reals. This set is definable without parameters, but it can have no definable member, since no L-generic Cohen real can be definable in L[G], since the definable objects in L[G] must all be in L, as the forcing is almost homogeneous.

Thus, some models of set theory have your property, and some do not.

Finally, other considerations to think about are:

 

• The property that definable sets have definable members is not actually first order expressible. Thus, one cannot really say in a formal sense that this statement is independent of ZFC, since it is not even expressible in the language. This is a second order property of a model of set theory, rather than a statemenbt of set theory itself.

 

• If one allows parameters, then your question is related to the difference between the class of ordinal-definable sets OD and the class HOD of hereditarily ordinal definable sets. These classes are first order definable, and it is consistent, first, that not every set is ordinal definable, and second, that OD is not the same as HOD. If V is not OD, then the difference V-OD is of course definable, but has no ordinal-definable members. This example is similar to the example above with L[G] (and I guess the same model works).

Responding to Ashutosh's first comment below. Let A(x) be the statement "x is a real number not in OD, or there or no such reals and x is a real". Thus, A is the class of reals not in OD, if this is nonempty, and the class of all reals, if they are all in OD. This class is provably nonempty, since either it consists of all reals, or a lot of reals, depending on whether the reals are all in OD or not. But A cannot provably contain any definable set, and indeed, any ordinal definable set, since it is consistent with ZFC that there are reals not in OD, and in this case A contains no ordinal definable elements. Thus, it has the properties you desired.

Nevertheless, my answer above shows that for any definable class A, it is consistent with ZFC that A has definable elements, since in the pointwise definable models, every element of A will be definable. So there cannot be a class A that is provably nonempty, such that ZF proves that every definition fails to define an element of A. Your requested property is exactly on the borderline, between ZF proving that definable sets are not in A, and ZF not proving that any particular definable set is in A.

I've realized that your property actually implies the Axiom of Choice. That is, I claim that any model of ZF with your definability property will necessarily also model AC. The reason is that if your property holds, then every set must be in OD, for if not, then we could define the set of minimal-rank sets not in OD, which would be definable, but have no minimal element. Thus, V=HOD, and this implies AC. There is always a definable well-ordering of HOD in V, where x precedes y if x is definable in a smaller V_α than y, or if they are defined in the same minimal V_α, then by an earlier definition.

Edit: The comments below, with remarks by F. G. Dorais (please vote up his answer), have now led to the realization that the requested property is equivalent to the assertion V=HOD. Namely, if a model satisfies V=HOD, then it has a definable well-ordering of the universe, and so every definable set will have a definable member (the least one in the definable order), and conversely, if the model thinks V is not HOD, then the set of minimal rank sets outside OD will be definable, but have no definable member.

In summary, the requested definability property IS first order expressible, and is equivalent to the axiom called V=HOD, introduced by Kurt Goedel.

Update. (June, 2017) François Dorais and I have completed a paper that ultimately grew out of this questions and several follow-up 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 ordinal-definable element. Meanwhile, every model of ZFC has a forcing extension satisfying $V\neq\HOD$ in which every $\Sigma_2$-definable set has an ordinal-definable 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](http://jdh.hamkins.org/when-does-every-definable-nonempty-set-have-a-definable-element/).

Click on the history to see the original answer. Related questions and answers appear at:

 
• Can $V\neq\HOD$, if every $\Sigma_2$-definable set has an ordinal-definable element?
 
• Is it consistent with ZFC (or ZF) that every definable family of sets has at least one definable member?
• We also make use of the $\Sigma_2$ conception of Local properties in set theory.

Edit: The comments below, with remarks by F. G. Dorais (please vote up his answer), have now led to the realization that the requested property is equivalent to the assertion V=HOD. Namely, if a model satisfies V=HOD, then it has a definable well-ordering of the universe, and so every definable set will have a definable member (the least one in the definable order), and conversely, if the model thinks V is not HOD, then the set of minimal rank sets outside OD will be definable, but have no definable member.

In summary, the requested definability property IS first order expressible, and is equivalent to the axiom called V=HOD, introduced by Kurt Goedel.

I've realized that your property actually implies the Axiom of Choice. That is, I claim that any model of ZF with your definability property will necessarily also model AC. The reason is that if your property holds, then every set must be in OD, for if not, then we could define the set of minimal-rank sets not in OD, which would be definable, but have no minimal element. Thus, V=HOD, and this implies AC. There is always a definable well-ordering of HOD in V, where x precedes y if x is definable in a smaller V_α than y, or if they are defined in the same minimal V_α, then by an earlier definition.