set theory - A question about ordinal definable real numbers

The original problem solves in the positive: there is a model of ZFC in which there exists a countable OD (well, even lightface $Pi^1_2$, which is the best possible) set of reals $X$ containing no OD elements. The model (by the way, as conjectured by Ali Enayat at http://cs.nyu.edu/pipermail/fom/2010-July/014944.html) is a $mathbf P^{<omega}$-generic extension of $L$, where $mathbf P$ is Jensen's minimal $Pi^1_2$ real singleton forcing and $mathbf P^{<omega}$ is the finite-support product of $omega$ copies of $mathbf P$.

A few details. Jensen's forcing is defined in $L$ so that $mathbf P =bigcup_{xi<omega_1} mathbf P_xi$, where each $mathbf P_xi$ is a ctble set of perfect trees in $2^{<omega}$, generic over the outcome $mathbf P_{<xi}=bigcup_{eta<xi}mathbf P_eta$ of all earlier steps in such a way that any $mathbf P_{<xi}$-name $c$ for a real ($c$ belongs to a minimal countable transitive model of a fragment of ZFC, containing $mathbf P_{<xi}$), which $mathbf P_{<xi}$ forces to be different from the generic real itself, is pushed by $mathbf P_{xi}$ (the next layer) not to belong to any $[T]$ where $T$ is a tree in $mathbf P_{xi}$. The effect is that the generic real itself is the only $mathbf P$-generic real in the extension, while examination of the complexity shows that it is a $Pi^1_2$ singleton.

Now let $mathbf P^{<omega}$ be the finite-support product of $omega$ copies of $mathbf P$. It adds a ctble sequence of $mathbf P$-generic reals $x_n$. A version of the argument above shows that still the reals $x_n$ are the only $mathbf P$-generic reals in the extension and the set ${x_n:n<omega}$ is $Pi^1_2$. Finally the routine technique of finite-support-product extensions ensures that $x_n$ are not OD in the extension.

Addendum. For detailed proofs of the above claims, see this manuscript.

Jindra Zapletal informed me that he got a model where a $mathsf E_0$-equivalence class $X=[x]_{E_0}$ of a certain Silver generic real is OD and contains no OD elements, but in that model $X$ does not seem to be analytically definable, let alone $Pi^1_2$. The model involves a combination of several forcing notions and some modern ideas in descriptive set theory recently presented in Canonical Ramsey Theory on Polish Spaces. Thus whether a $mathsf E_0$-class of a non-OD real can be $Pi^1_2$ is probably still open.

Further Kanovei's addendum of Aug 23.
It looks like a clone of Jensen's forcing on the base of Silver's (or $mathsf E_0$-large Sacks) forcing instead of the simple Sacks one leads to a lightface $Pi^1_2$ generic $mathsf E_0$-class with no OD elements. The advantage of Silver's forcing here is that it seems to produce a Jensen-type forcing closed under the 0-1 flip at any digit, so that the corresponding extension contains a $mathsf E_0$-class of generic reals instead of a generic singleton. I am working on details, hopefully it pans out.

Further Kanovei's addendum of Aug 25.
Yes it works, so there is a generic extension $L[x]$ of $L$ by a real in which the
$mathsf E_0$-class $[x]_{mathsf E_0}$ is a lightface $Pi^1_2$ (countable) set with no OD elements. I'll send it to Axriv in a few days.

Further Kanovei's addendum of Aug 29. arXiv:1408.6642