8
February 9, 2024

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, where consistency means that the theory does not prove any contradictions, then that mathematical theory must actually be inconsistent. The theory says, "If I can prove that I'm consistent, then I must actually be inconsistent."

Gödel's original proof of the second theorem is quite complicated. 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 you can avoid all of that complexity if you're only interested in proving the theorem for theories strong enough to talk about strings and Turing machines. The complicated Gödel-numbering stuff is necessary to prove the theorem in weaker systems like Peano arithmetic, because there you need crazy trickery to encode statements about proofs into statements about numbers, but if you just want to prove it for theories like ZFC set theory, where most of modern mathematics operates, the proof is much easier.

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.

Let's go!

Proving the Second Theorem

Let $T$ be the mathematical theory we're working in. A theory is basically a list of axioms and an algorithm for checking that proofs are correct. For example, $T$ could be ZFC set theory, with all of its axioms and rules of inference.

You should imagine that all of the arguments we're about to give are translated into the formal language of $T$. In other words, to make this proof rigorous, we would just need to translate all of the English below into the formal symbols and deduction rules that $T$ allows.

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 $\text{Prf}_T$. The string $p$ is a valid proof of the statement $x$ within the theory $T$ if and only if $\text{Prf}_T(p, x) = \text{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 $\text{Prf}_T(p, x) = \text{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 $\lnot 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 $\lnot 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$:

  1. For all strings $p$ in lexicographical order: if $\text{Prf}_T(p, \text{``}X(X) \text{ 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, $\text{Prf}_T$, 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) \text{ halts} \rightarrow \lnot\text{Con}(T)$$

...where $\text{Con}(T)$ means that $T$ is consistent.

Now suppose our theory $T$ can prove its own consistency, i.e. there's a proof of $\text{Con}(T)$ within $T$ itself.

Using this, we can prove that $M(M)$ never halts:

  1. $\text{Con}(T)$ (by the proof we suppose exists)
  2. $M(M) \text{ halts} \rightarrow \lnot\text{Con}(T)$ (as above)
  3. Therefore, $\lnot(M(M) \text{ 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:

$$\text{Con}(T) \text{ is provable in } T \rightarrow M(M) \text{ halts}$$

We can now complete the argument:

  1. $\text{Con}(T) \text{ is provable in } T \rightarrow M(M) \text{ halts}$
  2. $M(M) \text{ halts} \rightarrow \lnot\text{Con}(T)$
  3. Therefore, $\text{Con}(T) \text{ is provable in } T \rightarrow \lnot\text{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 Kolmogorov complexity.