Specker sequence

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).

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, since LUPLUP is equivalent to excluded middle.

Last revised on November 5, 2012 at 23:53:48. See the history of this page for a list of all contributions to it.