Approachable = provably approachable?

Question

Question: Let’s call a real number $x$ approachable if there exists a Turing machine $M$ such that $M(1), M(2),\dots$ is a sequence than converge to $x$. If we can prove (edit: In ZFC) that the sequence converge, we say that $x$ is provably approachable. Is every approachable number also provably approachable?

Clearification: Another way to ask the same question is: Is it true that: "If there exists a Turing machine M such that x is the limit of the output values, then there exists a Turing machine M' that converge to the same number, and we can prove that it converge".

Comments: I don't know these concepts have names, I just invented the terminology: If they have names, please make a comment, so I can change it (edit: Approachable is called "computable in the limit", but I don't know if there is a name for provably appoachable. "Approachable" have been used a lot in the answers, so I have decided not the change it in the question). All computable numbers are provably approachable but not all provably approachable numbers are computable (Chatins constant is a counterexample). I don't know what the relation is between approachable and definable (I don't even know if there is an accepted definition of definable number?)

Answer 1

After a discussion with Russell Miller, I've got an answer to the question. There is in fact an approachable real that is not provably approachable.

Let us adopt PA as the base theory, although the construction can easily adapt to other theories. I will describe a Turing machine $M$ that produces a convergent sequence of rational numbers, but any Turing machine $M'$ that PA proves to produce a convergent sequence of rational numbers converges to a different number than $M$ does.

The idea is to diagonalize against any such proofs that may be discovered. Fix an enumeration of the Turing machines $M_n$. Consider the following Turing machine $M$. Our machine will at stage $k$ produce a rational number $r_k$ by giving finitely many trinary digits, but using only the digits 0 and 1 and not 2, to avoid non-unique readibility issues. As the construction proceeds, we systematically enumerate all possible proofs from the theory. We may find at some stage $k$ that there is a proof that Turing machine $M_n$ produces a convergent sequence of rational numbers. In this case, we run $M_n$ for $k$ steps, getting the current rational $q_{n,k}$ approximation to the real to which $M_n$ is converging. In this case, if $r_k$ is different from $q_{n,k}$ by digit $n$, then we use $r_{k+1}=r_k$; otherwise, we produce $r_{k+1}$ by flipping the $n$-th digit of $r_k$ from $0$ to $1$ or vice versa to ensure that $r_{k+1}$ is different from $q_{n,k}$. (Note, we are flipping the $n$-th digit, not the $k$-th digit, so each machine $M_n$ is tied to the $n$-th digit of our limit real.) And simply proceed with this plan, considering the new proofs as they appear.

Note that each machine $M_n$ that provably produces a convergent sequence will be considered infinitely many times, for increasingly large $k$, since there are many proofs that it does so. So the relevant $k$ for $M_n$ will become arbitrarily large. Since $M_n$ was proved to produce a convergent sequence, it follows that the values of $q_{n,k}$ really do converge, and thus eventually stabilize in their first $n$ bits (if those bits are all $0$s and $1$s). Thus, we will flip the $n$-th bit of our rational $r_k$ at most finitely many times. It follows that our sequence $r_k$ is a convergent sequence of rational numbers.

But also, it follows that whenever there is a proof that some machine $M_n$ produces a convergent sequence of rational numbers, then the limit of our real will differ from the limit of that machine by digit $n$.

Thus, we have an approachable real that is not provably approachable, as desired.

Let me remark on the confusing subtle point here about in which theory we have proved our machine to produce a convergent sequence of rationals. The answer is that we have done so in any theory that knows that any statement that is provable in the base theory is in fact true, since we needed to know that when we found a proof that $M_n$ produces a converging sequence of rationals, that those rationals really did converge. For example, ZFC has this relation to PA, since ZFC proves that if $\varphi$ is provable in PA, then $\varphi$ is true. But more generally, for any $\omega$-consistent theory $T$, we may extend to a stronger theory $T^+$ that knows this implication.

Answer 2

This post is marked community wiki because it is just an elaboration on how I understand the question.

To make these question precise, I would make this definition:

A provably approachable real number in a theory $T$ is a Turing machine $A$ such that $T$ proves that $A$ enumerates a convergent sequence of rational numbers.

On the other hand, a real number $z$ is approachable if there is a Turing machine $M$ such that $M$ enumerates a sequence of rationals converging to $z$. The statement ``every approachable real number is provably approachable'' then means that, for every approachable real number $z$, there is a machine $M$ such that $M$ enumerates a sequence of rationals converging to $z$ and $T$ proves that $M$ enumerates a convergent sequence of rationals.

The approachable reals are usually called "limit computable" in the literature, because of the following result.

Theorem. A real number is approachable if and only if its binary expansion is computable from the halting problem, which happens if and only if the binary expansion is a $\Delta^0_2$ set when viewed as a subset of $\mathbb{N}\times\{0,1\}$.

Here is the question as I read it.

Question 1. Is every approachable real number provably approachable in ZFC? (ZFC can be replaced with any other effective theory.)

The issue is not: given a Turing machine which we know to be total, can we prove in ZFC that the machine is total - the answer to that is certainly "no". Instead, the question is, essentially: if we have a Turing machine $A$ that happens to be total in the standard model, is there some other Turing machine $M$ that computes the same function on standard inputs, but which is also provably total? (Note that in general the function computed in an arbitrary model is an extension of the function computed in the standard model because now there are also nonstandard inputs.) I don't know the answer to that yet, but I think it's a very interesting question.

When I first wrote this comment, I had the idea of "provably computable" real number in my head instead of "provably approachable". The same question can be asked for that:

Question 2. Is every computable real number provably computable in ZFC, where computable means that the binary expansion is c.e. and provably computable means there is some machine that enumerates the binary expansion and which ZFC proves to be total?

This is essentially equivalent to the first question, because the first question is just the relativization of the second to $0\prime$.

Answer 3

Your question is vague, which prevents an answer. This is too long for a comment, so I am writing it here.

First of all, you haven't said what the axioms of your proof system are. If we have a very weak formal system, of course, then you will get a negative answer, since we won't be able to prove very much. But as the system gets stronger, we will be able to prove more. (In an inconsistent system, of course, we can prove anything.) So perhaps you are really asking whether, say, ZFC or PA are already strong enough to prove the instances you are interested in.

Second, however, what statement is it that should be provable, exactly? You seem to want to suppose that a real $x$ is approachable, and ask of this particular real whether it is provable that it is approachable. But of course ZFC doesn't know which particular $x$ you are talking about, unless you provide a description of it. So what do you mean? Since we have supposed that $x$ is approachable by some Turing machine $M$, then the only sensible description of $x$ we have is simply "the limit of the values output by $M$". But in this case, the question becomes the triviality of proving the statement: "The real $x$ that is the limit of the output values of Turing machine $M$ is the limit of the output values of some Turing machine."

So it seems that the question wants clarification.