An Exposition of Gödel’s First Incompleteness Theorem

Eric Zheng <ericzheng@cmu.edu>
(Version 1)

Impossible. Perhaps the archives are incomplete.

Obi-Wan Kenobi

Introduction

In this document, I’d like to make an informal presentation of Gödel’s first incompleteness theorem, a very beautiful result of mathematical logic. The discussion is inspired by Douglas Hofstadter’s famous book Gödel, Escher, Bach: An Eternal Golden Braid, except very much condensed. In fact, there is little original content; my aim is to collect in an accessible format what I consider to be the key parts of Hofstadter’s presentation of Gödel’s proof, which are scattered throughout the several hundred pages of his book.

Firefox reader claims that this document should take roughly twenty minutes to read. However, my prose is not always the clearest, so it may take longer. I expect that the reader has some mathematical background about equal to a first semester college course in pure mathematics; for example, familiarity with propositional logic is assumed.

Statement of the Theorem

Gödel’s theorem describes a fundamental limitation in the power of any “sufficiently powerful” axiomatic system. What is meant here by “sufficient power” is that the system is expressive enough to represent statements of number theory, such as “four times five equals twenty” and “ten is not a prime number”. When we speak of number theory, we are interested here in only the natural numbers.

Specifically, Gödel proved the following:

As defined above, no sufficiently powerful axiomatic system can be both consistent and complete.

We’d better define what we mean by consistency and completeness:

Summary of the Proof

Gödel proved his theorem by combining a few ingenious ideas:

I will elaborate on each of these ideas, but their end goal is to produce the Gödel sentence G which is a logical statement that asserts:

The statement G is not a theorem of number theory.

It is not immediately obvious whether G is a theorem of number theory or not. Either way, the construction of such a sentence exposes a deep flaw in any axiomatic system that is powerful enough to express number theory.

Now if G is indeed a theorem of number theory, then we are in deep trouble, since if number theory is sound (i.e. its theorems are true), then G asserts that it is not a theorem of number theory, which is a contradiction. Thus the arithmetic of the natural numbers would be proven inconsistent, which is a rather unpleasant result.

But on the other hand, if G is not a theorem of number theory, then we must concede that G is a true statement. We have proven the incompleteness of any axiomatic system of number theory: there is a true statement G which is not a theorem of our system!

Typographical Number Theory

To speak about Gödel’s proof, it is useful to have a reference axiomatic system so that we may talk concretely about statements of number theory. There are many axiomatic systems that are powerful enough for this task, such as the Zermelo-Fraenkel set theory or the system of Whitehead and Russell’s Principia Mathematica. In keeping with Hofstadter, I will use a modified version of the system that he calls typographical number theory.

In the modified typographical number theory (mTNT), we represent each number using tagged tally marks. For example, we can represent the number 1 as {1} and the number 7 as {1111111}. The number 0 is represented by the empty tally {}. We will additionally define the addition (+), multiplication (×), and equality (=) operators with their usual meaning.

Onto this basic framework of natural numbers we bolt the machinery of propositional logic, such as the universal and existential quantifiers ∀ and ∃. Significantly, we add variables such as a, b, c, and so on. We need not worry about running out of symbols for variable names, since we can always produce a new variable name by appending a prime (’) to another variable name. In fact, it would suffice to name all our variables a, a’, a’’, and so on, but it is pointless to strain the reader’s eyes with this strict notation.

What are the axioms and rules of inference of mTNT? We will not make them explicit (it is not the purpose of this document to build a new formalization of number theory), but one can imagine fleshing out the system with a scheme similar to the Peano arithmetic and usual laws of propositional logic.

Nothing presented in the rest of the proof will be tied to our choice of mTNT; the techniques that Gödel employed are quite general and apply to any similarly powerful axiomatic system.

Gödel Numbering

The idea of Gödel numbering is a simple but powerful one: let us associate with each typographical symbol a unique number. Once we do this, every statement of number theory itself becomes a number! For example, consider the statement “seven is prime”. We can represent this statement in mTNT as:

¬((∃a,b)(a×b={1111111} ∧ ¬(a={1} ∨ b={1})))

or “there do not exist natural numbers a and b such that a×b=7 and neither a nor b is 1”. The numerical assignment for each symbol is arbitrary; for instance, we might let a left parenthesis be 23, and we might let a right curly brace be 17. As long as the encoding is unambiguous, all that matters is this:

Any statement of number theory can be expressed as a finite string of symbols taken from a finite alphabet. Hence it is possible to associate each statement with a unique number, which we will term its Gödel number.

