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 uncountablefor instance S could be the set of all nonmeasurable 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 nonempty and the cardinal number of S is greater than the cardinal number of R.

2$\begingroup$ Could you clarify your remark about nonmeasurable sets? It is relatively consistent with ZFC that some nonmeasurable sets are definable. For example, if V=HOD holds, then there is a definable nonmeasurable set of real numbers, namely, the least nonmeasurable set with respect to the HODwellordering of the universe. The same argument shows that under V=HOD there are definable instances of sets having any desired firstorder expressible property. $\endgroup$ – Joel David Hamkins Feb 11 '13 at 15:39

3$\begingroup$ Related questions: mathoverflow.net/questions/17608/…, mathoverflow.net/questions/44102/…, mathoverflow.net/questions/71537/…, mathoverflow.net/questions/107441/…, mathoverflow.net/questions/10413/…. $\endgroup$ – Joel David Hamkins Feb 11 '13 at 15:48

$\begingroup$ The question asks for provability, not consistency. Is there a definable set of reals which is provably nonmeasurable in ZFC? I rather doubt it, although I don’t see why the negative answer should be obvious, as the wording of the question suggests. $\endgroup$ – Emil Jeřábek Feb 11 '13 at 16:28

$\begingroup$ Yes, Emil, those were my thoughts exactly. I don't know how to prove that ZFC cannot prove that a definable set is nonmeasurable. $\endgroup$ – Joel David Hamkins Feb 11 '13 at 16:35

$\begingroup$ In the update to my answer, I provide a definable provably nonempty (but possibly uncountable) set such that ZFC, if consistent, does not prove any specific definable set is a member. This example can therefore substitute for the OP's proposal with nonmeasurable sets. $\endgroup$ – Joel David Hamkins Feb 11 '13 at 20:29
Here are a few partial answers.
First, I claim that if ZFC is consistent, then for every ZFCdefinable 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 nonmeasurable 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 ordinaldefinable 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 ZFCprovably 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

1$\begingroup$ If one just wants the consistency of a definable element of $S$, then one doesn't need pointwise definability; it suffices simply to consider a model of V=HOD, which has a definable wellordering of the universe. In this case, the least element of $S$ with respect to that order will be definable without parameters (and the next point, and the next, and so on). $\endgroup$ – Joel David Hamkins Feb 11 '13 at 16:17

$\begingroup$ Doesn't Solovay's model of ZFC + "All HOD(R) sets of reals are Lebesgue measurable" witness that, for any definable set (without parameters), ZFC cannot prove that such a set is Lebesgue non measurable? $\endgroup$ – Ashutosh Feb 12 '13 at 17:12

$\begingroup$ Ashutosh, I think that is almost right, except that he uses an inaccessible cardinal. $\endgroup$ – Joel David Hamkins Feb 12 '13 at 17:18

$\begingroup$ One can avoid inaccessibles by appealing to Shelah's model where a similar result holds for sets with Baire property. $\endgroup$ – Ashutosh Feb 12 '13 at 17:43

2$\begingroup$ You can redefine $S$ to be the set of reals outside HOD, or $\mathbb N$ if there are none such. The same argument applies, and moreover $S\le2^\omega$. $\endgroup$ – Emil Jeřábek Feb 14 '13 at 14:36