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

[Andrej Bauer]

On Sunday 19 February 2006 00:38, Andrej Bauer wrote:
> 2) A computable bounded rational sequence such that every computable
>    subsequence fails to be _classically_ Cauchy.

The following argument is constructive modulo the statement

 (*) every binary sequence contains infinitely many 0's or infinitely many 1's 

We show that 2) is impossible. Suppose (a_n) is a bounded computable rational 
sequence. Then it contains a monotonically decreasing or a monotonically 
increasing subsequence, which follows from (*). Suppose it contains a 
monotonically decreasing sequence and let a_k be its first term. Define a 
computable subsequence

  b_0 = a_k
  b_n = first term of (a_n) after b_{n-1} which is less or equal b_{n-1}

Then (b_n) is a bounded computable monotonically decreasing sequence, 
therefore it is classically Cauchy. If (a_n) contains a monotonically 
increasing subsequence, the argument is similar.

Replacing in 2) above computable rational sequences by computable sequences of 
computable reals does not help. We can still prove that there exists a 
monotone subsequence, as above, except that b_n is defined by a parallel 
search for the next term smaller than b_{n-1}, because we cannot rely on 
decidablility of "less than or equal" order on rationals.

Andrej Bauer