In fact, a particularly nice way of interpreting this fact (at least to a programmer) is that if our alphabet has, say, N symbols, then every statement of number theory that is expressible in our axiomatic system becomes one massive base-N number: that statement’s Gödel number.

What does this insight net us? Well, since each statement is now a number, we can do arithmetic on statements! We get a new way of interpreting our axiomatic system: statements about arithmetic are now statements of arithmetic as well. To give a concrete example, consider the following somewhat trivial rule of propositional logic:

If a statement of the form ¬(¬P) is a theorem of mTNT, then so is P.

This is just the rule of double negation. Now suppose we encode logical negation “¬” as the number 78, left parenthesis “(” as the number 17, and right parenthesis “)” as the number 15. Then we can consider the following analogous rule about p, which is the Gödel number of P:

If a number of the form 781778p15 is the Gödel number of a theorem of mTNT, then so is the number p

At first, this doesn’t seem terribly useful, but recall that any natural number can be represented within mTNT using the curly brace notation. For example, we can speak of the theorem ¬(¬P) by referring to the number {111⋯111}, where there are 781778p15 of the 1’s in the curly braces. (Note here that p is not a variable of mTNT but a specific, rather large number.) This is very unwieldy, but it means that we can refer implicitly to statements of number theory within other statements of number theory, which is the first major stepping stone in Gödel’s proof.

Proof Pairs

In order to construct the Gödel sentence G, we need to figure out how to represent the notion of theoremhood within number theory itself. To do this, we introduce the concept of proof pairs. We say that the natural numbers (m,n) form a proof pair if and only if m is the Gödel number of a valid derivation in mTNT and n is the Gödel number of the last line of that derivation.

To give an example of what I mean by a derivation, consider again the rule of double negation. We will introduce a punctuation mark “.” into mTNT to separate statements in the derivation. Now define (m,n) via:

m is the Gödel number of “¬(¬(¬(¬P))).¬(¬P).P”

n is the Gödel number of “P”

Now is (m,n) a valid proof pair? Well, assuming that the first line ¬(¬(¬(¬P))) is a valid axiom of mTNT, then the answer is yes, because:

  1. The derivation corresponding to m is a valid one. In particular, each line follows logically from the preceding ones according to the rules of mTNT: it is just two applications of the rule of double negation. (Technically, there is also the matter of lifting the parenthesis, but we will not get bogged down in details.)
  2. The last line of the derivation corresponding to m is P, whose Gödel number is indeed n.

It is important to note that checking whether (m,n) is indeed a proof pair is in general a very trivial (if tedious) mechanical process:

  1. Is m indeed a valid derivation of mTNT? We need to check that the statement whose Gödel number is m is well-formed and that each line in the derivation follows logically from the previous ones using the axioms that we have.
  2. Is n indeed the last line of the derivation given in m? This is very easy to check.

The key point is that these two checks involve a finite, bounded number of steps; the process is long and boring but is ultimately an arithmetical one that is guaranteed to terminate within a certain bound. Because of this, it is one of the so-called “primitive recursive” properties of computer science. Another example of a primitive recursive property is primality.

What is remarkable about primitive recursive properties is that they can all be expressed as predicates within mTNT. I do not know the proof of this fact, but it means that there exists some predicate, probably very complicated, that we shall call PROOF-PAIR(m,n), which is true if and only if the natural numbers m and n form a proof pair. Armed with such a predicate, it becomes simple to represent within mTNT the property of theoremhood for a statement with Gödel number b: define the predicate IS-THEOREM(b) to be equivalent to (∃a)(PROOF-PAIR(a,b)). In other words, “there exists some natural number a which forms a proof pair with b”.

Quining and the Epimenides Paradox

What we ultimately want to do is to construct a sentence that is very similar to the following paradoxical statement attributed to the Greek philosopher Epimenides:

This sentence is false.

At this point, we have made several important advances toward our goal of constructing the Gödel sentence G: we have figured out how to get mTNT to talk about itself, and we have figured out how to represent the notion of theoremhood within mTNT. The tricky part that remains is to figure out how to achieve self-reference in a statement of number theory—to construct a statement that talks about its own theoremhood.

To do this, we turn to a concept that is probably familiar to a reader who enjoys computer programming puzzles: that of quining. (In the language of mathematics, such an argument is typically called diagonalization after a famous proof by Cantor, but in keeping with Hofstadter I will use the programming term.) In programming, a quine is a program that prints out its own source code. This is commonly accomplished by preceding (or succeeding) a program by its own quotation, an action that we shall call “quining”. For instance, the quine of “is a sentence fragment” is:

