View source for Specker sequence

A recursive, monotone, bounded sequence of rational numbers that is not a [[Cauchy sequence|Cauchy sequence]] in the constructive (algorithmic) sense.

The first example of such a sequence was mentioned by E. Specker [[#References|[1]]]. More precisely, for a Specker sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086320/s0863201.png" /> there does not exist a [[General recursive function|general recursive function]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086320/s0863202.png" /> such that for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086320/s0863203.png" /> for which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086320/s0863204.png" />, the following inequality holds:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s086/s086320/s0863205.png" /></td> </tr></table>

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 mathematics]]; [[Constructive analysis|Constructive analysis]].

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  E. Specker,   "Nicht konstruktiv beweisbare Sätze der Analysis"  ''J. Symbol. Logic'' , '''14'''  (1949)  pp. 145–158</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  B.A. Kushner,   "Lectures on constructive mathematical analysis" , Amer. Math. Soc.  (1984)  (Translated from Russian)</TD></TR></table>



====Comments====


====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  C. Calude,   "Theories of computational complexity" , North-Holland  (1988)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  H. Hermes,   "Aufzählbarkeit, Entscheidbarkeit, Berechenbarkeit" , Springer  (1978)</TD></TR></table>