[FOM] Can someone give me an example of...

[Andrej Bauer]

Let me see if this time around I can get things right. There are two possible 
readings of what Giovanni Lagnese asked for:

1) A computable bounded rational sequence such that every computable
   subsequence fails to be _effectively_ Cauchy.

2) A computable bounded rational sequence such that every computable
   subsequence fails to be _classically_ Cauchy.

In my earlier post I was answering 1), although I explained things rather 
unsuccessfully. Let me try again.

Consider a monotone Specker sequence (s_n) inside [0,1]. Suppose there existed 
a computable subsequence a_k = s_{n_k} which were also effectively Cauchy. 
Then its limit x = lim a_k would be a computable real and an accumulation 
point of (s_n). But (s_n) has no computable accumulation points.

This I think answers 1). Clearly, it does not answer 2) because a montone 
Specker sequence itself is a Cauchy sequence (but not effectively Cauchy). I 
believe Giovanni is asking about 2). I do not know the answer.

Andrej Bauer