[FOM] counterexamples to the computable Bolzano-Weierstrass theorem

[Alexander Kreuzer]

On Mar 17, 2010, Alberto Marcone wrote:

> it is well-known that there exists a computable sequence of points in 
> the unit interval without computable accumulation points (here reals are 
> coded by Cauchy sequences of rationals converging at a prescribed rate). 
> Therefore the Bolzano-Weierstrass theorem is computably false.

> Actually, the sequence can be strictly increasing and its (unique) 
> accumulation point computes 0' (see e.g. the proof that BWT implies ACA0 
> in Simpson's book).

> Recent work in Weihrauch-style computable analysis (Le Roux and Ziegler, 
> Singular coverings and non-uniform notions of closed set computability, 
> MLQ 54 (2008), 545-560, see Theorem 3.6) implies that there exists a 
> computable sequence with no Delta^0_2 accumulation point.

> I am wondering whether this sharper result was already known, e.g. by 
> people working in computable mathematics.

Dear Alberto, dear FOMers,

this result was known in proof mining. The formalized proofs of the
Bolzano-Weierstrass principle (BW) in [1] or [2] require an instance
of \Sigma^0_1-WKL, that is weak Koenig's lemma for trees given as
\Sigma^0_1 predicate.
The proofs immediately suggest that solutions of BW correspond
to infinite branches of \Sigma^0_1 0/1-trees. Thus the accumulation 
points are in general only computable in a degree d>>0'.

However, I am not aware of any reference for this fact. But I put
a draft at

http://www.mathematik.tu-darmstadt.de/~akreuzer/files/coh.pdf

including a proof for this equivalence.

Moreover our recent work shows that passing from a bounded sequence
to a naively computable accumulation point (that is a Cauchy
subsequence without prescribed convergence rate) is equivalent to the
(strong) cohesive principle, see also the draft.
A real number for the accumulation point is then computable in the
Turing jump of the naively computable accumulation point.
Since the cohesive principle is low_2 and in general not low, this also
shows that a solution of BW is in general only computable in a 
degree that is low relative to 0' and not in 0'.

Best wishes,
Alexander

[1] Pavol Safarik and Ulrich Kohlenbach, On the computational content
    of the Bolzano-Weierstrass principle,
    to appear in Math. Log. Quart.
    http://www.mathematik.tu-darmstadt.de/~kohlenbach/bw.pdf 
[2] Ulrich Kohlenbach, Arithmetizing proofs in analysis,
    Logic Colloquium '96 (San Sebastian), Lecture Notes Logic, vol. 12,
    Springer, Berlin, 1998, pp. 115-158.

--
Alexander Kreuzer
TU Darmstadt
www.mathematik.tu-darmstadt.de/~akreuzer