Assume that $V = L$ is true in the ground model $M$, and let $G$ be generic for $\mathbb{P} = Fn(I, 2)$, which is just the set of finite functions from $I$ to $2$. Then, ${\rm HOD}^{\mathbb{R}} = L[\mathbb{R}]$ is true in $M[G]$.

I assume that the proof is just a modification of the proof that ${\rm HOD}$ in $M[G]$ is contained in $L[\mathbb{P}]$ in $M$, but I can't figure out how to do it.

As in Kunen, ${\rm HOD}^\mathbb{R}$ are the sets hereditarily definable from ordinal and real parameters, and $L[\mathbb{R}]$ is the constructible hierarchy over the reals, i.e., $L[\mathbb{R}]_0 = \{\mathbb{R}\} \cup {\rm tcl}(\mathbb{R})$, $L[\mathbb{R}]_{\alpha +1} = {\rm Def}(L[\mathbb{R}]_\alpha)$, etc., and where ${\rm tcl}(x)$ is the transitive closure of $x$.

Hopefully the exercise isn't too trivial for mathoverflow.

  • 1
    $\begingroup$ Whether or not it is trivial, we need to see what you have tried or something that indicates the mental block you have. Tell us (briefly) more about things you know won't work. Gerhard "MathOverflow Isn't A Hint Service" Paseman, 2017.05.11. $\endgroup$ – Gerhard Paseman May 11 '17 at 17:36
  • 3
    $\begingroup$ @GerhardPaseman This is not a straightforward exercise, and the question is on-topic here at MO. $\endgroup$ – Joel David Hamkins May 15 '17 at 14:13
  • $\begingroup$ @Joel, I concur. I think the question needs improving by noting a specific challenge arising from the problem consideration. If the poster had said something like "I tried modifying the other proof, but at step blah, I could not see lemma.", that would give experts more clue as to the difficult portion and more students and other readers a specific item to consider and appreciate. To me, that would help frame an answer more useful than a solution: it would provide a means to teach or help understand the challenge being faced. Gerhard "More Like Advice Than Solution" Paseman, 2017.05.15. $\endgroup$ – Gerhard Paseman May 15 '17 at 15:07

This question seems to be a little more subtle than the usual homogeneity arguments. Here is one way that I found to do it.$\newcommand\R{{\mathbb{R}}}\newcommand\HOD{\text{HOD}}\newcommand\Ord{\text{Ord}}$

Allow me to describe the problem like this. We start in $L$ and force with $\newcommand\P{\mathbb{P}}\P=\text{Add}(\omega,\kappa)$ to add $\kappa$ many Cohen reals. In the forcing extension $L[G]$, we form the class $\HOD_\R^{L[G]}$ of hereditarily ordinal-definable sets. Meanwhile, $L(\R)$ is the class of sets constructible from reals in $L[G]$, defined by starting with the real numbers of $L[G]$ and iteratively taking the definable power set.

Theorem. $\HOD_\R^{L[G]}=L(\R)$.

Proof. The inclusion $L(\R)\subseteq\HOD^\R$ is easy to see, as alluded to in the question, because every real is definable using itself as a parameter and, as can be seen by induction, every object in $L(\R)$ is definable in $L(\R)$ using finitely many ordinal and real parameters, and so every object there is definable in $L[G]$ using real and ordinal parameters. Indeed, in $L(\R)$ there is a definable surjection $s:\Ord\times\R\to L(\R)$, and this surjection is definable in $L[G]$.

It remains to see, conversely, that $\HOD^\R\subseteq L(\R)$. Suppose that $A$ is hereditarily definable in $L[G]$ using ordinal and real parameters. By $\in$-induction, we may assume that $A\subseteq L(\R)$. Let $B=\{(\alpha,z)\mid s(\alpha,z)\in A\}$, which is also definable in $L[G]$, using the definable surjection. It suffices to show that $B\in L(\R)$.

Since $B\in\HOD_\R^{L[G]}$, there is a formula $\varphi$ for which $$B=\{(\alpha,z)\mid L[G]\models\varphi(\alpha,z,\beta,a)\},$$ for some ordinal parameter $\beta$ and real parameter $a$. Fix names $\dot B$ and $\dot a$ for which $\dot B_G=B$ and $\dot a_G=a$, and fix a condition $p_0\in G$ forcing that $\dot B$ is defined by $\varphi(\cdot,\cdot,\check\beta,\dot a)$.

Claim. $(\alpha,z)\in B$ if and only if there is $\dot z$ and $L$-generic $g$ for a countable complete suborder of $\P$ in $L$, with $p_0\in g$ and $\dot a_g=a$ and $\dot z_g=z$ and $\exists p\in g$ with $L\models p\Vdash \varphi(\check\alpha,\dot z,\check\beta,\dot a)$.

Proof. The forward implication is easy, since we can take $g$ to be a fragment of $G$. Conversely, suppose that we have $g$ and $\dot z$ as stated. Since $g$ is an $L$-generic real in $L[G]$, we may extend $g$ to a full $L$-generic filter $H\subset\P$ with $L[G]=L[H]$. It follows that there is an automorphism of the forcing $\pi:\P\cong\P$ in $L$ with $\pi[H]=G$. Since $p\Vdash\varphi(\check\alpha,\dot z,\check\beta,\dot a)$, it follows that $\pi(p)$ forces $\varphi(\check\alpha,\dot z^\pi,\check\beta,\dot a^\pi)$, where the superscript $\pi$ means that we have applied the induced automorphism on names.

Since $\dot a_G=a=\dot a_g=\dot a_H=\dot a^\pi_{\pi[H]}=\dot a^\pi_G$, it follows that there is some condition $q\in G$ forcing that $\dot a=\dot a^\pi$. Without loss, $q\leq \pi(p)$. So $q$ forces $\varphi(\check\alpha,\dot z^\pi,\check\beta,\dot a^\pi)$. Since $z=\dot z_g=\dot z_H=\dot z^\pi_{\pi[H]}=\dot z^\pi_G$, this implies $(\alpha,z)\in B$, as desired. QED (claim)

The claim implies the theorem, since that definition can be carried out in $L(\R)$, using $a$ and $\beta$ as parameters and the fact that the forcing relation is definable in $L$. QED

This argument is a little more complicated than I expected, and I'm not sure if there is a more direct argument.

  • $\begingroup$ One can avoid the fussing with $\dot a$ if you just move to $L[a]$ as a new ground model. $\endgroup$ – Joel David Hamkins May 15 '17 at 16:05
  • $\begingroup$ The first inclusion is trivial. $L(\Bbb R)$ is the smallest model of ZF which contains all the reals, certainly any $N$ which contains all the reals satisfies $L(\Bbb R)\subseteq N$. In particular $\rm HOD_\Bbb R$. $\endgroup$ – Asaf Karagila May 16 '17 at 10:57
  • 1
    $\begingroup$ I agree with that. That is why I said it is "easy to see". The question is about the converse. $\endgroup$ – Joel David Hamkins May 16 '17 at 11:04
  • $\begingroup$ Thanks so much, Joel! Sorry it took me a while to work through your answer! $\endgroup$ – Sam Roberts May 22 '17 at 10:03
  • $\begingroup$ Just came back to this, and realised I wasn't as clear as I thought I was :S How do we construct $H$, and how do we know that there is such a $\pi$ in $L$? Thanks again for all your help, Joel! $\endgroup$ – Sam Roberts May 30 '17 at 13:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.