How should the relativized Kleene pointclass $\Sigma^1_1(A)$ be defined, when $A$ is a set of reals ($A \subset \omega^\omega$)? I assume that there is a standard definition, but I can't seem to find it in print.
I asked a question at mathoverflow about this pointclass, and then realized that I didn't know what I was talking about. Here is the definition I attempted to give there:
A $\Sigma^1_1(A)$ set is a set definable by a $\Sigma^1_1(A)$ formula, which is like a $\Sigma^1_1$ formula except that the language is expanded by a predicate symbol for $A$.
We define the class of $\Delta^0_1(A)$ formulas recursively by starting with atomic formulas (now including the formula $A(x)$) and applying $\neg$, $\wedge$, $\vee$, $\forall^\omega$, and $\exists^\omega$. Then the $\Sigma^1_1(A)$ formulas are obtained by adding blocks of real existential quantifiers $\exists^{\omega^\omega} x_1 \cdots \exists^{\omega^\omega} x_n$ in front of $\Delta^0_1(A)$ formulas.
However, I don't think this is the right definition. For example, I think that if $A$ is a binary relation on the reals then the statement "$A$ is ill-founded" should be $\Sigma^1_1(A)$, but the definition above doesn't seem to allow asking about membership of countably many ordered pairs of reals (as coded by a single real) in $A$. Also, it's not clear to me that the pointclass defined above is closed under recursive substitution.