Proof of Kondô-Addison theorem The proof of the (lightface) Kondô-Addison theorem (aka $\Pi^1_1$ uniformization) that I know goes like this: for a $\Pi^1_1$ set $R \subseteq 2^\omega \times 2^\omega$, define the uniformization of $R$ as follows.  By the Spector-Gandy theorem, there's a $\Sigma_0$ formula $\phi$ such that
$$
L_{\alpha}[x \oplus y] \models \exists u\phi(x, y, u).
$$
where $\alpha=\omega_1^{x\oplus y}$.
Then the uniformization $R_0$ is defined such that $(x,y) \in R_0$ iff


*

*$y \in L_{\alpha}[x]$;

*There's a $u$ in $L_{\alpha}[x]$ s.t. $L_{\alpha}[x] \models \phi(x, y, u)$; and

*$L_{\alpha}[x] \models \forall \hat u \forall \hat y[(u, y) <_{L[x]} (\hat u, \hat y) \rightarrow \neg\phi(x, \hat y, \hat u)]$, where $<_{L[x]}$ is a $\Delta_1$ wellordering of $L[x]$.


(Note the absence of $y$ in the brackets above.) The conjunction above is $\Sigma_1(L_\alpha[x\oplus y])$ (note the presence of $y$ in the bracket), so by Spector-Gandy again, $R_0$ is $\Pi^1_1$. (You need a lemma of Guaspari's to fill the last gap: if $R$'s fiber at $x$ is nonempty then so is $R_0$'s fiber at $x$.)
My question is the reason for the use of $L_\alpha[x]$ in the proof.  Why not appeal to the $\Delta_1$ wellordering directly in $L_\alpha[x \oplus y]$?  I suppose that the reason is to reduce the complexity of the definition to at most $\Sigma_1(L_\alpha[x\oplus y])$, since there are unbounded quantifier to the right of $\models$.  If so, however, I do not understand why the detour via $L_\alpha[x]$ reduces the complexity; I imagine that one has to attach the $\Sigma_1$ definition of $L[x]$ inside $L_\alpha[x\oplus y]$ to every quantifier, and that seems to increase the complexity above $\Sigma_1$.
 A: First, you should note that the Spector-Gandy theorem states that every lightface $\Pi_1^1$ relation $R$ takes the form $R(x) \Leftrightarrow (\exists y \in \text{HYP})(A(y,x))$ where $A$ is arithmetic. It is important to note that the existential quantifier is over hyperarithmetic reals. This shows that you can find a witness y and u in $L_\alpha[x]$ to satisfy your condition (1), (2), and (3). 
Also when you write condition 1, 2, and 3, it is not clear what is $\alpha$ since you are ranging it over $(x,y)$. I think the following writing of 1, 2, and 3 should also work: $(x,y) \in R_0$ if and only if
(1) $y \in L_{\omega_1^x}(x) = HYP(x)$
(2) There exists $u \in L_{\omega_1^x}[x]$ so that $L_{\omega_1^x} \models  \Phi(x,y,u)$
(3) $(u,y)$ is $L[x]$-least solution in $L_{\omega_1^x}(x)$. 

Again a solution $u$ and $y$ can be found in $L_{\omega_1^x}(x)$ since $R(x,\cdot)$ is a $\Pi_1^1(x)$ relation and using Gandy-Spector again. 

It seems more natural to use $L[x]$ then $L[x,y]$. Remember what uniformization is is asking for: You have a binary relation $R(x,y)$. You want to find a subset which is a function. That is, for each $x$, you want to (in a $\Pi_1^1$ way) pick a $y$ so that $R(x,y)$. It seems natural that you would just go into $L_{\omega_1}(x)$, and choose the least solution $y$ corresponding to $x$.
Anyway suppose you did it using $L[x,y]$. Suppose there were two $y_1,y_2$ satisfying (1) and (2). If you use the well ordering of $L[x,y_1]$ and $L[x,y_2]$ in (3), I can not see how (3) would tell you how to pick between $y_1$ or $y_2$? If you use the well ordering $L[x,y]$ in (3), can you prove for every $x$ there is only one $y$ so that $R_0(x,y)$?
