Specker sequence

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

${\displaystyle q_{n}=\sum _{i=0}^{n}2^{-a_{i}-1}.}$ 

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

${\displaystyle \sum _{i=0}^{\infty }2^{-i-1}=1.}$ 

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(2^k+1). 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(2^k+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 then return 0 or 1 depending on whether k is found.

• Computation in the limit

• Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics, Oxford, 1987.
• B.A. Kushner (1984), Lectures on constructive mathematical analysis, American Mathematical Society, Translations of Mathematical Monographs v. 60.
• Jakob G. Simonsen (2005), "Specker sequences revisited", Mathematical Logic Quarterly, v. 51, pp. 532–540. doi:10.1002/malq.200410048
• S. Simpson (1999), Subsystems of second-order arithmetic, Springer.
• E. Specker (1949), "Nicht konstruktiv beweisbare Sätze der Analysis" Journal of Symbolic Logic, v. 14, pp. 145–158.