In this post, we present a sketch of Godel’s proof of his first incompleteness theorem. As the word sketch suggests, we will lay out the broad strokes of the proof without filling in many of the details. I personally find this level of description best for giving me an intuitive feel for the proof as a whole. Granted, that may only be true because I’ve already spent many hours pouring over the details and so I’m not troubled by the lack of rigor. Either way, I hope this will give you a high level understanding of how the proof goes. At the end, I will present links to further reading where you can fill in the details for yourself.

To start, let’s fix on a particular formal system, which we will call \(PM\). In the end, we will show that Godel’s proof applies to any sufficiently strong formal system, but we can leave generalizations for later.

First, Godel came up with an encoding scheme that can associate a unique number to any formula within \(PM\). In a similar way, he was able to associate a unique number with any proof (or derivation) within \(PM\). A formula’s number is sometimes called its “Godel number” (abbreviated as g.n.) and a proof’s number is called its “super g.n”.

Next, Godel constructed the following formula (with Godel number 421):

Formula 42: \(\lnot \exists m. \mathrm{Proof}(m, 42)\)

\(\mathrm{Proof}(m,n)\) is a relation between two numbers that is true iff \(m\) encodes a \(PM\) derivation (proof) of formula with number \(n\). Take it on faith, for now, that such a relation can be expressed within \(PM\).

If we intepret formula 42, it says the following:

It is not true that there exists a number m which encodes a \(PM\) proof of formula 42. In other words, formula 42 is not provable within \(PM\).

The problems that follow from formula 42 are probably somewhat self-evident, but for the sake of clarity let’s spell them out.

The semantic argument

Say we found a proof of formula 42 within \(PM\). Then formula 42, when interpreted, would make a false statement. It claims that no proof exists, and yet we found one. This is bad; we just proved a false statement within \(PM\). This means that \(PM\) is not sound, since a sound system can only derive true statements. To summarize, if we can prove formula 42, then \(PM\) is not sound. Contrapositively, if \(PM\) is sound, then \(PM\) cannot prove formula 42.

Let’s assume \(PM\) is sound and therefore it cannot prove formula 42. Now formula 42, when interpreted, makes a true statement! It claims that no proof exists, and indeed we cannot find one. The trouble in this case is that we’ve found a true statement that we cannot prove. We cannot prove a true statement, and therefore \(PM\) is incomplete.

That is not strictly true. What if we could prove the negation of formula 42? Wouldn’t that undermine the claim that \(PM\) is incomplete? After all, incompleteness just means you can derive either \(\varphi\) or \(\lnot \varphi\), for any formula \(\varphi\).

We can show, using similar arguments, that we cannot prove the negation of formula 42. We have already shown that if \(PM\) is sound, then it cannot prove formula 42, which means that formula 42 is true. That implies that the negation of formula 42 is false. A sound formal system can only prove true statements, so again - assuming \(PM\) is sound - it cannot prove the negation of formula 42 either.

This completes a sketch of what’s called the semantic argument. It says that if a formal system is sound and sufficiently expressive, then it is incomplete. Of course we’ve left out all the details. We haven’t shown why a sufficiently expressive formal system can indeed express the \(\mathrm{Proof}\) relation. Even after that, it takes considerable mental acrobatics to construct formula 42 such that its own Godel number happens to be the same number for which it claims there is no proof. Lastly, we have not shown Godel’s numbering scheme, although that part is relatively straightforward.

Notice that the semantic argument derives incompleteness from a sound and sufficiently expressive formal system, whereas the Godel’s incompleteness theorem claims that consistent and sufficiently strong formal systems are incomplete. The argument that derives incompleteness from a consistent and sufficiently strong formal system is called the syntactic argument. It’s considerably more involved, so it’s worth pausing to reflect that the semantic argument should be quite satisfying! Any formal system that we hope to use as a foundation for all of mathematics had better be sound. Otherwise, it’s able to prove formulas that make false statements, which doesn’t sound like a great fit. So, if you try to follow the syntactic argument below and find that your brain is left looking like a pretzel, you can rest easy knowing that the semtantic argument is “good enough”.

The syntactic argument

The syntactic argument does not assume that \(PM\) is sound, only that it is consistent. Consistency is a weaker requirement than soundness, which is what makes this argument more impressive. However, in weaking one requirement, it needs to strengthen another. Instead of requiring that \(PM\) is sufficiently expressive, it requires that it’s sufficiently strong. Remember that sufficiently strong means that \(PM\) can not only express all primitive recursive relations, but that it can capture them. Here is a refresher on what it means to capture a property (or relation) \(P\).

