logoalt Hacker News

cofunctoryesterday at 7:28 PM0 repliesview on HN

Here’s a nice concrete construction. To start, fix some enumeration ϕ of Turing machines. Let’s define a sequence of rational numbers x_k as $\sum_{i=0}^k 2^{-(i+1)} * halts(ϕ(i),k)$, where $halts(M,k)$ returns 1 if the machine M halts before taking k steps when fed the empty tape, and 0 otherwise. This is perfectly computable, as we only ever need to run a finite number of machines a finite number of steps for each k.

This sequence of rationals is monotonic and is upper-bounded by 1, but does not have a computable least upper bound. If such an upper bound existed, then it would encode solutions to the halting problem for every program. However, the reals have least upper bounds of all upper bounded subsets under mild classical assumptions, so we’ve made ourselves an uncomputable real out of computable data.

Sequences of this form are called Specker sequences, and are how you cook up most uncomputable numbers. There are models of constructive logic that do not admit any Specker sequences and admit only computable reals, but that is beyond the scope of a single comment :)