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?
 A: 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$. 
A: (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!
