Is it possible for the convergence of a sequence to be undecidable?

[carmine timber]

I am not talking about a sequence like $$a_n=\cases{0 \text{ ,if $2^n-1$ is not prime and }\ 1 \text{ , if $2^n-1$ is prime } }$$ Because theoretically it is provable that Mersenne primes are either infinite or finite and from there the convergence of the sequence follows.

[vital idol]

trigonometria
Compile Error! Click the reaction for more information.
(You may edit your message to recompile.)

[zenith kraken]

If I got your question right, any sequence of numbers either have a limit or doesn't have one. So, any series is either convergent or divergent.

[carmine timber]

Yes. But are there cases where (in theory) we cannot prove if a sequence converges or diverges? In other words , can the convergence of a sequence only be provable by tools we do not have?

[zenith kraken]

you have just given an example of that with those Mersenne primes. We dont have a tool to prove that it is a finite set right now. But this sequence is well defined. It is either convergent or divergent.

[carmine timber]

When I say tools I mean , whatever foundational system S we are working in , if it can handle basic arithmetic , we can not prove that it converges or diverges inside S .

This , now, seems obvious that such sequences have to exist otherwise S proves itself consistent, which contradicts Godel's incompleteness theorem. But I am still interested in a specific example.

[next swift]

I don't think you can have a specific undecidable sequence, but i can prove that an undecidable sequence exists

[sick iris]

not exactly your question but every Goodstein sequence (https://en.wikipedia.org/wiki/Goodstein's_theorem) eventually converges to 0, which is a fact that is true yet unprovable within Peano Arithmetic

[sick iris]

you can also do something akin to Chaitin's constant:
https://mathworld.wolfram.com/ChaitinsConstant.html

let $\Omega_{U}$ be (some) Chaitin's constant.\
let $a_n = n$th digit of Chaitin's constant in binary (so $a_n \in {0,1}$).\
let $f(x) = 2x-1$. we then have $f(0) = -1$ and $f(1) = 1$\
consider the sequence of partial sums:
$$S_n = \sum_{k=1}^n \frac{f(a_k)}{k}$$

[vital idol]

artemetra

[sick iris]

since the exact value of Chaitin's constant is undecidable, the converge of this sum is undecidable as well and hence the convergence of the sequence of partial sums