Proof sketch of Gödel's incompleteness theorems

In this post, I will follow the outline of the proof given in Section VII of Nagel and Newman's book. Recall that:

• a formal system F is consistent if there is no well-formed formula (wff) w such that F proves both w and ¬ w, and
• a formal system is (semantically) complete if it can prove all of the true wff's that it can express.

Now, Gödel's first incompleteness theorem can be paraphrased as:

Any consistent formal system that is expressive enough to model arithmetic is both incomplete and "incompletable."

and Gödel's second incompleteness theorem can be paraphrased as:

Any consistent formal system that is expressive enough to model arithmetic cannot prove its own consistency.

According to Nagel and Newman, a proof of the first theorem can be sketched in 4 steps:

Mappings and the arithmetization of meta-mathematics

In an earlier post, we discussed mappings in general and then described Gödel numbering, which is a mapping between the set of well-formed formulas (wff's) in a formal system and the set of positive integers.

In part B of section VII, Nagel and Newman describe a more interesting mapping used in Gödel's proof. In this mapping, the domain is the set of meta-mathematical statements about structural properties of wff's, while the co-domain is the set of wff's. This post describes how this mapping enabled Gödel to arithmetize meta-mathematics.

Mappings and Gödel numbering

Section VI of Nagel and Newman's book describes mappings. A mapping is an operation that applies to two sets called the domain and the co-domain. More specifically, a mapping associates to each element of the domain one or more elements of the co-domain.

Absolute proof of consistency of FSN

In section IV of their great little book, Nagel and Newman discuss efforts by Gottlob Frege and then Bertrand Russell to reduce arithmetic to logic. This is clearly another attempt at a relative proof of consistency: if this reduction were successful, then arithmetic would be consistent provided logic is consistent.

Whether this latter statement is true or not, Whitehead and Russell's Principia Mathematica was a landmark achievement: it almost completed the first step in an absolute proof of consistency of arithmetic, since it led to the formalization of an axiomatic system for arithmetic.

In section V, Nagel and Newman describe a formalization of propositional (or sentential) logic, that is, a subset of the logic system in Principia Mathematica (but not a large enough subset to represent arithmetic). The bulk of this section first describes the formalization process, which yields the standard syntax and inference rules of propositional logic (including modus ponens) and then outlines an absolute proof of consistency of this formalized axiomatic system.

This absolute proof of consistency is a proof by contrapositive, which relies on the following true conditional statement:

Relative proofs of consistency

In the last post, we defined and explained the importance of the property of consistency for an axiomatic system. The second half of Section II in Nagel and Newman's book describes ways of proving that an axiomatic system is consistent.

But first, note that the question of consistency of Euclidean geometry did not arise. Its axioms were supposed to describe the real world; and something that actually exists cannot be self-contradictory. In other words, existence (or truth) implies internal consistency.

The need for consistency proofs arose much later, with non-Euclidean geometries, which do not obviously model space as we experience it. Non-existence does not imply inconsistency. But any interesting abstract construct had better be internally consistent.

Second, checking the internal consistency of all of the theorems produced so far is typically not a valid proof of consistency, because (interesting) axiomatic systems generate an infinite number of theorems. The proof of consistency must guarantee that not a single theorem, including some that we have not yet produced and that we might never produce, contradicts any other theorem in the system.

One possible way to prove the consistency of an axiomatic system is model-based, where a model is a kind of interpretation.

Consistency of axiomatic systems

The "problem of consistency" is the topic of Section II of Nagel and Newman's book.  This section defines "consistency" and explains when and why it became an important property of axiomatic systems.

The oldest and most famous axiomatic system is that of Euclid, in which he systematized all of the knowledge of geometry (and more) available to him over two thousand years ago. Based on five axioms, Euclid was able to rigorously prove a very large number of known and new theorems (called "propositions" in his Elements). His axioms were supposed to be intuitively true. The first four axioms dealt with line segments, lines, circles and angles (see this Wikipedia entry) and have been viewed as self-evident. In contrast, the fifth axiom, which was equivalent to the following statement: "Through a point outside a given line, only one parallel to the line can be drawn" (page 9), was not intuitively true (apparently because the two lines involved extend to infinity in two directions, similarly to asymptotes).

Since this proposed axiom was not obviously true, many mathematicians tried to prove that it logically follows from the first four axioms. Only in the nineteenth century was it demonstrated that it is NOT possible to prove the parallel axiom from the first four axioms.

This proof that it is impossible to prove a given statement is a great precursor of Gödel's incompleteness theorems.

Let's get started with Nagel and Newman (Section I)

Let's ease our way into this. I haven't read the Nagel and Newman book in a few years. But I remember it as a short and highly readable overview of the proof. I have a 1986 softcover edition by NYP Press. Today, I want to write about Section I - Introduction. It's really short: under 5 pages.

First, a short quote that makes me feel better about my past failures at REALLY understanding the proof of GIT:

I just want to understand the proof of Gödel's incompleteness theorems

So this is it! Summer 2013... This is when I get to master the proof of Gödel's incompleteness theorems (thereafter: GIT).

I discovered GIT as an undergraduate student in one of my Artificial Intelligence courses. My instructor was reading Gödel, Escher, Bach and was raving about the book. He even took some of our exam problems from it. But what I remember most is the outline of the proof of GIT, more precisely the first theorem. To be honest, the only part of it that stuck with me was the idea of numbering the formulas. Of course, at the time, I bought a copy of the book. I liked many parts of it but I never finished it.

Years later, while I was teaching computability theory and other computer science topics, I encountered GIT several times. At some point, I decided I wanted to understand the proof of GIT. 

First, I read the classic "Gödel's Proof" by Nagel and Newman. That is a concise and user-friendly overview of the proof. But it was only a proof sketch. So I looked at some textbooks on formal logic, which were neither concise nor user-friendly. I still did not understand the proof.

Finally, a couple of years ago, I came across a promising volume: "Introduction to Gödel’s Theorems" by Peter Smith. I read the first few chapters but then ran out of time (and motivation) to finish it. The following year, I made another attempt: I had to start from scratch and did not get any farther into it the second time around...