Question

Can anyone provide an example of a set S which is definable in ZFC and provable in ZFC to be denumerably infinite, while at the same time, no set definable in ZFC can be proved in ZFC to be an element of S? Such examples are easy to find if S is allowed to be uncountable-for instance S could be the set of all non-measurable sets of real numbers. In most of the examples where S is uncountable the axiom of choice is needed just to prove that S is non-empty and the cardinal number of S is greater than the cardinal number of R.

Answer 1

Here are a few partial answers.

First, I claim that if ZFC is consistent, then for every ZFC-definable nonempty set $S$, whether countable or uncountable, it is consistent with ZFC that $S$ contains a definable element. Further, there will be a model of ZFC in which every element of $S$ is definable.

Suppose that we have defined a nonempty set $S$ in ZFC. What I mean by this is that we have provided the defining formula $\phi$ of $S$ and proved in ZFC that there is a unique object, which we call $S$, that satisfies $\phi$, and furthermore that ZFC proves that this set is nonempty.

Now, it is known that if ZFC is consistent, then there are pointwise definable models of ZFC, models in which every set is definable without parameters. The main result of my paper Pointwise definable models of set theory, joint with Jonas Reitz and David Linetsky, is that every countable model of ZFC and indeed of GBC has an extension obtained via class forcing that is pointwise definable, in which every set and indeed every class is definable without parameters. My point now is that if $M$ is a pointwise definable model of ZFC, then every member of $S$ as interpreted in $M$ will be definable, by some definition.

Although this answer seems relevant to me, it doesn't quite answer the exact question you asked, since we don't expect that ZFC will prove that that set is a member of $S$.

Second, I claim that there is an example if you drop the denumerability requirement. That is, there is a definable set $S$, which is provably nonempty, but which does not provably contain any specific definable object.

(This argument therefore fills in for your proposal with non-measurable sets, which I don't really see how to make work.)

Define $S$ to be the sets of minimal rank not in $\text{HOD}$, in the case that $V\neq\text{HOD}$, and otherwise $S=\mathbb{N}$. So ZFC proves that $S$ is nonempty, but there can be no definable object $a$ such that ZFC proves $a\in S$, since in this case, in a model of $V\neq\text{HOD}$, the object $a$ would be a definable set that is a subset of $\text{HOD}$, by the minimality part of the definition of $S$, and hence $a$ would be not only definable but hereditarily ordinal-definable and hence an element of $\text{HOD}$, contrary to the definition of $S$.

Further update. Extending the observation of Emil in the comments, let's prove that there is a positive solution, if you change the countability requirement, size $\aleph_0$, to require instead $\aleph_1$.

Theorem. There is a ZFC definable set $S$, which ZFC proves has size exactly $\aleph_1$, such that if ZFC is consistent, then for no ZFC-provably definable object $t$ does ZFC prove $t\in S$.

Proof. Let $S$ be the set of reals not in HOD, provided that CH holds and there are reals not in HOD, and otherwise let $S$ be $\aleph_1$ itself. ZFC proves that this set has size $\aleph_1$, since either $S$ is explicitly $\aleph_1$, or else there are reals not in HOD and CH holds. But if there are reals not in HOD, then it is not difficult to see that there must be continuum many reals not in HOD, and so if CH also holds, this has size $\aleph_1$.

Meanwhile, if ZFC is consistent, then there is a model in which CH holds and there are reals not in HOD. In this case, every element of $S$ is not in HOD, and so ZFC cannot prove that any particular definable object $t$ is in $S$. QED