I found a construction in which I encountered a contradiction that I was not able to resolve by myself. I would be glad if someone can help me finding the error.
We look at binary sequences, i.e. infinite sequences $(b_i)$ with $b_i\in\{0,1\}$. Such a sequence should be called provably computable if there is
- a Turing machine $T$ which accepts the binary representation of a natural number $n$ as input, and halts on the $n$-th entry of $(b_i)$ (i.e. $b_n$) and an otherwise empty tape.
- a proof $P$ that the Turing machine $T$ in 1. halts for all inputs $n\in\Bbb N$.
Let $\mathcal T$ be the set of all Turing machines, and $\mathcal P$ the set of all proofs. A provably computable sequence is uniquely determined by such a pair $(T,P)\in\mathcal T\times\mathcal P$ (but not all such pairs describe such a sequence).
Since $\mathcal T$ and $\mathcal P$ are recursively enumerable, so is $\mathcal T\times \mathcal P$, and so are the provably computable sequences.
I think (but I am not quite sure here) that this informal description finally gives me a Turing machine $T'$ that starts on a tuple of natural numbers $n,m\in\Bbb N$ and halts on the $m$-th digit of the $n$-th provably computable sequence, as well as a proof $P'$ that shows that $T'$ indeed halts for all valid inputs. In detail, I would do it like this:
Enumerate all tuples $(T,P)\in\mathcal T\times\mathcal P$. Check if $P$ proves that $T$ halts for all valid inputs. If so, and if this was the $n$-th such finding so far, then simulate $T$ to output the $m$-th digit of the sequence $(T,P)$.
I know that this might encounter a sequence multiple times. But this does not matter (I think). It is only important that any provably computable sequence can be found in this way.
Now, I can use $T'$ and $P'$ to construct a sequence $(T'',P'')$, where $P''$ (as always) is a proof that $T''$ halts, and $T''$ starts on a natural number $n$ and halts on $1-T'(n,n)$. This means $(T'',P'')$ is the flipped diagonal of the list of all provably computable sequences, but as far as I can see, it is a provably computable sequence itself. By the usual argument of diagonalization it cannot be contained in the already presented enumeration. But the set of provably computable sequences is countable for sure.
So where is the mistake? Are some of the Turing machines or some of the proofs not so straightforwardly constructible as I thought?
Best Answer
The issue that you have run into is that you need to specify the system in which these proofs are being carried out. The set of "all possible proofs" is not r.e. - only the list of proofs in some fixed effective theory.
However, as a corollary of the incompleteness theorems, we know that such systems are very bad at talking about their own proofs. So, although ''we'' can use $T'$ and $P'$ to construct a new machine, this construction cannot be carried out within the same system which was used to make the list $P'$ in the first place. Instead, as it turns out, we will need to form $P''$ in a stronger system. This does not lead to a contradiction because $P''$ will not be in the previous enumeration.