# 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 $\left({S}_{n}{\right)}_{n}$ as

${S}_{n}=\sum _{i+j=n}{2}^{-i}\left\{i{\right\}}_{j},$S_n = \sum_{i + j = n} 2^{-i} \{i\}_j ,

where $\left\{i{\right\}}_{j}$ is the bit ($0$ or $1$) giving whether the $i$th Turing machine halts before $j$ steps. The theoretical limit of this sequence is

$\sum _{i}{2}^{-i}\left\{i\right\},$\sum_i 2^{-i} \{i\} ,

where $\left\{i\right\}$ is the bit giving whether the $i$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? ($\mathrm{LUP}$).

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 $\mathrm{LUP}$ is equivalent to excluded middle.

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