A formal system \(T\) can capture a property \(P\) by the open formula \(\varphi(x)\) iff, for any \(n\):

  • if \(n\) has the property \(P\), then \(T \vdash \varphi(\bar{n})\), and
  • if \(n\) does not have the property \(P\), then \(T \vdash \lnot \varphi(\bar{n})\)

If \(PM\) is consistent (and sufficiently strong), then \(PM\) cannot prove formula 42

Say we found a proof of formula 42 within \(PM\). Let’s compute the super g.n. of that proof and call it \(p\). We can now derive the formula \(\mathrm{Proof}(p, 42)\) within \(PM\). It’s easy to miss, but here is where we needed the requirement that \(PM\) is sufficiently strong and therefore can capture any primitive recursive relation. If \(PM\) can capture the \(\mathrm{Proof}\) relation, then \(PM \vdash \mathrm{Proof}(p, 42)\).

Formula 42 states \(\lnot \exists m. \mathrm{Proof}(m, 42)\) which is equivalent to \(\forall m \lnot \mathrm{Proof}(m, 42)\). If we instantiate the \(\forall m\) quantifier with the number \(p\), we get \(\lnot \mathrm{Proof}(p, 42)\).

In summary, if we find a proof of formula 42 with super g.n. \(p\), \(PM\) can derive both \(\mathrm{Proof}(p, 42)\) and \(\lnot \mathrm{Proof}(p, 42)\). In other words, if we can find a proof of formula 42, then \(PM\) is inconsistent. Contrapositively, if \(PM\) is consistent (and sufficiently strong), then \(PM\) cannot prove formula 42.

If \(PM\) is consistent, then \(PM\) cannot prove \(\lnot\) formula 42

In order to derive incompleteness, we also need to show that \(PM\) cannot derive the negation of formula 42. In the semantic argument, this was easy. We relied on the fact that if \(PM\) could not prove formula 42, then formula 42 was true, and therefore \(\lnot\) formula 42 was false, and a sound formal system cannot prove false statements. QED.

In the syntactic argument, it’s not so easy. This is where the details get particularly subtle. We need to take a small digression to explain the idea of \(\omega\)-consistency.

\(\omega\)-inconsistency:

A theory T is \(\omega\)-inconsistent iff, for some open formula \(\varphi(x)\), \(T \vdash \exists \varphi(x)\) and yet for every number \(m\) we have \(T \vdash \lnot \varphi(m)\).

\(\omega\)-inconsistency is a Very Bad Thing (TM). It basically says that you can prove something is not true for every single number, but also you can prove that there exists “some” number for which it’s true. In the same way that any useful formal system should be consistent, it should also be \(\omega\)-consistent. Note that \(\omega\)-consistency is a stronger requirement than plain consistency; \(\omega\)-consistency implies plain consistency, but plain consistency does not imply \(\omega\)-consistency.

We will now try to finish the syntactic argument, using the stronger assumption that \(PM\) is \(\omega\)-consistent.

If \(PM\) is \(\omega\)-consistent, then \(PM\) cannot prove \(\lnot\) formula 42

Say that \(PM\) is \(\omega\)-consistent and we can find a proof of \(\lnot\) formula 42. If \(PM\) is \(\omega\)-consistent, then it is also consistent, meaning that it cannot prove formula 42.

If \(PM\) cannot prove formula 42, we know that, for any \(m\), \(\lnot \mathrm{Proof}(m, 42)\), otherwise we’ve found the proof of formula 42 within PM.

Recall the definition of formula 42 is \(\lnot \exists m. \mathrm{Proof}(m, 42)\). So \(\lnot\) formula 42 is equivalent to \(\exists m. \mathrm{Proof}(m, 42)\).

Now let’s bring the argument home. Say that \(PM\) can prove \(\lnot\) formula 42, which is equivalent to \(\exists m. \mathrm{Proof}(m, 42)\). If \(PM\) is consistent, then it cannot also prove formula 42, which means that for any \(m\), it can prove \(\lnot \mathrm{Proof}(m, 42)\). The ability to prove \(\lnot \mathrm{Proof}(m, 42)\), for any \(m\), as well as \(\exists m. \mathrm{Proof}(m, 42)\) would mean that \(PM\) is \(\omega\)-inconsistent. Contrapositively, if \(PM\) is \(\omega\)-consistent, then it cannot prove \(\lnot\) formula 42.

