Computable increasing function from $\omega_1^{CK} \to \mathbb{R}$

258 Views Asked by At

If $f:\omega_1 \to [0,1]$ such that $f(0)=0$ and such that $f(\alpha)<1$ and $\alpha<\beta$ imply $f(\alpha)<f(\beta)$ then there is a $\gamma$ such that $f(\gamma)=1$. Non-constructive proof: suppose not, then we have an increasing sequence of type $\omega_1$ in the reals; impossible.

I cannot find a constructive proof or computable counterexample. Is there a computable partial function defined on Kleene's $\mathcal{O}$ and such that $\alpha <_{\mathcal{O}} \beta$ implies $f(\alpha) <_{\mathbb{R}} f(\beta)$? Or is there a way to compute from $f$ a fundamental sequence for some (not necessarily the least) such $\gamma$?