Dependent choice and $L(\mathbb R)$.

Question

I am curious what is the relation between the inner model $L(\mathbb R)$ and the axiom of dependent choice $\mathsf{DC}$. Do we have $$L(\mathbb R)\models \mathsf{DC},$$ when $V\models \mathsf{DC}$?

Answer 1

The inductive construction of $L(\mathbb R)$ shows that every element, say $x\in L_\alpha(\mathbb R)$, has the form $\{y\in L_\beta(\mathbb R):L_\beta(\mathbb R)\models\phi(y,\vec p)\}$ for some $\beta<\alpha$ and some parameters $p\in L_\beta(\mathbb R)$. Each parameter in $\vec p$ can itself be so expressed, with even smaller $\beta$. Continue thus until you get $x$ expressed in terms of finitely many ordinals, finitely many reals, and finitely many formulas. By coding, you get $x=F(\gamma,r)$ for an ordinal $\gamma$, a real $r$, and a definable class-function $F$ with a sufficiently simple definition to be absolute for $L(\mathbb R)$.

Now suppose you're given, in $L(\mathbb R)$, a binary relation $Q$ on some set $A$, such that $(\forall x\in A)(\exists y\in A)\,Q(x,y)$. You want an $\omega$-sequence $s$ such that, for all $n$, $Q(s(n),s(n+1))$. Define a new, smaller relation on $A$ by letting $Q'(x,y)$ mean that $Q(x,y)$ and $y=F(\gamma,r)$ for some $\gamma$ and $r$ such that no $\gamma'<\gamma$ and $r'$ have $Q(x,F(\gamma',r'))$. In other words, among all options $y$ for a fixed $x$, keep only those that can be represented as $F(\gamma,r)$ with minimum possible $\gamma$. Note that this $\gamma$ is determined by $x$; I'll write it as $\gamma(x)$.

This reduces the problem to dependently choosing reals $r$ to go with these minimal $\gamma$'s. In detail, starting with any specified $x_0\in A$, you want to choose an $\omega$-sequence $t$ of reals so that the sequence $s$ defined by $s(0)=x_0$ and $s(n+1)=F(\gamma(s(n)),t(n))$ satisfies $Q(s(n),s(n+1))$ (and in fact $Q'(s(n),s(n+1))$) for all $n$.

The task of producing such a $t$ is an instance of dependent choice (of reals), so it can be carried out in the real world $V$, by hypothesis. But $t$ is an $\omega$-sequence of reals, so it can be coded (in an absolute way) by a single real. Therefore $t$ is available in $L(\mathbb R)$, and, using it, we immediately get the desired $s$.