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 as
where is the bit ( or ) giving whether the th Turing machine halts before steps. The theoretical limit of this sequence is
where is the bit giving whether the th 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? ().
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 is equivalent to excluded middle.
Revised on November 5, 2012 23:53:48
by Toby Bartels