Specker Sequence¶
A computable bounded monotone sequence of rational numbers whose classical supremum is not a computable real.
Core Idea¶
A Specker sequence is a bounded sequence of rational numbers whose terms an algorithm can calculate, one stage at a time. The terms never decrease, so they approach a real limit. But there is no algorithm that computes that limit to any requested accuracy. The sequence converges in ordinary real analysis; its limit is missing only when we restrict attention to computable real numbers.[ref-02d9492f2b8c][ref-fc04d2291636]
Simpson builds such a sequence by adding small positive fractions as members of an undecidable, computably enumerable set appear. Beeson gives a different example using the measures of finite unions in a special recursive cover. In both, finite stages are computable but the total is not.[ref-02d9492f2b8c][ref-10826519d9ae]
What It Is Not¶
- Not a sequence that fails to converge. It has a limit in the full real numbers. The limit is not a computable real.[^ref-02d9492f2b8c]
- Not every slow or rate-free sequence. A computable sequence can lack a computable rate and still converge to computable zero if it is not monotone; Neri and Powell construct such a near miss.[^ref-fc04d2291636]
- Not the halting problem itself. Halting can supply the undecidable information in one construction, but the named type is the rational sequence and its noncomputable total. Simpson can use any suitable nonrecursive computably enumerable set.[^ref-02d9492f2b8c]
- Not a proof of an entire reverse-mathematics equivalence by itself. Simpson uses a related coded sequence for a
BW → ACA₀reversal; his separate theorem states the least-upper-bound equivalence.[^ref-02d9492f2b8c]
Scope of Application¶
Use the name in computable analysis when one uniform algorithm produces the rational terms, they are bounded and nondecreasing, and their classical supremum is provably noncomputable. The full real line is the space where the sequence converges. The computable reals are the restricted setting where its least upper bound is absent.[^ref-02d9492f2b8c]
The same test appears in unlike constructions: Simpson's set-encoded sums and Beeson's measures of finite unions in his singular cover.[ref-02d9492f2b8c][ref-10826519d9ae] It does not apply just because a numerical process has an unknown future value.
Clarity¶
Ask what can the algorithm calculate? It can calculate q_n for any given stage n. Then ask can it tell how close q_n is to the final real? For a Specker sequence, no algorithm provides a general answer for every requested accuracy. If it did, the limit would be computable, contrary to the construction.[^ref-fc04d2291636]
Classical convergence and computable convergence answer different questions. The first says there is a real limit; the second asks for an effective name or rate that can recover it. A Specker sequence passes the first test and fails the second.[^ref-02d9492f2b8c]
Manages Complexity¶
The label summarizes four checks: a uniform algorithm for rational terms, boundedness, monotonicity, and a noncomputable supremum. It keeps a long list of computed prefixes from being mistaken for an effective value of the total. Simpson's dyadic sums encode a nonrecursive set in that total.[^ref-02d9492f2b8c]
Beeson's finite-cover measures show a different route. The measures of growing finite unions can be calculated, but no computable accuracy cutoff gives the full union's measure in his construction. The interval-length partial sums discussed nearby in the paper are a separate sequence and should not be confused with these union measures.[^ref-10826519d9ae]
Abstract Reasoning¶
First show how to calculate the rational at stage n. Then show that the stages never decrease and stay below a common bound. Finally prove that computing their supremum would solve a noncomputable problem, or use another sound impossibility argument. In Simpson's example, the supremum would reveal membership in the nonrecursive set.[^ref-02d9492f2b8c]
The sequence still converges in the full real line. Its parent idea is Convergence. No computable rate tells us when a desired error has been achieved.[^ref-fc04d2291636] Its use is a mathematical counterexample, not a certified numerical stopping method.
Knowledge Transfer¶
When finite approximations can be computed, a separate tail bound is needed before the total can be called computable. That question transfers from Simpson's set-encoded sum to Beeson's cover measure, although the proofs that the total is noncomputable differ.[ref-02d9492f2b8c][ref-10826519d9ae]
The lesson is precise: an algorithm for every stage does not automatically become an algorithm for the limit. Calling any uncertain forecast a “Specker sequence” would skip the required monotonicity, boundedness, and proof of noncomputability.
Examples¶
Dyadic sums encoding a nonrecursive set¶
Simpson lets a one-to-one computable enumeration list a nonrecursive c.e. set. At each stage he sums positive dyadic fractions indexed by the members seen so far. These rational sums increase and stay bounded, but their supremum is not computable: computing it would determine the set.[^ref-02d9492f2b8c]
Role map: The enumeration computes each stage; adding distinct positive terms gives bounded monotone growth; the total is a noncomputable real. The stages converge classically without a computable rate.
Finite-union measures of a singular cover¶
Beeson considers a recursive singular cover and takes the measure of the union of its first N members. The values are bounded and cannot decrease as members are added. He identifies this sequence as Specker-type and proves that the measure of the full union is not computable in the specified construction.[^ref-10826519d9ae]
Role map: The finite cover prefix provides each stage; nested unions give bounded monotone measures; the full measure is the noncomputable limit. The proof here uses a late-cover accuracy-cutoff contradiction, not Simpson's dyadic membership coding.[^ref-10826519d9ae]
Relationships to Other Abstractions¶
Current abstraction Specker Sequence Domain-specific
Parents (1) — more general patterns this builds on
-
Specker Sequence is a kind of Convergence Prime
A Specker sequence converges to its real supremum, while its computable rational stages provide no computable rate for that limit.
Hierarchy path (1) — routes to 1 parentless root
- Specker Sequence → Convergence
Neighborhood in Abstraction Space¶
Specker Sequence sits in a sparse region of the domain-specific corpus (91st percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Integer Properties & Number-Theoretic Sets (15 abstractions)
Nearest neighbors
- Creative and Productive Sets — 0.82
- Clone (Universal Algebra) — 0.78
- Friedberg numbering — 0.78
- Grzegorczyk hierarchy — 0.78
- Coin Problem — 0.78
Computed from structural-signature embeddings · 2026-10-17
References¶
[^ref-02d9492f2b8c]: Simpson, Stephen G. Subsystems of Second Order Arithmetic, second-edition author PDF, 2006. Example I.8.4, pp. 29–30; Theorem I.9.1, p. 34; Theorem I.9.3(1), p. 35 (PDF pp. 37–38 and 42–43). https://sgslogic.net/t20/sosoa/chapter1.pdf. Full author PDF consulted; I.9.1 proves the BW → ACA₀ reversal, while I.9.3 states the LUB equivalence.
[^ref-10826519d9ae]: Beeson, Michael. Constructivity, Computability, and the Continuum. Author-hosted full PDF, especially PDF pp. 5 and 9–10, halting-digit illustration and singular-cover measures. https://www.michaelbeeson.com/research/papers/ccc.pdf. The finite-union measure case is distinct from the interval-length-series discussion.
[^ref-fc04d2291636]: Neri, Morenikeji, and Thomas Powell (2023). A computational study of a class of recursive inequalities. Journal of Logic & Analysis 15:3, Definition 2.1 and Propositions 2.2–2.3, PDF pp. 7–8. https://math.hawaii.edu/home/jla/469-1553-1-PB.pdf. Full journal PDF consulted.