Twitter
A Simple Proof of Gödel's Second Incompleteness Theorem Using Turing Machines
Gödel's second incompleteness theorem, in a nutshell, says that if a certain kind of mathematical theory can prove its own consistency (i.e. that it does not prove any contradictions), then that mathematical theory must actually be inconsistent.
Gödel's original proof of the second theorem is quite complicated, and even modern treatments of the full theorem involve hard-to-wrap-your-head-around concepts like Gödel numbering, ω-consistency, and Rosser's trick.
It turns out that all of this complexity can be avoided if you're willing to consider a version of the theorem that applies to mathematical theories strong enough to easily express strings and Turing machines. All of the Gödel-numbering complexity is necessary to make the theorem work in weaker systems like Peano arithmetic, but if you just want to prove it for theories like ZF(C), where most of modern mathematics operates, the proof is much easier, and we'll sketch that proof below.
I claim that if you can understand the proof that the halting problem is undecidable, then you can understand the proof of Gödel's second incompleteness theorem for theories like ZF(C).
Let's go!
Let T be the mathematical theory we're working in. For example, T could be ZF(C) set theory. You should imagine that all of the arguments we're about to give are translated into the formal language of T.
We need to make some assumptions about T, namely that there's an algorithm for checking proofs in T that always halts and tells us whether a proof is correct or not, which we'll call PrfT. The string p is a valid proof of the statement x within the theory T if and only if PrfT(p, x) = true. We also need to assume that some familiar rules of inference, like modus tollens, and others from first-order logic, are valid within T.
A statement x is provable in T if and only if there exists some string p (the proof) such that PrfT(p, x) = true.
What it means for T to be consistent is that it cannot prove a contradiction, i.e. there is no string A such that A and ¬A are both provable in T.
Gödel's second theorem says that if T can prove its own consistency, i.e. that there is no A such that both A and ¬A are provable within T, then T has to be inconsistent.
To prove this, we'll start by defining a Turing machine M that does the following:
On input X:
- For all strings p in lexicographical order: if PrfT(p, "X(X) never halts"), halt.
If we run M on a description of itself, M(M), then what it will do is start enumerating all possible strings, looking for a valid proof in T that M never halts when it's run on a description of itself, and it will halt only when it finds one. Crucially, PrfT, the proof-checking algorithm, always halts, so M(M) halts if and only if there exists a proof within T that M(M) never halts.
Note that if M(M) halts, then T has to be inconsistent. Since M(M) halted, it found a proof that M(M) doesn't halt. But since M(M) halted, there's also a proof that M(M) halts, which can be made by executing M(M) one step at a time inside a T proof until it halts. With a proof that M(M) halts and a proof that M(M) doesn't halt, we have a proof of a contradiction in T.
In other words, we've proven...
M(M) halts → ¬Con(T)
...where Con(T) means that T is consistent.
Now suppose our theory T can prove its own consistency, i.e. there's a proof of Con(T) within T itself.
Using this, we can prove that M(M) never halts:
- Con(T) (by the proof we suppose exists)
- M(M) halts → ¬Con(T) (as above)
- Therefore, ¬(M(M) halts).
But this argument can be turned into a valid proof in T, and so M(M) will eventually find it, and once it does, it will halt. This means that:
Con(T) is provable in T → M(M) halts.
We can now complete the argument:
- Con(T) is provable in T → M(M) halts
- M(M) halts → ¬Con(T)
- Therefore, Con(T) is provable in T → ¬Con(T).
Summarizing, in English: if T can prove its own consistency, then there's a proof that M(M) never halts. But since M(M) will find that proof, M(M) will actually halt, and since M(M) halts, T is inconsistent. We've established Gödel's second incompleteness theorem for T.
The only requirement for this argument to work is that T is powerful enough to express strings and Turing machines, and to formalize all of the arguments given above.
There you go! A proof of Gödel's second incompleteness theorem that's no harder to understand than the proof that the halting problem is undecidable!
If you're interested in Turing-machine-based proofs of Gödel's theorems, check out Scott Aaronson's blog post and a prior proof of the second theorem using Kolmogrov complexity.
