# Uncountable closed set of reals biject with reals without replacement or choice

I recently gave a proof of this theorem:

Every uncountable closed set of reals is in bijection with the reals.

My proof used the axiom of countable choice. Asaf Karagila stated in a comment that Arnie Miller showed in "A Dedekind Finite Borel Set" (Arch. Math. Logic 50, No. 1-2, 1-17 (2011); or on arXiv), that we do not need choice to get perfect subsets of uncountable Borel sets, provided that they can be written as a countable union of $G_δ$ sets, and so the theorem can be proven without choice. But it appears that this proof requires the use of the replacement schema.

So my question is:

Is there a proof of that theorem in Z, namely without replacement or choice? (Z does not have the foundation axiom either, but that seems irrelevant to this theorem.)

If the answer is yes, of course the proof would be interesting.

If the answer is no, it would be equally interesting, as an example of a theorem that can be proven in Z+CC or Z+R despite CC and R both being independent of each other over Z, and apparently unrelated. Also, if the answer is no, I have a follow up question:

Is there a proof of that theorem in Z plus replacement on $ω$? (Namely that the image of any definable function on $ω$ is a set.)

• I would imagine that the answer is positive. But currently too busy/lazy to verify that. – Asaf Karagila Dec 1 '17 at 19:18
• @AsafKaragila Which is it busy or lazy ? It cant be both. – Rene Schipperus Dec 1 '17 at 19:28
• Does your proof work for compact sets? If so, maybe you can transport your closed set along a bijection of $\mathbb R$ with $(0,1),$ add $0$ and $1,$ then you get a compact set. – Dap Dec 1 '17 at 19:35
• @Rene: I can do both. I'm very skilled at the art of doing and not doing things. – Asaf Karagila Dec 1 '17 at 19:39
• @Dap There are 2 usages of countable choice in the argument. The first is easily avoidable as you suggest. The second is the essential use (and it is invoked repeatedly in a recursive construction) and removing it is not so clear. – Andrés E. Caicedo Dec 1 '17 at 21:48

Here is a partial answer. It cannot be proved by $KP$.

Let $M=L_{\omega_1^{CK}}$, where $\omega_1^{CK}$ is the least nonrecursive ordinal. Fix a recursive binary tree $T$ so that

(1) For any $\alpha<\omega_1^{CK}$, $0^{(\omega\cdot \alpha)}$, the $\omega\cdot\alpha$-th $\Sigma_1$-master code, belongs to $[T]$; and

(2) $[T]\cap M$ only contains those $\omega\cdot \alpha$-master codes; and

(3) $[T]$ is uncountable.

$T$ can be obtained by an effective transfinite recursion through a nonstandard ordinal.

Then in $M$, $T$ is uncountable due to (1).

Now suppose there is a bijection $f:[T]\to 2^{\omega}$ in $M$. Assume that $f\in L_{\alpha}$ for some $\alpha<\omega_1^{CK}$. Let $x\equiv_T 0^{(\beta+1)}$ for some $\beta>\alpha$ in $M$ which is not in $f(L_{\alpha}\cap [T])$ (such $x$ exists due to the admissibility of $M$). Then $f^{-1}(x)\in L_{\beta+1}$. Moreover, by the assumption, $f^{-1}(x)$ is the $\gamma$-th master code for some $\gamma>\alpha$ not greater than $\beta+1$. So $x$ must belong to $L_{\gamma}$ and so $\beta+1\leq \gamma$. In other words, $\gamma=\beta+1$, a contradiction to (2).

• Thanks a lot for your answer! I will read through it and get back to you. =) – user21820 Feb 15 '18 at 5:15
• I'm sorry to say I can't understand your answer, as I lack the necessary background in set theory. If you have a reference for the basics, I would appreciate. Thanks! – user21820 Feb 16 '18 at 15:29
• Sacks "higher recursion" or Chong and Yu's "recursion theory" – 喻 良 Feb 17 '18 at 15:19
• Thank you! I'll look them up. By the way, your answer is showing that KP (some weak fragment of ZF) is insufficient to prove the theorem, right? I don't think I had any essential use of power-set in my proof, so it can be done in KP+CC, right? So if Asaf is correct that it can be done in Z, it must be by a proof that crucially uses the power-set axiom? – user21820 Feb 17 '18 at 16:34
• It may use comprehension in an essential way. – 喻 良 Feb 18 '18 at 0:38