There is a proof in the Ash/Knight book "Computable Structures and the Hyperarithmetical Hierarchy" Theorem 5.19 that states that if $Q$ is a $\Pi^1_1$-relation then $Q$ has a $\Pi^1_1$-(skolem) choice function $F$. See below:
For reference: $O$ -is Kleene's O, and $E^1_{\Sigma}$ kleene's $\Sigma^1_1$ enumeration relation.
Theorem 5.19: Let $Q$ be a $\Pi^1_1$ binary relation. Then there is a $\Pi^1_1$ function $F$ such that $F \subseteq Q$ and $\forall x [\exists y Q(x,y) \rightarrow Q(x,F(x))]$
Proof. Say $Q \leq_m O$ via $g$. For each $x$ we define $F(x)=y$ so that the ordinal $|g(x,y)|_O=\beta$ is as small as possible, and $y$ is the least such that $|g(x,y)|_O=\beta$. By earlier theorems, there is a partial computable function $h$ such that for $u \in O$, $h(u)$ is a $\Sigma^1_1$ index for $\{v \in O : |v|_O \leq |u|_O \}$. Let $F(x)=y$ if and only if
(1) $Q(x,y)$
(2) $\forall z [ Q(x,z) \rightarrow E^1_{\Sigma}(h(g(x,z)), g(x,y)]$ $ \ $ (ensures $|g(x,y)|_O=\beta$ is as small as possible)
(3) $\forall z [ Q(x,z) \wedge E^1_{\Sigma}(h(g(x,y)),g(x,z))\rightarrow y \leq z )]$ $ \ $(ensures that $y$ is the least such that $|g(x,y)|=\beta$.)
It is clear from the definition that $F$ has all the desired properties. (END PROOF)
Here is how I see it:
- Clearly this relation is $\Pi^1_1$ by definition.
- Looking inside the brackets we have $[\neg Q(x,z) \vee E^1_{\Sigma}(h(g(x,z)),g(x,y)]$. Since $Q$ is $\Pi^1_1$ then $\neg Q$ is $\Sigma^1_1$, and since $E^1_{\Sigma}$ is $\Sigma^1_1$ whats inside the brackets is $\Sigma^1_1$. Since $\forall z$ quantifies over natural numbers and not a function, thus the stipulation in (2) is $\Sigma^1_1$
Right away, since (1) is $\Pi^1_1$ and (2) is $\Sigma^1_1$ if they are satisfied together, this makes $F$ at least $\Delta^1_2$. What am I getting wrong?