A model without a choice function Suppose we force over $\operatorname{Add}(\omega, \omega)$ with a $V$-generic $G$. Let $g = \bigcup G$ and $r_i$ be the $i$th real added, i.e $r_i = \{n : g(i, n) = 1\}$.
Then define (in $V[G]$) for all $i$, $R_i = \{r \subseteq \omega : |r \Delta r_i| < \aleph_0 \}$. Let $S = \{\{R_{2i}, R_{2i+1}\} : i < \omega\}$. Then consider the model $N = \mathrm{HOD}(\operatorname{trcl}\{S\})^{V[G]}$. I want to show that $N$ has no choice function for $S$.
I know that there is a choice function for $\{\{r_{2i}, r_{2i+1}\}:i < \omega\}$ in $N$ at least, and I have tried some homogeneity arguments. Unfortunately I haven't been able to get far. I would appreciate hints or help.
 A: Let $p$ be a condition such that $p\Vdash\varphi(\dot X,\dot y,\check\alpha,\vec S_i)\text{ defines a choice function}$, i.e. $p$ forces that there is an ordinal-definable choice function with parameters in the transitive closure $S$.
Since $p$ is a finite condition in the Cohen forcing, and $\vec S$ is finite, we can assume for simplicity that if $(n,m)$ is in the domain of $p$, then $\{R_n,R_{n\pm1}\}$ or $R_n$ itself is in $\vec S$; and vice versa, if $R_n$ is in $\vec S$, then $(n,m)\in\operatorname{dom}(p)$ for some $m$, etc.. Here $\{R_n,R_{n\pm1}\}$ is the unique pair that contains $R_n$.
Pick some large enough $n$ such that $(n,m)$ is not in the domain of $p$, and therefore also not mentioned in $\vec S$ in the sense above. Let $q$ be a stronger condition such that without loss of generality, $q\Vdash\varphi(\{\dot R_n,\dot R_{n\pm1}\},\dot R_n,\check\alpha,\vec S)$, of course we can take $\dot R_{n\pm1}$.
Note that neither $n$ nor $n\pm1$ can appear in the original $p$ or $\vec S$. Let $m$ be large enough such that $(n,k)$ or $(n\pm1,k)\in\operatorname{dom}p$ implies $k<m$. Now consider the following automorphism $\pi$:

*

*It acts on the left coordinate as the cycle $(n\ \ n\pm1)$,

*On these two coordinates, $(n,k)$ is switched with $(n,m+k)$ for all $k<m$ (and likewise for $(n\pm1,k)$ that is).

In other words, $\pi$ "flips" between the $n$th and $n\pm1$th reals, and then on these two coordinates it also switches the first $m$ points with the next $m$ points to make sure that we end up in "a disjoint part of the domain".
We can show that:

*

*$\pi p=p$ and $\pi q$ is compatible with $q$: the former is easy, since $n$ and $n\pm1$ are not mentioned in the domain of $p$; the latter is straightforward, we only changed two coordinates and it is easy to see that these are compatible since we also moved them "internally" to make them disjoint.


*If $\dot x$ is in $\vec S$, then $\pi\dot x=\dot x$: this is also a straightforward consequence of $\pi p=p$ and the condition with which we selected $p$ and $\vec S$.


*$\pi\dot R_n=\dot R_{n\pm 1}$ and $\pi\dot R_{n\pm1}=\dot R_n$.
Now we get that $\pi q\Vdash\varphi(\{\pi\dot R_n,\pi\dot R_{n\pm1}\},\pi\dot x,\pi\check\alpha,\pi\vec S)$. But the above tells us that this is the same as writing $\pi q\Vdash\varphi(\{\dot R_n,\dot R_{n\pm1}\},\pi\dot x,\check\alpha,\vec S)$.
Using now that $q$ and $\pi q$ are compatible that means that $$\pi q\cup q\Vdash\varphi(\{\dot R_n,\dot R_{n\pm1}\},\dot x,\check\alpha,\vec S)\land\varphi(\{\dot R_n,\dot R_{n\pm1}\},\pi\dot x,\check\alpha,\vec S),$$
but it is easy to show that $\varnothing\Vdash\dot x\neq\pi\dot x$, since $\dot x$ is either $\dot R_n$ or $\dot R_{n\pm1}$. And so this is a contradiction.
