Suslin–Kleene theorem

In effective descriptive set theory, the Suslin–Kleene theoremTemplate:R characterizes the hyperarithmetic subsets of $\mathbb{N}$. Informally, it states that the hyperarithmetic, i.e., lightface ${\mathrm{\Delta }}_1^1$ subsets of $\mathbb{N}$ form the “effective” σ-algebra “effectively” generated by the singletons. This is an effective analog of Suslin's theorem, which states that the subsets of a Polish space which are boldface ${𝜟}_1^1$, i.e., both analytic and co-analytic, are exactly the Borel subsets, which form the σ-algebra generated by open subsets.

Statement

Let $X$ be a set. A modest assembly structure on $X$ is a function which maps every $x\in X$ to a non-empty subset $E(x)\subseteq \mathbb{N}$, whose elements are called the realizers of $x$, such that different elements do not share realizers: $E(x)$ and $E(y)$ are disjoint for $x\ne y$. The realizers of $x$ are intuitively understood as concrete computational representations of the abstract element $x$.

The Suslin–Kleene theorem states that the class of hyperarithmetic subsets of $\mathbb{N}$ is the least $\mathrm{\Gamma }\subseteq 𝒫(\mathbb{N})$ such that there exists a modest assembly structure on $\mathrm{\Gamma }$ for which the following conditions are satisfied:

1. For all $n\in \mathbb{N}$, the singleton $\{n\}$ belongs to $\mathrm{\Gamma }$. Moreover, there exists a (total) computable function $S:\mathbb{N}\to \mathbb{N}$ such that $S(n)$ realizes $\{n\}$ for all $n$.
2. For all $P\in \mathrm{\Gamma }$, the complement $P^c$ belongs to $\mathrm{\Gamma }$. Moreover, there exists a computable function $C:\mathbb{N}\to \mathbb{N}$ such that $C(n)$ realizes $P^c$ for all $P\in \mathrm{\Gamma }$ and for all $n\in \mathbb{N}$ realizing $P$.
3. For all sequence of subsets $P_n\in \mathrm{\Gamma }$, if there exists a computable function $r:\mathbb{N}\to \mathbb{N}$ such that $r(n)$ realizes $P_n$ for all $n$, then the union $\bigcup _{n\in \mathbb{N}}{P}_n$ belongs to $\mathrm{\Gamma }$. Moreover, there exists a computable function $U$ such that $U(e)$ realizes $\bigcup _{n\in \mathbb{N}}{P}_n$ for all sequence $P_n\in \mathrm{\Gamma }$ and for all $e\in \mathbb{N}$ such that ${\varphi }_e(n)$ is defined and realizes $P_n$ for all $n$.