[FOM] counterexamples to the computable Bolzano-Weierstrass theorem
akreuzer at mathematik.tu-darmstadt.de
Wed Apr 14 04:41:04 EDT 2010
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  or  require an instance
of \Sigma^0_1-WKL, that is weak Koenig's lemma for trees given as
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
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'.
 Pavol Safarik and Ulrich Kohlenbach, On the computational content
of the Bolzano-Weierstrass principle,
to appear in Math. Log. Quart.
 Ulrich Kohlenbach, Arithmetizing proofs in analysis,
Logic Colloquium '96 (San Sebastian), Lecture Notes Logic, vol. 12,
Springer, Berlin, 1998, pp. 115-158.
More information about the FOM