The hereditarily ordinal-sequence-definable Solovay model

In $V[G]$ let $S={\bigcup }_{\alpha \in \mathrm{O}\mathrm{r}\mathrm{d}}{}^{\omega }\alpha$, the class of countable ordinal sequences. A set $x$ is $OD(S)$ when, for some $s\in S$, finite tuple of ordinals $\vec{\alpha }$, formula $\phi$ and rank $V_{\theta }^{V[G]}$, it is the unique $y\in V_{\theta }$ satisfying $\phi (y,s,\vec{\alpha })$ in that rank. Define

$M=HOD(S)=\{x:\mathrm{tc}(\{x\})\subseteq OD(S)\}\mathrm{.}$

Rank bounds and satisfaction codes make this a uniform first-order class: “$s\in S$” means that $s$ is a function with domain $\omega$ and ordinal range. Finite and countable tuples of members of $S$ are interleaved using a fixed pairing function on $\omega$, so the convention “one member of $S$” loses no parameters. Reals are themselves members of $S$ after identifying natural numbers with finite ordinals. This definition asserts no equality with $L(\mathbb{R})$ or $HOD(\mathbb{R})$.