nLab Specker sequence

Specker sequences

Specker sequences


A Specker sequence is a bounded computable increasing infinite sequence of rational numbers with no computable supremum.


Since there is a sequence of all Turing machines, define a sequence (S n) n(S_n)_n as

S n= i+j=n2 i{i} j, S_n = \sum_{i + j = n} 2^{-i} \{i\}_j ,

where {i} j\{i\}_j is the bit (00 or 11) giving whether the iith Turing machine halts before jj steps. The theoretical limit of this sequence is

i2 i{i}, \sum_i 2^{-i} \{i\} ,

where {i}\{i\} is the bit giving whether the iith Turing machine halts at all, but this is uncomputable (on pain of solving the halting problem).

Many famous non-computable numbers may be expressed as limits of Specker sequences. For example, a Chaitin constant? is defined as the sum of an infinite series with non-negative computable terms (each of which is a dyadic rational), and so is the limit of a Specker sequence.

In constructive mathematics

In Russian constructivism, all real numbers are computable, so a Specker sequence has no (located) supremum, giving a counterexample to the classical least upper bound principle? (LUPLUP).

In many other varieties of constructive mathematics, the computability of all real numbers can be neither proved nor refuted, but Specker sequences still provide weak counterexamples.

For a non-computable number that can be expressed as the limit of a Specker sequence, the sequence itself is a way to work with the number in constructive mathematics without assuming that it exists as a real number. (This amounts to treating it as a computable lower real number.)

Last revised on September 20, 2020 at 00:22:57. See the history of this page for a list of all contributions to it.