Question

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"?

Answer 1

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.

Answer 2

There is a nice model-theoretic 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 (parameter-free) 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 Tarski-Vaught 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), 363-385. MR2140616] has shown that for a completion $T$ of $ZF$ the following three properties are equivalent:

1. $T \vdash V = OD$.
2. $T$ has a unique Paris model up to isomorphism.
3. $T$ has a prime model.

A Paris model is a model where every ordinal is first-order definable. This is slightly weaker than property (A), but it is equivalent when $T \vdash V = OD$.

Answer 3

The question admits an answer that may be somewhat more "concrete" in the sense of having "applications", and seems somewhat relevant (correct me if I am wrong). Namely, Kanovei and Shelah have constructed definable models of the hyperreals where each of the nonstandard elements is actually undefinable. Thus the set of nonstandard elements is definable, but none of its members are.