[FOM] counterexamples to the computable Bolzano-Weierstrass theorem

[Alberto Marcone]

Dear FOMers,
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.

Thanks in advance for any reference.

Best wishes,
Alberto
-- 
Alberto Marcone                            alberto.marcone at dimi.uniud.it
Dip. di Matematica e Informatica
Universita' di Udine                                tel: +39-0432-558482
via delle Scienze 206                               fax: +39-0432-558499
33100 Udine
Italy                       http://users.dimi.uniud.it/~alberto.marcone/