“is a sentence fragment” is a sentence fragment.

Now quining ordinary statements usually leads to some hilarity, because the resulting statements often make little sense. But something curious occurs when we quine a statement that itself speaks about the act of quining. Consider quining the statement “when quined, is false”:

“when quined, is false” when quined, is false.

But this is precisely “when quined, is false” when quined! Hence this is a sentence that is its own subject: an unusual form of self-reference that does not rely on slippery phrases of the English language such as “this sentence”. A closer inspection reveals that this is quite analogous to the Epimenides paradox, and it gives us a blueprint for how to achieve the same effect within mTNT.

Constructing the Gödel Sentence

We are finally ready to construct G. We will first construct a predicate of mTNT, with one free variable, that corresponds to the statement “when quined, is false”. To do this, we will need a way to talk about quining within mTNT. The analogous operation to quining within mTNT is to replace all free variables within a statement with that statement’s own Gödel number. For example, consider the statement a=1, which is represented within mTNT as:

a={1}

Now suppose our numbering scheme leads to this statement’s Gödel number being 123456. Quining this statement then leads to 123456=1, or within mTNT:

{111⋯111}={1}

where there are 123456 of the 1’s within the curly braces. Clearly, this is a nonsensical statement, very much like most English phrases, which are nonsensical when quined. But we use this example to illustrate the tools needed to use quining in mTNT.

Let us call a natural number b the quine of the natural number a if and only if b is the Gödel number of a statement which is obtained by quining the statement whose Gödel number is a. Now quining is a simple arithmetical substitution; like proof pairs, it is easy but tedious to check if some number b is the quine of a. In fact, such a check is bounded, which implies that quine-hood is a primitive recursive property. As with proof pairs, there is a predicate of mTNT that is capable of checking whether b is the quine of a. We aren’t interested in its exact form; we will refer to this predicate opaquely as IS-QUINE(a,b).

Now we will construct the mTNT analogue of the phrase “when quined, is false”. Consider the statement:

¬(∃b)(IS-THEOREM(b) ∧ IS-QUINE(a,b))

Let us call this statement G0. In English, this statement says that “there does not exist a b such that b is the Gödel number of a theorem of mTNT and b is the quine of a”: a statement which speaks of quining. All that is left to do is to quine this very statement. Suppose the Gödel number of G0 is g. Then the Gödel sentence G, in all its glory, is:

¬(∃b)(IS-THEOREM(b) ∧ IS-QUINE(g,b))

This looks very similar to G0, except that we have replaced the free variable a with the concrete number g. In English, this says that “there is no number b that corresponds to both a theorem of mTNT and the quine of G0”, or more clearly: “the quine of G0 is not a theorem of mTNT”. But what is the quine of G0? G itself! Thus, G asserts precisely:

G is not a theorem of mTNT.

This was our goal from the beginning: we have transplanted the Epimenides paradox into mTNT, thus proving that it (and any system of similar power) cannot be both consistent and complete. □

Some Implications of the Theorem

Gödel’s theorems were the first in a series of profound results in meta-mathematics that were discovered in the early twentieth century. Other famous results of similar nature include Tarski’s theorem about the non-representability of truth and Turing’s proof that the halting problem is undecidable.

In particular, Gödel threw quite the wrench into the efforts of David Hilbert, one of the preeminent mathematicians of the nineteenth and twentieth centuries. Hilbert, and many others, had proposed to undertake the ambitious program of formalizing all known mathematics under a single axiomatic system. This would be quite the crowning achievement: all of human mathematical knowledge unified under a single system! The mathematicians of the time wanted to do for all of mathematics what Euclid had tried to do for plane geometry two millennia ago.

Unfortunately, Gödel poked a rather large hole in their efforts by proving that such a system was impossible. That is not to say that there are not useful “foundations of mathematics”, such as set theory and category theory, but that we must be keenly aware of the shortcomings of any such formalization. There are also interesting philosophical arguments about knowledge and intelligence that can be derived from Gödel’s theorems (and other theorems of meta-mathematics); Hofstadter gives the example (and provides a counter-argument) of Lucas’s argument for the existence of souls.

The fields of meta-mathematics and philosophy are rich with similarly interesting problems, but these are well beyond the scope of this document (and indeed, beyond the ken of its author).

References

A lot of the information in this document came from Hofstadter. If this document was vaguely interesting, I’d recommend reading his book Gödel, Escher, Bach: An Eternal Golden Braid. I also referenced the Wikipedia article for Gödel’s incompleteness theorems when writing this document.