Specker series

A Specker episode. The -th digit of is when the calculation of after steps stops; otherwise ${\displaystyle n}$ ${\displaystyle x_{n+k}}$ ${\displaystyle 4,}$ ${\displaystyle \left\{n\right\}(n)}$ ${\displaystyle k}$ ${\displaystyle 3.}$

In the theory of computability , the Specker sequence is a computable , monotonically growing, bounded sequence of rational numbers whose supremum is not a computable real number . The first example of such a sequence was constructed by Ernst Specker in 1949 .

The existence of Specker sequences has consequences for computable analysis . The fact that such sequences exist means that the class of computable real numbers does not have the supremum property known from real analysis , even if one restricts oneself to computable sequences. A common way to solve this problem is to consider only calculable sequences provided with a calculable convergence module. No Specker sequence has a calculable convergence module, which means: Each convergence module of a Specker sequence grows faster than any calculable function, otherwise it would be possible to estimate in a calculable way how many elements of the sequence the first digits are after , and the supremum would be a calculable real one Number. ${\displaystyle n}$

The supremum property has also been studied in the area of reverse mathematics , where its exact strength has been determined. In the language of the discipline, the Supremum property is equivalent to ACA ₀ over RCA ₀ .

Violation of the supremacy property

Since every rational number is calculable and the completion of the rational numbers is known to be exactly the set of real numbers, but the calculable real numbers as a countable set form a real subset of the real numbers, the calculable real numbers cannot be complete. Since said supremacy property in metric , separable , ordered spaces and thus every subspace of the real numbers is equivalent to order completeness and thus to completeness, the computable real numbers cannot fulfill the supremacy property. The obvious thing to do now would be to limit oneself to calculable sequences of calculable numbers.

construction

The existence of a Specker sequence also means that the supremum property is already violated if one restricts oneself to calculable sequences. The following construction was described by Kushner. Let be a recursively enumerable , but not decidable set of natural numbers, and let ( ) be a computable enumeration of without repetition. A sequence of rational numbers is through ${\displaystyle A}$ ${\displaystyle a_{i}}$ ${\displaystyle A}$ ${\displaystyle \left(q_{n}\right)}$

${\displaystyle q_{n}:=\sum _{i=0}^{n}2^{-a_{i}-1}}$

Are defined. Obviously, each is nonnegative and rational, and the sequence grows monotonously. It is also possible to put each one in turn ${\displaystyle q_{n}}$ ${\displaystyle \left(q_{n}\right)}$ ${\displaystyle q_{n}}$

${\displaystyle \sum _{i=0}^{\infty }2^{-i-1}=1}$

to be estimated upwards, as there is no repetition. Hence the sequence is limited by. Classically, this means having a supremum . ${\displaystyle (a_{i})}$ ${\displaystyle \left(q_{n}\right)}$ ${\displaystyle 1}$ ${\displaystyle (q_{n})}$ ${\displaystyle x}$

It has been shown that is not a computable real number. The proof uses a certain property of computable real numbers: If it were computable, then there would be a computable function such that for all . To calculate, compare the binary expansion of with the binary expansion of for ever larger values ​​of . The definition of means that every time um increases, a binary digit changes from to . So there is a such that a sufficiently large initial section from through is defined in such a way that no further binary digit in this section can change to, which leads to an estimate of the distance between and for . ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle r(n)}$ ${\displaystyle \left|q_{j}-q_{i}\right|<{\tfrac {1}{n}}}$ ${\displaystyle i,j>r(n)}$ ${\displaystyle r}$ ${\displaystyle x}$ ${\displaystyle q_{i}}$ ${\displaystyle i}$ ${\displaystyle q_{i}}$ ${\displaystyle i}$ ${\displaystyle 1}$ ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle n}$ ${\displaystyle x}$ ${\displaystyle q_{n}}$ ${\displaystyle 1}$ ${\displaystyle q_{i}}$ ${\displaystyle q_{j}}$ ${\displaystyle i,j>n}$

If any such function were computable it would result in a decision process for in the following way . Calculate for an input . If the sequence occurred, it would cause an increase of um . But that cannot happen as soon as all elements are no further than apart from each other. So if one is enumerated, it must be less than the value of . There remains a finite number of possible places where one could enumerate. In order to complete the decision-making process, you check this finite number of positions in a predictable way and output or output, depending on whether it is found or not. ${\displaystyle r}$ ${\displaystyle A}$ ${\displaystyle k}$ ${\displaystyle r(2^{k+1})}$ ${\displaystyle k}$ ${\displaystyle \left(a_{i}\right)}$ ${\displaystyle q_{i}}$ ${\displaystyle 2^{-k-1}}$ ${\displaystyle \left(q_{i}\right)}$ ${\displaystyle 2^{-k-1}}$ ${\displaystyle k}$ ${\displaystyle a_{i}}$ ${\displaystyle i}$ ${\displaystyle r(2^{k+1})}$ ${\displaystyle k}$ ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle k}$

literature

• Douglas Bridges, Fred Richman: Varieties of Constructive Mathematics. Oxford 1987.
• Jakob G. Simonsen: Specker sequences revisited. In: Mathematical Logic Quarterly. 2005, Volume 51, pp. 532-540. doi : 10.1002 / malq.200410048
• S. Simpson: Subsystems of second-order arithmetic. Springer, 1999.
• E. Specker: Theorems of analysis that can not be proven constructively. In: Journal of Symbolic Logic. 1949, Volume 14, pp. 145-158.

Individual evidence

1. ^ BA Kushner: Lectures on constructive mathematical analysis. In: American Mathematical Society: Translations of Mathematical Monographs. 1984, volume 60.