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

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

-
Hint. Show that a family of nonempty open intervals in the line must be countable. –  GEdgar May 9 '11 at 21:34
@GEdgar: Thanks, but after a few days I'm still stuck. Not-quite-constructive proof: given a family of disjoint (you meant disjoint?) inhabited open intervals, map each interval to the set of rationals it contains. So the family is in bijection with a quotient of a subset of a countable set. By the law of the excluded middle, the subset of a countable set is countable. And then the quotient of a countable set is countable. I don't see the constructive proof. –  Unsecured sequence May 12 '11 at 20:42