I'm trying to read Kreisel's paper "Analysis of the Cantor-Bendixson Theorem by Means of the Analytic Hierarchy" 1959.
From what is written in the paper, I'm missing something simple. Here is the fragment (in italic) I'm struggling with.
THEOREM $0$. If $F$ is in $\Pi^1_1$, then $F_p$ is in $\Sigma^1_2$.
For $(a,b) \in G_p \equiv F \cap (a,b)$ is enumerable, i.e. there is a sequence $\xi_n$ of real numbers such that for all real numbers $\eta$, $$\eta \notin (a,b) \vee \eta \notin F \vee \exists n (\eta = \xi_n).$$ If $F$ is in $\Pi^1_1$, the function quantifier in $\eta \notin F$ can be absorbed, and so the set of $(a,b)$ for which $F \cap (a,b)$ is enumerable, is in $\Sigma^1_2$.
Some conventions from the earlier part of the paper:
- $F$ is a closed set of reals from the unit interval $[0,1]$,
- $F_p$ is its perfect kernel,
- $G_p$ is the complement of $F_p$ with respect to $[0,1]$,
- $(a,b)$ is an open interval with rational endpoints $a,b$.
Now, given that $F$ is $\Pi^1_1$, i.e. $F(\eta) \equiv \forall \zeta \exists n R(\eta, \zeta,n)$, for some recursive relation $R$, how one can absorb the function quantifier in $\eta \notin F$? As I see it, we express the fact that $F \cap (a,b)$ is countable by the following formula (by coding $\xi_n$ as the $n$-th column of $\xi$): $$\exists \xi \forall \eta [\eta \notin (a,b) \vee \eta \notin F \vee \exists n (\eta = \xi_n)],$$ so we have (assuming the above definition of $F$) $$\exists \xi \forall \eta [\eta \notin (a,b) \vee \exists \zeta \forall n \neg R(\eta, \zeta,n) \vee \exists n (\eta = \xi_n)]$$
It is clear that we have $\Sigma^1_3$ definition, but how this absorption works? I was trying applying some prefix transformations to obtain a simple predicate form but with no success.