Specker Sequence - Construction

Construction

The following construction is described by Kushner (1984). Let A be any recursively enumerable set of natural numbers that is not decidable, and let (a_i) be a computable enumeration of A without repetition. Define a sequence (q_n) of rational numbers with the rule

It is clear that each q_n is nonnegative and rational, and that the sequence q_n is strictly increasing. Moreover, because a_i has no repetition, it is possible to estimate each q_n against the series

Thus the sequence (q_n) is bounded above by 1. Classically, this means that q_n has a supremum x.

It is shown that x is not a computable real number. The proof uses a particular fact about computable real numbers. If x were computable then there would be a computable function r(n) such that |q_j - q_i| < 1/n for all i,j > r(n). To compute r, compare the binary expansion of x with the binary expansion of q_i for larger and larger values of i. The definition of q_i causes a single binary digit to go from 0 to 1 each time i increases by 1. Thus there will be some n where a large enough initial segment of x has already been determined by q_n that no additional binary digits in that segment could ever be turned on, which leads to an estimate on the distance between q_i and q_j for i,j > n.

If any such a function r were computable, it would lead to a decision procedure for A, as follows. Given an input k, compute r(2k+1). Note that if k were to appear in the sequence (a_i), this would cause the sequence (q_i) to increase by 2-k-1, but this cannot happen once all the elements of (q_i) are within 2-k-1 of each other. Thus, if k is going to be enumerated into a_i, it must be enumerated for a value of i less than r(2k+1). This leaves a finite number of possible places where k could be enumerated. To complete the decision procedure, check these in an effective manner and the return 0 or 1 depending on whether k is found.