Diagonalization on turing machines and proofs. Where does the argument fail?

Question

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

1. 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.
2. 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?

Answer 1

Let's say we fix a "background theory" in which our proofs take place, which is also sound, since otherwise this question is a bit silly - say, we work in ZFC.

The problem is that the sequence (call it $\Sigma$) you describe, while always defined, isn't provably (in ZFC) always defined! So there's no reason for it to be on the list.

Why isn't it provably computable? Well, the problem is this: ZFC proves that $\Sigma(n)$ is defined for each specific $n$, but it doesn't prove the sentence "$\forall n$, $\Sigma(n)$ is defined." So $\Sigma$ shouldn't in fact show up on the list, and there's no contradiction.

Why is this so? Well, first note that ZFC trivially proves "For each $n$, I prove that the $n$th bit of the $n$th computably provable sequence is defined." In particular, for a given $n$ let $S_n$ be the sequence all of whose terms are $0$ if there is no contradiction in ZFC of length $\le n$, and all of whose terms are undefined otherwise. For each specific $n$, ZFC proves that $S_n$ is always defined. Moreover, ZFC proves "For all $n$, I prove that $S_n$ is total" - by a cases argument (either ZFC is consistent, or ZFC is inconsistent and hence proves everything).

So ZFC proves "If $\Sigma$ is total, then each $S_n$ is total" (since it proves that each $S_n$ occurs as an entry in the list of provably computable functions). However, ZFC obviously doesn't prove the sentence "All $S_n$s are always defined." So ZFC can't prove the totality of $\Sigma$.

What's going on here? ZFC proves "I prove that each $S_n$ is total," but it apparently doesn't prove "Each $S_n$ is total." This is a soundness issue: in general, ZFC can't prove that things it proves are true. In fact, if ZFC proves "If I prove $\varphi$, then $\varphi$ is true," then it outright proves $\varphi$! So the "self-confidence" of ZFC doesn't extend past the things it already knows to be true.

In particular, $\Sigma$ is provably computable in the theory ZFC + "ZFC is ($\Pi^0_2$-)sound," but this is a vastly stronger theory - and this is similar to how ZFC + "ZFC is consistent" unproblematically proves the Goedel sentence of ZFC.

Answer 2

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.