How can OD be not transitive

Question

In Kennen's book about the Independence Results, it is said that the class of ordinal definable sets ($OD$) need not be necessarily transitive. Therefore, if I'm not mistaken, we would have that $OD \neq HOD$. How can $OD$ be not transitive? Thank you very much.

Answer 1

The set $2^\omega$ is obviously $\operatorname{OD}$, since it is just the set of infinite binary sequences. But there may be reals (elements of $2^\omega$) which are not definable using only ordinals as parameters. In that case $\operatorname{OD}$ is not transitive.

One example where this occurs is when adding a Cohen real. Recall that Cohen forcing is the partial order $\mathbb{C} = 2^{<\omega}$ consisting of finite binary strings together with the natural extension relation. Whenever $G$ is $\mathbb{C}$-generic over $V$, $\bigcup G$ is an infinite binary sequence (so an element of $2^\omega$) which is the so called "Cohen-real".

Theorem. Let $\varphi(x,\alpha_0, \dots, \alpha_n)$ be a formula in the language of set theory with one free variable $x$ and ordinal parameters $\alpha_0, \dots, \alpha_n$. Let $G$ be $\mathbb{C}$-generic over $V$. Then, in $V[G]$, $c := \bigcup G$ is not uniquely defined by $\varphi$.

Proof. Suppose $V[G] \models \varphi(c,\alpha_0, \dots, \alpha_n)$. Then, by the forcing theorem, there is a condition $s \in 2^{<\omega}$ so that $$s \Vdash \varphi(\dot c, \check \alpha_0, \dots, \check \alpha_n),$$ where $\dot c$ is a name for $c$. Consider $c'$ to be the infinite binary sequence that is equal to $c$ except at $\vert s\vert$, i.e. $$c'(n) := \begin{cases} c(n) & \text{ if } n \neq \vert s \vert \\ 1-c(n) & \text{ if } n = \vert s \vert \end{cases}.$$ Then you can check that $c'$ is also a Cohen real over $V$, i.e. there is a $\mathbb{C}$-generic $H$ over $V$ so that $c' = \bigcup H$. And in fact you can also see that $s \in H$. Thus, by the forcing statement above, $$V[H] \models \varphi(c', \alpha_0, \dots, \alpha_n).$$

But $V[G]$ and $V[H]$ are exactly the same model since $H \in V[G]$ and vice-versa $G \in V[H]$ and a forcing extension is the smallest transitive model of ZFC containing the ground model and the generic filter. Thus in fact, $$V[G] \models c' \neq c \wedge \varphi(c, \alpha_0, \dots, \alpha_n) \wedge \varphi(c', \alpha_0, \dots, \alpha_n).$$ So in $V[G]$, $c$ is not uniquely defined by $\varphi$.