This completes a sketch of the the syntactic argument. We’ve demonstrated if \(PM\) is \(\omega\)-consistent and sufficiently strong then it cannot derive either formula 42 or the negation of formula 42, making it incomplete.

If you think that a bait-and-switch just occurred where we promised to derive incompleteness from consistency but instead assumed \(\omega\)-consistency, you’re 100% correct. Godel’s 1931 proof did in fact require \(\omega\)-consistency to complete the syntactic argument. However, in 1936, John Barkley Rosser proved Rosser’s trick, which showed that the requirement for \(\omega\)-consistency may be weakened to consistency.

Filling in the details

In the proof sketch above, I asked you to take a few things on faith. One, that we could associate a unique number with any formula or proof within PM. Next, that the \(\mathrm{Proof}\) relation could be expressed and even captured within PM. Finally, that we can construct “formula 42” (usually called the Godel sentence \(G\)) such that it’s own Godel number is 42 and it claims that there is no proof of the formula with number 42.

Originally, I had planned on filling in each of these details with additional posts. However, filling in these details in a rigorous way requires a full book (which I read, it’s called An Introduction to Gödel’s Theorems by Peter Smith). So instead of trying to explain these details myself at some intermediate level of rigor, which may or may not satisfy you, I’m going to reference you to specific points at the book that explain each point. Not only will that likely be a better explanation, but if it doesn’t make sense or you require more background, you’ll have an entire book to fall back on. Without further ado:

  1. Two formalized arithmetics

    Everything we’ve talked about up to now has talked about “formal systems” in general, but I found it quite helpful to see the specifics of a few concrete formal theories of arithmetic. In chapter 10, Smith introduces \(BA\) (Baby Arithmetic) and then \(Q\). A few chapters later, Smith introduces First-order Peano Arithmetic or \(PA\) (Note: \(PA\) and the \(PM\) system which I refer to above are essentially the same).

  2. Godel Numbering

    For whatever reason, I find this detail relatively straightforward. It’s nice to see the details worked out, though.

  3. The \(\mathrm{Proof}\) relation can be expressed

    This is done in two steps. First, you show that the \(\mathrm{Proof}\) relation is primitive recursive (19.4 and 20.4). Then, you show that your formal system can express all primitive recursive relations (15).

  4. The \(\mathrm{Proof}\) relation can be captured

    I found this part of the proof to be, by far, the hardest to follow. I wish I could give you a two sentence explanation of the key insight here, but I’m not really sure what it is. Sometimes you just have to sit and stare at something until it finally clicks.

    In chapter 17, Smith shows that any primitive recursive function or relation (including the \(\mathrm{Proof}\) relation) can be captured by \(Q\), and hence in \(PA\). Most of the heavy lifting of this proof is done by invoking Theorem 11.5 that states that \(Q\) is \(\Sigma_1\)-complete.

    Here’s my best attempt at describing what clicked for me: The proof of Theorem 11.5 shows that \(Q\) is \(\Sigma_1\)-complete, which means that every \(\Sigma_1\) formula can be either proven or disproven in \(Q\). I think I was expecting the proof of this statement to show me how to prove any arbitrary \(\Sigma_1\) formula, but that’s not what’s being claimed. How you show that a true \(\Sigma_1\) formula can be derived is extremely unsatisfying. If you have a true formula that says “there exists some \(x\) for which \(P(x)\) is true”, you can prove that by finding a specific \(x\) for which it’s true and then adding the existential quantifier at the front. But finding that specific \(x\) for which \(P(x)\) is true might be insanely hard.

    Let’s say that Goldbach’s conjecture is false. Namely, “there exists some even number greater than two that is not the sum of two primes”. If that statement is true, then it’s provable within \(PA\). How would you prove it? Step 1: find an even number greater than two that is not the sum of two primes. Step 2: From that instance, derive the existential statement. Step 1 may take you a while.

  5. Constructing Godel’s sentence

    The final coup d’etat comes in Chapter 21: \(PA\) is incomplete. In this chapter, Smith shows how to construct Godel’s version of “formula 42” which claims (about itself) that it has no proof.

And with that, I conclude my series on Godel’s First Incompleteness Theorem!

  1. His actual formula most certainly did not have a Godel number of 42. Normally, people refer to the number of his formula with the letter \(G\), but I find having a concrete number makes my brain hurt just a bit less. ↩