Are limits decidable? Should definitions be decidable? [closed]

This question is about the Turing computability of the $\epsilon-N$ definition of a limit of an infinite sequence $S$. First, a proposition:

There cannot exist a Turing Machine $M$ which, given a program $P_S$ whose output is the sequence $S$, has output $$M(P_S) = \left\{ \begin{array}{rl} \operatorname{true} & \text{if}\,\lim(S)\, \text{exists} \\ \operatorname{false} & \text{otherwise.} \end{array}\right.$$

In other words, a Turing Machine cannot decide if $\lim(S)$ exists. A short argument as to why this is the case is below.

My questions are:

1. is there another (perhaps weaker) definition of limit which is decidable?

2. a definition is "a statement of the exact meaning". Does an undecidable concept have an exact meaning? Perhaps undecidable statements are less suited to be definitions than decidable statements.

Argument: A Turing Machine that decides the existence of $\lim(S)$ could be used to solve the Halting Problem in the following way.

Denote $P_S\oplus0$ as the program that runs $P_S$ and upon observing the termination symbol appends an infinite number of zeros. Similarly $P_S\oplus 01$ is the program that appends an infinite alternating sequence $01010101\ldots$.

Then $P_S$ halts iff ($M(P_S\oplus 0)$ and not $M(P_S\oplus 01)$).

Hence the existence of limits, for sequences given by algorithms, cannot be decided by a Turing Machine.

closed as off-topic by Jeremy Rickard, Andrés E. Caicedo, Chris Godsil, Andy Putman, Alex DegtyarevAug 5 '15 at 8:29

• This question does not appear to be about research level mathematics within the scope defined in the help center.
If this question can be reworded to fit the rules in the help center, please edit the question.

• I'm voting to close this as off-topic because MathOverflow is not a discussion forum and this post is seeking to start a discussion rather than asking a question. – Jeremy Rickard Aug 5 '15 at 1:48
• Now there is a question, but I don't understand what it means. What would you consider a satisfactory answer? – Noah Schweber Aug 5 '15 at 4:03
• Actually, when you look closely at elementary analysis, lots of things are undecidable. For example, you might consider Richardson's Theorem en.wikipedia.org/wiki/Richardson%27s_theorem which says that, for a very natural class of expressions, it's impossible to tell if they are equal to $0$. – Robert Israel Aug 5 '15 at 4:38
• Thanks for helping me to grow my question. I've split this into two parts: first I'd like to know if there is a decidable version of $\lim$. For the second question I'm interested in people's opinion on what constitutes a definition. – Daniel Mansfield Aug 5 '15 at 5:37
• Formally, mathematics is founded on axiomatic systems, rather than on computational models; the Church-Turing thesis does not apply to (say) structures of ZFC. In an axiomatic system, a term is well defined so long as it provably has a unique interpretation for all admissible choices of parameters. Computability of this interpretation would be a desirable bonus if available, but is not necessary in order to usefully take advantage of a mathematical definition. – Terry Tao Aug 5 '15 at 5:52