Specker sequence

In computability theory, a Specker sequence is a computable, monotonically increasing, 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 (1949).

A Specker sequence. The nth digit of xk is 4 if n ≤ k and the computation of {n}(n) halts after k steps; otherwise it is 3.

The existence of Specker sequences has consequences for computable analysis. The fact that such sequences exist means that the collection of all computable real numbers does not satisfy the least upper bound principle of real analysis, even when considering only computable sequences. A common way to resolve this difficulty is to consider only sequences that are accompanied by a modulus of convergence; no Specker sequence has a computable modulus of convergence. More generally, a Specker sequence is called a recursive counterexample to the least upper bound principle, i.e. a construction that shows that this theorem is false when restricted to computable reals.

The least upper bound principle has also been analyzed in the program of reverse mathematics, where the exact strength of this principle has been determined. In the terminology of that program, the least upper bound principle is equivalent to ACA0 over RCA0. In fact, the proof of the forward implication, i.e. that the least upper bound principle implies ACA0, is readily obtained from the textbook proof (see Simpson, 1999) of the non-computability of the supremum in the least upper bound principle.

Construction

The following construction is described by Kushner (1984). Let A be any recursively enumerable set of natural numbers that is not decidable, and let (ai) be a computable enumeration of A without repetition. Define a sequence (qn) of rational numbers with the rule

It is clear that each qn is nonnegative and rational, and that the sequence qn is strictly increasing. Moreover, because ai has no repetition, it is possible to estimate each qn against the series

Thus the sequence (qn) is bounded above by 1. Classically, this means that qn has a supremum x.

It is shown that x is not a computable real number. The proof uses a particular fact about computable real numbers. If x were computable then there would be a computable function r(n) such that |qj - qi| < 1/n for all i,j > r(n). To compute r, compare the binary expansion of x with the binary expansion of qi for larger and larger values of i. The definition of qi causes a single binary digit to go from 0 to 1 each time i increases by 1. Thus there will be some n where a large enough initial segment of x has already been determined by qn that no additional binary digits in that segment could ever be turned on, which leads to an estimate on the distance between qi and qj for i,j > n.

If any such a function r were computable, it would lead to a decision procedure for A, as follows. Given an input k, compute r(2k+1). If k were to appear in the sequence (ai), this would cause the sequence (qi) to increase by 2−k-1, but this cannot happen once all the elements of (qi) are within 2−k-1 of each other. Thus, if k is going to be enumerated into ai, it must be enumerated for a value of i less than r(2k+1). This leaves a finite number of possible places where k could be enumerated. To complete the decision procedure, check these in an effective manner and the return 0 or 1 depending on whether k is found.

See also

References
  • Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics, Oxford, 1987.
  • B.A. Kushner (1984), Lectures on constructive mathematical analysis, American Mathematical Society, Translations of Mathematical Monographs v. 60.
  • Jakob G. Simonsen (2005), "Specker sequences revisited", Mathematical Logic Quarterly, v. 51, pp. 532–540. doi:10.1002/malq.200410048
  • S. Simpson (1999), Subsystems of second-order arithmetic, Springer.
  • E. Specker (1949), "Nicht konstruktiv beweisbare Sätze der Analysis" Journal of Symbolic Logic, v. 14, pp. 145–158.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.