Specker sequence

A recursive, monotone, bounded sequence of rational numbers that is not a Cauchy sequence in the constructive (algorithmic) sense.The first example of such a sequence was mentioned by E. Specker [1]. More precisely, for a Specker sequence $\alpha$ there does not exist a general recursive function $\beta$ such that for any $i, j, n$ for which $i, j \ge \beta(n)$, the following inequality holds:\[|\alpha(i) - \alpha(j)| < \frac{1}{2^n}.\]The existence of a Specker sequence is fundamental both in constructive mathematics and traditional mathematical analysis. Since a Specker sequence does not converge to any constructive (computable) real number and it is impossible to select from it subsequences with such a property, it can be considered as a counterexample that contradicts, in the context of the most natural algorithmic conception of a constructive continuum, such fundamental principles as the Weierstrass theorem on the existence of a limit for a bounded monotone sequence, the Bolzano–Weierstrass theorem on the choice of a converging subsequence, and the theorem on the existence of exact bounds of bounded sets of numbers. From the point of view of traditional mathematics, Specker's result shows that the objects whose existence is asserted by the above-mentioned theorems may have a rather complex nature, even though the initial situations are very simple. Specker's theorem can be considered as a first essential step in the study of the computational and the descriptive complexity of these objects.See also Constructive mathematics; Constructive analysis.====References====

[1]	E. Specker, "Nicht konstruktiv beweisbare Sätze der Analysis" J. Symbol. Logic , 14 (1949) pp. 145–158
[2]	B.A. Kushner, "Lectures on constructive mathematical analysis" , Amer. Math. Soc. (1984) (Translated from Russian)

====Comments========References====

[a1]	C. Calude, "Theories of computational complexity" , North-Holland (1988)
[a2]	H. Hermes, "Aufzählbarkeit, Entscheidbarkeit, Berechenbarkeit" , Springer (1978)