21. Gödel's Incompleteness Theorems

Back in Lecture 18, we identified four properties that we want sets of axioms to satisfy:

We saw in that lecture that there are sets of axioms that satisfy all four of these properties for some theories like Euclidean planar geometry and addition-only arithmetic. But we are now ready to prove Gödel’s Incompleteness Theorems which show that we can not expect to achieve such success when considering sets of axioms for richer theories.

TM-expressive Sets of Axioms

Our first task before we can state Gödel’s incompleteness theorems is to formalize what we mean by “richer theories”. Or, to phrase it differently, we need to define what is the condition that sets of axioms must satisfy so that they are “sufficiently expressive” for the incompleteness theorems to apply to them. There are various ways to do this, but the condition boils down to whether or not a set of axioms can be used to express properties of Turing machines.

Definition. The set of axioms \(\Gamma\) is TM-expressive if there is a computable function \(\mathsf{Encode} \colon (\left< M \right> x ) \mapsto \phi_{M,x}\) which produces a sentence \(\phi_{M,x}\) that satisfies \(\Gamma \vDash \phi_{M,x}\) if and only if \(M\) halts on input \(x\).

The ZFC axioms for set theory are general enough to enable most mathematical statements to be encoded as sentences in that theory. So it is not too surprising that we can encode statements about Turing machines using these axioms. Perhaps more surprising is that the Peano axioms for arithmetic (with both addition and multiplication) are also general enough to encode Turing machines.

Lemma. The set of Peano axioms is TM-expressive. As a consequence, any set of axioms that is sufficiently expressive to encode statements about Peano arithmetic (including the set of ZFC axioms) is also TM-expressive.

Gödel’s First Incompleteness Theorem – Initial Version

We can now use the uncomputability of the Halting problem to prove an initial version of Gödel’s First Incompleteness Theorem.

Gödel’s First Incompleteness Theorem. (Initial version.) Every set of axioms \(\Gamma\) that is TM-expressive, computable, and sound must be incomplete.

Proof. Assume on the contrary that there exists a set of axioms \(\Gamma\) that is TM-expressive, computable, sound, and complete.

Consider the following algorithm A that takes \(\left<M\right>,x\) as input:

Since \(\Gamma\) is TM-expressive, the function \(\mathsf{Encode}\) is computable. And since \(\Gamma\) is computable, the function corresponding to deciding if a string is a valid formal proof is also computable. So the entire algorithm can be implemented with a Turing machine.

Since \(\Gamma\) is complete, there must exist a formal proof of \(\phi_{M,x}\) or of \(\neg \phi_{M,x}\) for any machine \(M\) and string \(x\), so the Turing machine that implements this algorithm always halts.

Finally, since \(\Gamma\) is sound, the algorithm outputs Yes when \(M\) halts \(x\) and No when it does not.

But this means that the algorithm we just described corresponds to a Turing machine that computes the \(\mathsf{Halting}\) function. And, as we have seen in the last lecture, no such algorithm exists. Therefore, by this contradiction we see that our initial assumption must be incorrect, and so \(\Gamma\) cannot be complete if it is TM-expressive, computable, and sound.

This version of Gödel’s First Incompleteness Theorem can be rephrased to say that for every set of axioms \(\Gamma\) that is TM-expressive, computable, and sound, there is a sentence \(\phi\) that is a logical consequence of \(\Gamma\) but is not implied by it. Or, to put is more informally: there is a theorem that is True in \(\Gamma\) but does not have a proof.

Gödel’s First Incompleteness Theorem – Stronger Version

We can strengthen Gödel’s First Incompleteness Theorem by showing that replacing the soundness of the set of axioms in the theorem statement with consistency still leads to incompleteness.

To prove this theorem, however, we first need to make a basic observation.

Proposition. For every set of axioms \(\Gamma\) that is TM-expressive and every Turing machine \(M\) that halts on the input string \(x\), there is a formal proof that \(\Gamma \vdash \phi_{M,x}\).

Proof sketch. We won’t cover the details but the main idea is that a formal proof that \(M\) halts on \(x\) simply needs to show the transcript of \(M\)’s execution on the input \(x\).

