A question about ordinal definable real numbers

Question

If ZFC (Zermelo-Fraenkel set theory with the Axiom of Choice) is consistent, does it remain consistent when the following statement is added to it as a new axiom?

"There exists a denumerably infinite and ordinal definable set of real numbers, not all of whose elements are ordinal definable"

If the answer to the above question is negative, then it must be provable in ZFC that every denumerably infinite and ordinal definable set of real numbers is hereditarily ordinal definable. This is because every real number can be regarded as a set of finite ordinal numbers and every finite ordinal number is ordinal definable. Garabed Gulbenkian

Answer 1

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

Answer 2

(I am replacing prior nonsense with a completely different suggestion. I am also turning this into CW so details can be added by somebody with time (which, sadly, most likely won't be me). Comments prior to Feb. 9, 2011, refer to said prior nonsense.)

---

Start with $V=L$ and force to add a Mathias real $s$. Let $W$ be the resulting extension. Let $A$ be the set of reals $r$ that are Mathias generic over $L$ and such that $L[r]=W$. I strongly suspect that a real $r$ is in $A$ iff it differs from $s$ finitely often, and so $A$ is countable, ordinal definable, and lacks any ordinal definable members.

(I have briefly discussed this idea with other set theorists, but we did not elaborate any details.)

---

From Andreas Blass: The following began as a comment, but Andres suggested adding it to his answer, for improved visibility. As it stands, with ordinary Mathias forcing, this won't work, because if $r\subset\omega$ is a Mathias real then so is the result of shifting it to the right (or left) by 1, and it still generates the same model. Instead of a simple shift, you could apply any strictly monotone function from $L$. But suppose you did Mathias forcing with respect to the constructibly-first non-principal ultrafilter on $\omega$ in $L$. That would avoid this problem. (Note that Joel David Hamkins's comment also depends on the fact that Prikry forcing is with respect to an ultrafilter in the ground model.)