I was reading Solovay's celebrated theorem on the existence of a model of ZF, in which every set of reals is Lebesgue-measurable from Kanamori's the higher infinite and I have a question.
Bellow is the statement that I think I have a proof for which has an assumption, which I don't know how to prove.
Suppose now that $A \subseteq {}^{\omega}\omega$ with $A \in L(\mathbb{R})$. Then $A$ is ${}^{\omega}On\text{-definable}$.
Also we say that $A$ is $^{\omega}On\text{-definable}$ when there exists a formula $\psi$ and some $a \in {}^{\omega}On$ s.t. $$ x \in A \longleftrightarrow \psi[a, x] $$
Ok now here are my thoughts:
We prove that for any $X \in L(\mathbb{R})$, $X$ is $^{\omega}\omega\text{-definable}$ in $L_{\alpha}(\mathbb{R})$ by induction, where $\alpha + 1$ is the first index in the hierarchy where $X$ appears.
The case $\alpha =0$ or the case for limit ordinals is immediate. Now suppose $X \in L_{\alpha + 1}(\mathbb{R})$. Then there exists a formula $\varphi$ and $t_1, \dots, t_n \in L_{\alpha}(\mathbb{R})$ s.t. $$x \in X \longleftrightarrow L_{\alpha}(\mathbb{R}) \models \varphi(x, t_1, \dots, t_n)$$ By the induction hypothesis there exist formulas $\tilde{\varphi}_1, \dots, \tilde{\varphi}_n$ and reals $a_1, \dots, a_n$ s.t. $$x \in t_i \longleftrightarrow L_{\alpha_{t_i}}(\mathbb{R}) \models \tilde{\varphi}_i[a_i, x]$$ Now using coding and replacing the respective formulas in $\varphi$, we arrive at a formula $\psi$ and a real $a$ s.t. $$x \in X \longleftrightarrow \psi(x, a, L_{\alpha}(\mathbb{R}), L_{\alpha_{t_1}}(\mathbb{R}), \dots, L_{\alpha_{t_n}}(\mathbb{R})).$$
Here is the assumption I was talking about, is it Ok and safe to assume that for all $\beta$, $L_{\beta}(\mathbb{R})$ is $^{\omega}On\text{-definable}$? If so, how can I prove it? If all I have written is incorrect, then how can I prove the main statement?
EDIT I: The $^{\omega}On\text{-definability}$ of $A$ in the main statement should be checked in $V[G]$, where $G$ is any generic filter on the Levy collapse of an inaccessible cardinal.
Note that your proof shows that $X$ is $^{\omega}On$-definable in $L(\mathbb R)$ (instead of in $L_\alpha(\mathbb R)$ as you claimed) - which is of course totally fine for what you want to do. The proof itself looks totally fine to me.
Now to your assumption: Yes, $L_\beta(\mathbb R)$ is $^{\omega}On$-definable. Even better: There is a definition of $L_\beta(\mathbb R)$ with only parameter $\beta$ that is uniform in $\beta$. This definition is just the usual definition of $L_\beta(\mathbb R)$: $$X=L_\beta(\mathbb R)\text{ iff there is a function } f \text{ with domain } \beta+1 \text{ so that } f(0)=tc(\{\mathbb R\}), \ \ \ \ \ \ \text{ for all successors } \alpha+1\leq\beta\ f(\alpha+1)=Def(f(\alpha)) \text{ and for all limit } \alpha\leq\beta\\\ f(\alpha)=\bigcup_{\gamma<\alpha} f(\gamma) \text{ and } X=f(\beta)$$ Where $Def(f(\alpha))$ is the definable powerset of $f(\alpha)$.
With your ideas, you can even improve your result and show that $L(\mathbb R)\models\ V=HOD_{\mathbb R}$, where $HOD_\mathbb R$ is the class of sets that are hereditarily definable from ordinals and reals as parameters.