# Decide the limit of a decreasing sequence of real number

Given a bounded decreasing sequence of rational number $a_0,a_1,\cdots$, then we know that it has limit $a$. Suppose this sequence satisfy that $|a_k-a|<1/2^k$ for any $k$.

The sequence is given as an oracle: One can obtain $a_k$ by querying $k$, and of course the limit $a$ is not known.

We are given another rational number $b$ and our goal is to decide whether $a=b$. Is this problem decidable?

-
You say "another rational number $b$." Does that mean $a$ is also rational? –  François G. Dorais Jun 4 '13 at 4:42
Surely not. Consider the case where $b=0$. Suppose we have asked the oracle about $a_k$ for all $k$ in a finite set $K$, and each time the oracle has replied that $a_k=2^{-k-1}$. We still cannot tell whether $a=0$; it might be $2^{-\max(K)-1}$. –  Neil Strickland Jun 4 '13 at 5:28
@Neil Strickland That argument is nice, but can it be considered as a proof? –  gondolf Jun 4 '13 at 8:03

No, in the sense that if we had a decision procedure for this then it could also be used to decide the halting problem, for example.

For simplicity and without loss of generality, I will take $b = 0$. Then $a \neq 0$ corresponds to one of two $\Sigma^0_1$-statements: $$(\exists k)(a_k \leq 0) \quad\text{or}\quad (\exists k)(a_k \geq 1/2^k).$$ Both of these are pretty generic so it's easy to reduce the halting problem to this.

Given a Turing machine $M$ (with blank input), consider the sequence $$a_k = \begin{cases} \frac{1+17^{-k}}{2^{h+2}} & \text{M halts in h \lt k steps,} \cr \frac{1+17^{-k}}{2^{k+2}} & \text{otherwise.} \end{cases}$$ Then $M$ halts precisely when $\lim_{k\to\infty} a_k \neq 0$.

-
I added a random factor to make the sequence decreasing. –  François G. Dorais Jun 5 '13 at 14:51
@François Thank you! We suppose $|a_k-a|<1/2^k$ holds for all $k$. –  gondolf Jun 6 '13 at 2:50

(More like comments than another answer, but I don't have enough reputation to comment.)

(1) It might be interesting, but is not quite explicit in François' answer, that this is undecidable even if the input is given as a Turing machine rather than just an oracle: For any TM $M$, we can construct a TM $M'$ that outputs François' sequence. (Hardwire $M$ into $M'$; then for each $k$, simulate $M$ for $k$ steps on blank input and output the appropriate number.) We still cannot decide if the limit of the sequence is zero by examining $M'$, unless we can decide if $M$ halts.

(2) Also maybe interesting -- I believe that, in computable analysis, the usual model is that a real number $a$ is given as you propose, but on both sides (an infinite sequence of intervals, each contained in the previous one, with limit equal to $a$). So your question is almost whether equality on the reals is decidable (except that the second number, $b$, is rational, but this doesn't seem easier); and undecidability of equality on the reals is a primary result in computable analysis!

-