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.)