In other words, the proof first specifies that initially the tape content is \(x\), the tape head is on the first symbol of \(x\), and the internal state of \(M\) is its initial state. Then after one step of execution, the string on the tape, the position of the tape head, and the current internal state are all completely determined by the transition function of \(M\). This can be asserted with sentences in the theory of \(\Gamma\). And after two steps, we can again specify the full configuration of \(M\) and verify that it obeyed the transition function.

The proof specifies the configuration at each step of the computation of \(M\), gives justification showing that each of these steps obeys the transition function, and finally demonstrates that the final configuration in the transcript is in the special Halt state.

We are now ready to complete the full version of the first incompleteness theorem.

Gödel’s First Incompleteness Theorem. (Stronger version.) Every set of axioms \(\Gamma\) that is TM-expressive, computable, and consistent must be incomplete.

Proof. Fix any set of axioms \(\Gamma\) that is TM-expressive, computable, and consistent.

Consider the following Turing machine that we will call \(D\) and which interprets its input as the encoding \(\left<M\right>\) of a Turing machine \(M\).

Once again, we use the fact that \(\Gamma\) is TM-expressive and computable to justify the claim that \(D\) does indeed correspond to a valid Turing machine.

Now for the key question: what does \(D\) do on the input \(\left< D \right>\)?

If \(D\) halts, it must be because it found a formal proof showing that \(\Gamma \vdash \neg \phi_{D,\left<D\right>}\). But, as we have seen in the Proposition above, if \(D\) halts on input \(\left<D\right>\), then we can also find a formal proof showing \(\Gamma \vdash \phi_{D,\left< D \right>}\). So this possibility contradicts the claim that \(\Gamma\) is consistent.

And if \(D\) does not halt because it finds a proof that \(\Gamma \vdash \phi_{D,\left< D \right>}\), then by the same reasoning as in the proof of the last proposition we can also find a proof that \(D\) reaches the special infinitely looping state, and therefore does not halt. Therefore, we can also find a proof of \(\Gamma \vdash \neg \phi_{D,\left<D\right>}\), again contradicting the consistency of \(\Gamma.\)

This means that the only possibility that is not ruled out in the execution of \(D\) on input \(\left< D \right>\) is that it runs forever, never finding a proof of \(\phi_{D,\left< D \right>}\) or of \(\neg \phi_{D,\left< D \right>}\). But this means that \(\Gamma\) is not complete.

Gödel’s Second Incompleteness Theorem

Gödel’s First Incompleteness Theorem shows that for every set of axioms \(\Gamma\) that is TM-expressive, computable, and consistent, there must exist some sentence \(\phi\) for which we can not obtain a formal proof of \(\phi\) or of its negation \(\neg \phi.\) But can we identify a specific sentence that satisfies this conclusion?

As it turns out, if we review the proof of the stronger version of the First Incompleteness Theorem carefully, we notice that we are very close to answering this challenge. Namely, we see that the specific conclusion of the argument can be phrased as follows:

If \(\Gamma\) is consistent, then \(D\) does not halt on input \(\left< D \right>\).

But now there are two key observations that we can make.

  1. That statement is a simple if-then conditional sentence. So if we can obtain a formal proof of the sentence that encodes “\(\Gamma\) is consistent”, we can use the Conditional Elimination rule to obtain a proof of the sentence “\(D\) does not halt on \(\left< D \right>\)”.
  2. … but the argument also shows that we can not obtain a formal proof of the sentence \(\neg \phi_{D, \left<D\right>}\) that encodes that statement!

From those two observations, we immediately obtain Gödel’s Second Incompleteness Theorem.

Gödel’s Second Incompleteness Theorem. For every set of axioms \(\Gamma\) that is TM-expressive, computable, and consistent, the sentence \(\phi\) that encodes the true statement “\(\Gamma\) is consistent” does not have a formal proof whose premises are all in \(\Gamma\).

Informally, this theorem states that a sufficiently strong set of axioms that is computable and consistent necessarily is not able to prove its own consistency. If we want to do so, we will need to consider a larger set \(\Gamma'\) of axioms. But then, if we want to be sure that this proof of the consistency of \(\Gamma\) is correct, we may want to prove that \(\Gamma'\) is consistent. And if we want to do so, we will need to consider an even larger set \(\Gamma''\) of axioms. Etc., etc., etc.