This question is an outgrowth of this MathSE question: <https://math.stackexchange.com/questions/276068/members-of-lightface-borel-sets>. 


A **Borel set** $X\subseteq 2^\omega$ is a member of the smallest collection of subsets of $2^\omega$ closed under complementation and countable union. As such, Borel sets come with "codes:" well-founded, potentially infinitely-branching subtrees of $\omega^{<\omega}$ interpreted as instructions for how to combine the basic open sets corresponding to the "leaves" to form the desired Borel set. Such a subtree is codeable by a set of natural numbers, so we can talk about the Turing degree of a code for a Borel subset of $2^\omega$. A Borel set $X$ is *lightface Borel* if it has a computable Borel code. More usefully, the class of Borel sets is naturally stratified into $\omega\_1$ many pairs of levels, with open and closed sets forming the bottom pair of levels, ${\Sigma^0\_1}$ and ${\Pi^0\_1}$, respectively. There are notions of codes for, and analogous lightface versions of, each of the levels ${\Sigma^0\_\alpha}$ and ${\Pi^0\_\alpha}$ (for $\alpha$ a computable ordinal, anyways).


According to the Low Basis Theorem, every nonempty lightface $\Pi^0\_1$ subset of $2^\omega$ has a low member. Trying to push this up the Borel hierarchy leads to problems: already at the level of $\Pi^0\_2$, there are computable codes for sets with no hyperarithmetic members. We still have a basis theorem, though: each nonempty lightface $\Pi^0\_\alpha$ subset of $2^\omega$ has a member computable in Kleene's $\mathcal{O}$.


But in the case of lightface $\Pi^0\_1$ sets, we have - in addition to the Low Basis Theorem - a "proof-theoretic" basis theorem: if $\mathcal{M}$ is an $\omega$-model of $WKL\_0$ (a particular subsystem of second-order arithmetic), then every nonempty $\Pi^0\_1$ subset of $2^\omega$ which has a code in $\mathcal{M}$ has a member in $\mathcal{M}$ (and the converse holds: if $\mathcal{M}$ has this property, and is an $\omega$-model of $RCA\_0$, then $\mathcal{M}\models WKL\_0$).


Trying to get an analogous proof-theoretic basis theorem for higher levels of the Borel hierarchy, one might want to close under hyperjump (the map $h: X\mapsto \mathcal{O}^X$); the relevant subtheory would seem to be $\Pi^1\_1-CA\_0$. However, it turns out that an $\omega$-model $\mathcal{N}$ of $RCA\_0$ is closed under the hyperjump iff it is a model of $\Pi^1\_1-CA\_0$ and is also a *$\beta$-model*, that is, everything $\mathcal{N}$ thinks is a well-order is actually a well-order; and this latter condition cannot be phrased in a first-order manner. What I want to know is whether we can in any way remove the need to restrict attention to $\beta$-models.


My question is the following: for which $n\in\omega$ is there a first-order theory $T\_n$, in the language of second-order arithmetic (and consisting only of true sentences, to avoid trivialities), such that whenever $\mathcal{M}\models T\_n$, $\mathcal{M}$ is an $\omega$-model, and $X\subseteq 2^\omega$ is a nonempty $\Pi^0\_n$ set with a code in $\mathcal{M}$, $X$ has a member in $\mathcal{M}$?


(Note: it's perfectly reasonable that there should be no such $T\_n$ for $n$ sufficiently large - even $n=2$ - since we're already sort of cheating at the level $n=1$ by restricting attention to $\omega$-models, which is again not a first-order thing. We need to, on the face of it, in order to make the question make much sense, but there's still a sense in which non-first-order-ness has already snuck in. My suspicion is in fact that for $n>1$ there is no such $T\_n$, but I don't know how to show that.)



Ensuring nonempty lightface Borel sets have elements via theories of second-order arithmetic
Given a tree $T \subseteq \omega^{\lt\omega}$, the statement "$B$ is an infinite path through $T$" is $\Pi^0\_2$. Therefore, if $\mathcal{M}$ is such that every nonempty $\Pi^0\_2$-class coded in $\mathcal{M}$ has a point in $\mathcal{M}$, then $\mathcal{M}$ is necessarily a $\beta$-model. So the models you want are precisely the $\beta$-models of $\Pi^1\_1$-$\mathsf{CA}\_0$.


