Gödel's First Incompleteness Theorem -- an intuitive sketch of the proof

In the early 20th century, Whitehead and Russell published a book called Principia Mathematica. In it the authors attempted to derive all mathematical truths from a finite set of axioms and rules of inference. The consensus amongst mathematicians at the time was that this was doable, and that it would make mathematics a lot more rigorous than it is even now.

But Gödel proved that such attempts would always end in vain. Gödel's First Incompleteness Theorem states that any consistent formal system strong enough to contain the natural numbers is incomplete. In other words, there will always be a mathematical statement whose truth value Principia Mathematica would not be able to determine.

Gödel showed this in a sneaky way, yet the logic of his proof is actually not too complicated. Essentially what Gödel did was to translate Epimenides's paradox ("this statement is false") into a formal language. I will give an intuitive and informal sketch of the proof below.

Preliminaries

A formal system consists of a formal language (a set of words/symbols, with some sort of formal grammar), and a set of rules of inferences that can be applied to an axiom or a previously derived theorem. Here, a theorem is just a statement in the formal language that is derivable from either an axiom or from a previously derived theorem. The rules of grammar and rules of inferences need to be algorithmic, meaning that one should be able to apply the rules symbolically or syntactically, without looking at the semantics.

This algorithmic aspect of grammar and rules of inference are important in determining what is expressible in the system. An English statement is expressible in our formal system if there is a statement in the formal language that have the same interpretation -- that is, we can "translate" the English sentence into a statement in our formal language.

We will assume here that our formal system is strong enough to contain the natural numbers, and that concepts such as equality, addition, existence, etc... can be expressed in it.

Expressibility of theoremhood and proofs

The most important aspect of Epimenides' paradox is self-reference. If we are to create self-reference in our formal system -- specifically self-reference about truth-hood -- we must be able to express the notion of a theorem and a proof within the formal system. Gödel showed that we can.

Statements in our formal system are nothing but a series of symbols in our formal language. But there is nothing special about the actual symbols being used. In particular, we can use natural numbers to replace those symbols. As a very arbitrary example, if we are using symbols "=", "1", and "0", we can replace every instance of "=" with 131, "1" with 101, "0" with 100 etc. Then our statement "1=1" becomes 101131101, and 101131100 can be interpreted as "1=0". Similarly, we can translate any statement in our formal system into a natural number. This natural number is commonly referred to as the Gödel numbering of a statement.

Likewise, a proof of a theorem is no more than a sequence of statements, with some special properties: that every statement in the sequence is either an axiom, or derived via a rule of inference from a previous statement in the sequence. We can represent a proof P using a natural number as well, by concatenating the Gödel numberings of each statement.

Now, note the following:

(1) Since our rules of grammar are algorithmic, it is possible to check algebraically whether a natural number S is a Gödel number of a syntactically correct statement ("=32" is not syntactically correct, whereas "1=2" is).

(2) Since our rules of inferences are algorithmic, we can translate these rules into numerical operations. We can hence check (algorithmically) whether a natural number P is a valid "proof" for a "statement" S, another natural number.

This is enough to show that the notion of proofs is expressible in our formal system -- we can make a statement called Proof(P,S) that is true if and only if P is a valid "proof" for the "statement" S (note P and S are both natural numbers). Now, the statement Provable(S) := There exists P such that Proof(P,S) would be true if and only if S is provable. We have succeeded in expressing provability inside our formal system.

The Fun Part!

A free variable is a variable that is not defined in the statement. For example, in the statement "b+b=2", b is a free variable. Let's call a statement with one free variable a class-sign. Some examples of class-signs are "a+0=1", and "there exists b such that b*b=a". Examples of non-class-signs are "1+1=2", "there exist b such that b+b=2" and "a+a=b".

We can assume that these class-signs are somehow ordered and numbered, say R_n is the nth class-sign*. We can also use R_n(k) to denote the statement one gets when replacing the free variables in R_n with a known number k. Again as an arbitrary example, if R_2 is the statement "a+0=1" then R_2(10) is the statement "10+0=1". If R_9 is the statement "there exists b such that b*b=a", then R_9(9) is the statement "there exists b such that b*b=9".

Now let's define a set K consisting of natural numbers. A natural number n is in K if and only if R_n(n) is not provable. That is, n is in K <=> ~Provable(R_n(n))

As before, R_n(n) is the statement you get when you substitute the free variable in R_n with the natural number n. In the example above, R_2(2) is an unprovable statement "2+0=1", so 2 would be in K. In contrast, R_9(9) is a provable statement "there exists b such that b*b=9", so 9 would NOT be in K. **

Note that checking provability, finding the ordering of the class-signs, and everything else we've done thus far are algorithmic operations. This is important, because it implies that the statement "n is in K" is expressible in our formal system -- that there is a statement in our formal system that corresponds to "n is in K".

But this statement "n is in K" has only one free variable, namely n, so it is a class-sign! So we can make the following modus ponens argument:

(1) "n is in K" is a class sign

(2) Class signs are enumerated by R_n

.'. (3) there must be a natural number q with R_q = "n is in K"

Now the question is, is q in the set K?

The Pitfall

If q is in the set K, then R_q(q) is not provable. But R_q(q) is the statement "q is in K", which must be true by assumption -- a contradiction. If q is not in the set K, then R_q(q) must be provable, which means q must be in the set K -- again we have a contradiction. This is Epimenides' paradox, and the statement "q is in K" is the undecidable proposition that will forever stump Principia Mathematica.

What this proof is missing

The construction I followed is from a translation of Gödel's paper, which contains the rigorous proof as well as a quick sketch. It has the advantage of providing a quick proof without complicated constructions. I tried to also take ideas from a more elegant (but time-consuming) construction in Hofstadter's book, Gödel Escher Bach. Hofstadter puts more emphasis on core concepts that are quite well hidden here, such as the concept of quining. Hofstadter also writes about the consequences of Gödel's theorem in philosophy, biology, and AI, which is nothing short of being fascinating.

End of Entry

Notes:

* We can do this, since (1) the natural numbers are countable, (2) class signs are a subset of statements in our formal system, which can be represented by natural numbers, so (3) the set of class signs have cardinality less than or equal to the natural numbers.

** Unprovability and provability of R_2(2) and R_9(9) are based on the assumption that our formal system is powerful enough to contain truths about the natural numbers. The two statements given are pretty basic truths about the natural numbers, so I would hope that they are provable/unprovable ...

More notes:

Thanks to Lilly for helping to ensure that I wrote something sane. =)