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

  • 2
    $\begingroup$ Looking at the complexity of "$B$ is a branch through the tree $T \subseteq \mathbb{N}^{\lt\infty}$," if $\mathcal{M}$ is an $\omega$-model of $\mathsf{ACA}_0$ and every nonempty $\Pi^0_2$-class coded in $\mathcal{M}$ has an element in $\mathcal{M}$, then $\mathcal{M}$ is a $\beta$-model. So what you want are exactly the $\beta$-models of $\Pi^1_1$-$\mathsf{CA}_0$. No? $\endgroup$ Jan 16, 2013 at 6:38
  • $\begingroup$ . . . Huh, I completely failed to notice that, simple as it is. Could you submit this as an answer so I can accept it? Thanks! $\endgroup$ Jan 16, 2013 at 18:19

1 Answer 1


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.