Edge Rewrite
// HTMLRewriter · presentation

This page was redesigned at the edge.

Cloudflare fetched the original article and streamed it through HTMLRewriter to apply an entirely new visual system without rebuilding the source page.

// request.cf · coarse context

A page that knows where it met you.

Only coarse request metadata is shown. This demo does not display or persist visitor IP addresses.

Country
US
Cloudflare location
CMH
Connection
HTTP/2
Language
Not provided

Ray ID: a242c7944a22ad68

Jump to content

Specker sequence

From Wikipedia, the free encyclopedia
A Specker sequence. The nth digit of xk is 4 if nk and the nth Turing machine in a computable Gödel numbering halts on input n after k steps; otherwise it is 3.

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).

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 1

[edit]

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 can be shown that is not a computable real number. Suppose, to the contrary, that were computable. Then the sequence would have a computable modulus of convergence: there would be a computable function such that

for all . Such a function can be obtained by approximating and comparing it with successive terms of . Since each new term in the enumeration changes a single digit in the binary expansion, a sufficiently accurate approximation to determines a stage after which the relevant initial segment can no longer change.

If such a function were computable, it would provide a decision procedure for . Given , compute . If were later enumerated into , the corresponding term would increase the sequence by . This cannot occur after all terms with indices greater than are within of one another. Therefore, if belongs to , it must appear among the first terms of the enumeration. These finitely many terms can be checked effectively, yielding a decision procedure for . This contradicts the assumption that is not decidable, so is not computable.

Construction 2

[edit]

Another construction of a Specker sequence (xm) can be given using an enumeration of Turing machines. Let {n}(n) denote the action of the n-th Turing machine on the number n. Then let the n-th decimal digit of xm be 4 if m > n and the computation {n}(n) halts within mn steps. If the computation has not finished after mn steps (or if m < n), the digit is 3. (See the figure above.)

  • Each xm is a rational number, since it has a periodic decimal expansion: after the first m decimal places, all digits are 3.
  • The sequence is computable, since to produce xm+1 after having calculated xm, one only has to simulate m + 1 Turing machines running for one step each.
  • The sequence is increasing, because when passing from xm to xm+1, digits can only change from 3 to 4.
  • The sequence is bounded, because it never exceeds 0.4444444... = 4/9.

The limit of this sequence is not a computable real number, since its decimal expansion contains a 4 in its n-th decimal place if the computation {n}(n) halts, and a 3 otherwise. Determining the digits of the limit would therefore solve the Halting problem, which is impossible.

See also

[edit]

References

[edit]
  • 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.