Specker sequence

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

The existence of Specker sequences has implications for computable analysis. The fact that there are such consequences, it means that the class of computable real numbers is not as known from real analysis Supremumseigenschaft, even if this one is limited to predictable consequences. A common way to solve this problem, it only predictable consequences provided viewed with a predictable convergence module. No Specker sequence has a predictable convergence module, which means that each convergence module of a Specker sequence grows faster than any computable function, otherwise would reveal in a predictable way, how many sequence elements are fixed the first digits, and thus would be the supremum of a computable real number.

The Supremumseigenschaft was also studied in the field of reverse mathematics, where their exact strength was determined. In the language of the discipline is the Supremumseigenschaft equivalent to ACA0 about RCA0.

Violation of Supremumseigenschaft

Since every rational number is computable and the completion of the rational numbers exactly the set of real numbers is known, form the computable real numbers as a countable set but a proper subset of the real numbers, the computable real numbers can not be complete. As said Supremumseigenschaft in metric, separable, ordered spaces, and thus each subspace of the real numbers is equivalent to the order of completeness and, consequently, for completeness, the computable real numbers can not meet the Supremumseigenschaft. The obvious would now be limited to predictable consequences predictable numbers.

Construction

The existence of a Specker sequence also stipulates that the Supremumseigenschaft is already violated if one is limited to predictable consequences. The following construction was described by Kushner (1984). Let A be a recursively enumerable, but not decidable set of natural numbers, and let ( ai) a computable enumeration of A without repetition. A sequence ( qn ) of rational numbers is defined by the rule

Obviously each qn is non-negative and rational, and the sequence ( qn ) increases monotonically. It is also possible, each Qn to the series

Estimate, since (ai ) contains no repetition. Therefore, the sequence ( qn ) is bounded by 1. Classically, this means that ( qn ) x has a supremum.

It has been shown that X is not a predictable real number. The proof uses a certain fact about computable real numbers: If x would be computable, then there would be a computable function r (n) such that | qj - qi | <1 / n for all i, j > r (n). To calculate r, we compare the Binärexpansion of x with the Binärexpansion of qi for larger and larger values ​​of i, the definition of qi means that every time i increases by 1, a binary digit from 0 to 1 transition. So there is an n such that a sufficiently large initial segment is determined by x by qn such that no more binary digit can change in the play to 1, which leads to an estimate of the distance between qi and qj Füri, j > n.

If any such function would be r predictable, this would result in the following way to a decision procedure for A. Given an input k, we compute r ( 2k 1). If k in the sequence ( ai) would show up, this would cause an increase of ( qi) by 2 -k -1, but this can not happen as soon as all elements of ( q i) not more than 2 -k -1 apart are. If, therefore, enumerated in a k a i, it must be less than R (2k 1) to the value of i. It is a finite number of possible locations where k may be enumerated. To complete the decision-making process, one examines these finitely many points in a predictable manner and give 0 or 1 from, depending on whether k is found or not.