So I am studying the chapter "$\Pi^1_1$ Sets and $\Sigma^1_2$ Sets" from "The Higher Infinite" and I got stuck when trying to come up with a definition for the desired function below.
Some definitions:
Def $1$. For each $x \in {^\omega\omega}$, let $E_x$ be the binary relation on $\omega$ as below: $$ (m, n) \in E_x \longleftrightarrow x(\langle m, n \rangle) = 0,$$ where $\langle m, n \rangle$ is the code for the tuple $(m, n)$. And now let, $$\text{WF} = \{x \in {^\omega\omega} \mid E_x \text{ is well-founded}\}.$$ Def 2. Fix an enumeration of ${^{<\omega}\omega}$, and for each $i \in \omega$, let $S_i$ be a $\Delta^0_0$ decoding of the sequence of members of ${^{<\omega}\omega}$.
Def 3. We say that $T$ is a tree on ${^k\omega} \times \omega$ iff $T \subseteq \bigcup_{m \in \omega} {^k(^m\omega)} \times {^m\omega}$ and for each $(t_0, \dots, t_k) \in T$ and $m \in \omega$ we have that $(t_0|m, \dots, t_k|m) \in T$.
And for $w = (x_0, \dots x_{l-1}) \in {^l(^\omega\omega)}$, $l \leq k$, $T_w$ is that tree on ${^{k-l}\omega} \times \omega$ defined by, $$(t_0, \dots t_{k-l}) \in T_w \longleftrightarrow \exists m( (x_0|m, \dots, x_{l-1}|m, t_0, \dots t_{k-l}) \in T).$$ Also we say that a tree $T$ is well-founded iff it is well-founded with respect to $^*{\supset}$, Where $^*{\supset}$ is point-wise reverse inclusion.
A useful Theorem that we are going to quote:
Th(*). Let $a \in {^\omega\omega}$ and $A \subseteq {^k({^\omega\omega})}$. Then $A$ is $\Pi^1_1(a)$ iff there is a tree $T$ on ${^k\omega} \times \omega$ such that for any $w \in {^k(^\omega\omega)}$, $$A(w) \longleftrightarrow T_w \text{ is well-founded ,}$$ and the relation $\{(i, w) \mid S_i \in T_w\}$ is recursive in $a$.
The part of the book, which I have a problem with:
By (*), for any $\Pi^1_1(a)$ set $A \subseteq {^k(^\omega\omega)}$ there is a function $f:{^k(^\omega\omega)} \rightarrow {^\omega\omega}$ (whose graph is) recursive in $a$ such that $A = f^{-1}(\text{WF})$.
My thoughts:
By (*) we have a tree $T$ for $A$. And going with intuition I think I must construct $f$ in such a way that for each $w$, $f$ codes $T_w$ so that when $w$ is in $A$ we know that $T_w$ is well-founded and the real coding it should be in $\text{WF}$. I have tried writing such $f$ but I can't handle the complexity (by complexity here I mean the complexity of the graph of $f$, which should be recursive in $a$). Anything I have written down was at best $\Pi^0_2$.
Sorry for the long post.