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

[Andrej Bauer]

On Thursday 16 February 2006 15:13, Giovanni Lagnese wrote:
> Can someone give me an example of a recursively generable bounded sequence
> of rationals, for which there is no recursively enumerable set of indexes
> corresponding to a subsequence that is a Cauchy sequence?

Unless I misunderstood your question a Specker sequence will do the job. The 
following argument is written in constructive logic + formal Church's thesis, 
i.e. Recursive Mathematics (if you would prefer to have it written in the 
language of recursion theory, please let me know).

Let q_0, q_1, ... be a Specker sequence, i.e. a strictly increasing sequence 
of rationals inside the closed interval [0,1] such that it is without 
accumulation point, meaning that for every x in [0,1] there is m and epsilon 
> 0 such that |x - q_n| > epsilon for all n > m. A subsequence a_i = q_{f(i)} 
with f : N -> N strictly increasing is still without accumulation point, 
therefore it is non-Cauchy in a strong sense: for every epsilon > 0 and k 
there is m such that |a_k - a_n| > epsilon for all n > m.

Is that what you are looking for? Specker sequences are explained in many 
places, e.g. "Constructivism in Mathematics, vol. 1" by Troelstra and van 
Dalen.

Andrej Bauer