Some Additional Results

In this section we present some additional results and open questions.

Lemma 4.1   Let $\varphi(X)$ be a $\Sigma^1_1$ formula with no free set variables other than X. The following is provable in $\mathsf{ATR}_0$. If $\exists X\,(X\notin\mathrm{HYP}$ and $\varphi(X))$, then $\exists P\,(P$ is a perfect tree and $\forall X\,($if X is a path through P then $\varphi(X)))$.

Proof.This is a well known consequence of formalizing the Perfect Set Theorem within $\mathsf{ATR}_0$. See Simpson [5, §§V.4 and VIII.3]. See also Sacks [4, §III.6].$\Box$

Lemma 4.2   Let $\varphi(X)$ be a $\Sigma^1_2$ formula with no free set variables other than X. The following is provable in $\mathsf{ATR}_0\,+{}$ ``all ordinals are recursive''. If $\exists X\,(X\notin\mathrm{HYP}$ and $\varphi(X))$, then $\exists P\,(P$ is a perfect tree and $\forall X\,($if X is a path through P then $\varphi(X)))$.

Proof.Since $\varphi(X)$ is $\Sigma^1_2$, we can write $\varphi(X)\equiv\exists Y\,\forall f\,\exists n\,R(X[n],Y[n],f[n])$ where R is a primitive recursive predicate. Let T_X,Y be the tree consisting of all $\tau$ such that $\lnot\,(\exists n\le\mathrm{lh}(\tau))\,R(X[n],Y[n],\tau[n])$. For $\alpha<\omega_1^{\mathrm{CK}}$ put

$\varphi_\alpha(X)\,\,\equiv\,\,\exists Y\,(T_{X,Y}$ is well founded of height $\le\alpha)$.

Note that, for each $\alpha<\omega_1^{\mathrm{CK}}$, $\varphi_\alpha(X)$ is $\Sigma^1_1$. Reasoning in $\mathsf{ATR}_0\,+{}$ ``all ordinals are recursive'', we have $\forall X\,(\varphi(X)$ if and only if $(\exists\alpha<\omega_1^{\mathrm{CK}})\,\varphi_\alpha(X))$. Thus Lemma 4.2 follows easily from Lemma 4.1.$\Box$

Theorem 4.3   Let T be $\mathsf{ATR}_0$ or $\Pi^1_\infty$- $\mathsf{TI}_0$. Let $\varphi(X)$ be a $\Sigma^1_2$ formula with no free set variables other than X. If $T\vdash\exists X\,(X\notin\mathrm{HYP}$ and $\varphi(X))$, then $T\vdash\exists P\,(P$ is a perfect tree and $\forall X\,($if X is a path through P then $\varphi(X)))$.

Proof.From Friedman [1] or Simpson [5, §VII.2], we have that $T\vdash$ the disjunction (1) all ordinals are recursive, or (2) there exists a countable coded $\beta$-model M satisfying $T\,+{}$ ``all ordinals are recursive''. In case (1), the desired conclusion follows from Lemma 4.2. In case (2), we have $M\models\exists X\,(X\notin\mathrm{HYP}$ and $\varphi(X))$, so the proof of Lemma 4.2 within M gives $\alpha<\omega_1^{\mathrm{CK}}$ such that $M\models\exists X\,(X\notin\mathrm{HYP}$ and $\varphi_\alpha(X))$. It follows that $\exists X\,(X\notin\mathrm{HYP}$ and $\varphi_\alpha(X))$. We can then apply Lemma 4.1 to $\varphi_\alpha(X)$ to obtain the desired conclusion.$\Box$

Corollary 4.4   Let T and $\varphi(X)$ be as in Theorem 4.3. If $T\vdash\exists X\,(X\notin\mathrm{HYP}$ and $\varphi(X))$, then $T\vdash\forall Y\,\exists X\,(\varphi(X)$ and $\forall n\,(X\ne(Y)_n))$.

Proof.This follows easily from Theorem 4.3.$\Box$

Theorem 4.5   Let T and $\varphi(X)$ be as in Theorem 4.3. If $T\vdash(\exists$ exactly one $X)\,\varphi(X)$, then $T\vdash\exists X\,(X\in\mathrm{HYP}$ and $\varphi(X))$.

Proof.Consider cases (1) and (2) as in the proof of Theorem 4.3. In both cases it suffices to show that, for all $\alpha<\omega_1^{\mathrm{CK}}$, if $(\exists$ exactly one $X)\,\varphi_\alpha(X)$ then $\exists X\,(X\in\mathrm{HYP}$ and $\varphi_\alpha(X))$. This follows from Lemma 4.1 applied to $\varphi_\alpha(X)$.$\Box$

Remark 4.6   Theorems 4.3 and 4.5 appear to be new. Corollary 4.4 has been stated without proof by Friedman [3, Theorems 3.4 and 4.4]. A recursion-theoretic analog of Corollary 4.4 has been stated without proof by Friedman [3, Theorem 1.7], but this statement of Friedman is known to be false, in view of Simpson [6]. A recursion-theoretic analog of Theorem 4.5 has been proved by Simpson/Tanaka/Yamazaki [7].

Question 4.7   Suppose $\mathsf{WKL}_0\vdash\exists X\,(X\notin\mathrm{REC}$ and $\varphi(X))$ where $\varphi(X)$ is $\Sigma^1_1$, or even arithmetical, with no free set variables other than X. Does it follow that $\mathsf{WKL}_0\vdash\exists X\,\exists Y\,(X\ne Y\land\varphi(X)\land\varphi(Y))$? A similar question has been asked by Friedman [2, unpublished].

Question 4.8   Suppose $\mathsf{WKL}_0\vdash(\exists$ exactly one $X)\,\varphi(X)$ where $\varphi(X)$ is $\Sigma^1_1$ with no free set variables other than X. Does it follow that $\mathsf{WKL}_0\vdash\exists X\,(X\in\mathrm{REC}$ and $\varphi(X))$? If $\varphi(X)$ is arithmetical or $\Pi^1_1$ then the answer is yes, by Simpson/Tanaka/Yamazaki [7].