nLab
Specker sequence

Specker sequences

Definition

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

Examples

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.

Revised on November 5, 2012 23:53:48 by Toby Bartels (64.89.58.121)