CooperToons HomePage Merry History Dept. of Education CooperToons Books Return to Kurt Godel Caricature

Gödel's Theorem
A Most Brief and Very Sketchy Outline

Kurt Gödel

A Bit of an Involved Process


We all know how bouquets are thrown toward certain gentlemen (and gentle ladies) for accomplishments that few have any idea what it's about. Albert Einstein's theory of relativity is probably the prime example. Everyone has heard about it and many people realize Albert's theory was perhaps the most revolutionary in the history of the world. There are even some people who know enough about the theory to tell you that time actually slows down as you go faster.

But ask Joe or Josephine Blow on the street to show you exactly why time slows down, and they'd probably be at a loss. But it's not really all that tough to do so. You need a little middle school math and acceptance of an experimental fact which - amazingly - certain, well, certain "groups" even in so-called "modern" societies find objectionable. The particular fact happens to be that the speed of light has the same measured velocity regardless of the direction or speed of the observer. The middle school math is the Pythagorean theorem. Take the fact and the math and with a little algebra, you can show that time slows down by a factor of √1-(v/c)2 where v is the velocity of the person and c the speed of light. And mass also goes up by a factor of 1/1-(v/c)2.

Albert Einstein - Relativity

After divorcing Mileva, Albert had some difficulties in the single bars around Zurich.

But in relatively recent times (no joke intended), one of the most admired of these We-Know-He's-Important-Because-Eggheads-Tell-Us-He-Is is the Austrian mathematician and logician, Kurt Gödel. Kurt, we read, showed that there are true statements that have no proof. Not surprisingly, Kurt has since become the idol of many people who expect you to believe things they believe but can't prove. Kurt has been cited as "proving" the truth of the Bible, the Koran, and the United States Constitution.

Well, soddy, folks, Kurt never proved there are Great Revealed Truths That Can't Be Proven. He didn't even prove there are little tiny itty-bitty truths that can't be proven. Certainly nothing he did had anything to do with any political tomes, religious texts, or government documents.

Actually, that last statement isn't quite true. Before Kurt applied for American citizenship in 1948, he had been studying the US Constitution. By logical analysis he had concluded that it was possible for the United States - quite legally and through constitutional means - to become a dictatorship. Then when the judge asked him why he wanted to be an American citizen, Kurt replied it was because he had seen how the countries of Europe had been transformed into dictatorships before and during World War II. "Well," the judge said, "that can't happened here." Kurt jumped up and cried, "Oh but you're wrong!" Fortunately, one of his friends got Kurt to sit back down, and the judge just let the remark pass.

Truths Without Proofs?

OK. Just what is it that Kurt actually did?

Well, Kurt proved that if you took mathematics - particularly the "formal" system of mathematics that was derived by Bertrand Russell and Alfred North Whitehead back in 1913 and which is essentially modern number theory - you could follow their rules and create quite legitimate but certain specialized mathematical formulas that were true and yet could not be proven as a theorem.

Note we say he created mathematical formulas which you could not prove as a theorem. There's absolutely nothing about saying there are true statements that can't be proven by at least some means.

For decades, Kurt's paper was pretty much ignored by the mainstream public. Then in 1970, Scientific American printed an article called "Unsolved Problems in Arithmetic". Kurt was mentioned briefly, but at least the article brought some attention to a reasonably mainstream audience to Kurt's work.

As time went on more and more people began writing popularizations - both articles and books - about what Kurt did. But very few of them actually get into the meat of Kurt's arguments. Kurt's paper, they say, is difficult, even for mathematicians to understand. On the other hand, some say it is important as it was the first demonstration of a psychological truth of the human mind with the rigor of a mathematical proof and which is as revolutionary as Albert's Theory of Relativity, Erwin Schrödinger Wave Equation, or Werner Heisenberg's Uncertainty Principle.

Now you can get a copy of Kurt's paper in an English translation. Or you can get a copy of the original German paper (it can be found). And you can even get both if you want (there is a book which has the German and English facing each other). Get any of those and you'll find, by golly, they're right. Kurt's paper is difficult.

Now, it isn't quite true that the 1970 article was the first attempt to explain Kurt's paper. In 1956 - twenty-five years after Kurt's original article - there was an article also in Scientific American by James Newman and Ernest Naegel . This in turn was an abridged version of a chapter from, The World of Mathematics. The chapter and the article, both called "Godel's Theorem", was later published as a small booklet under the same name. And the authors did get into the nitty gritty of Kurt's proofs.

James and Ernest's article - although a simplification of Kurt's more demanding article - is a good place to start. They begin at Square 1 and explain what formal logic is and then go into details of how to define numbers like Bertie and Alfred did. From there they do a good job of going through the steps to creating Kurt's non-provable formula. Then they prove the non-provable formula was true.

So for the interested reader, a modest CooperToons suggestion is:

Get a copy of James's and Ernest's chapter or booklet first (and read it, of course).
Then get a copy of Kurt's paper. But start reading - not at the first of Kurt's paper - but where he starts his definitions.

But if this isn't practicable, you can read on!

A Non-Gödelian Example

Before we move on to what Kurt actually did, we'll go through, if not Kurt's proof, then a proof that there are true mathematical statements that can't be proven. It requires only the simplest of mathematical knowledge.

For instance, take the set of natural {counting} numbers, 1, 2, 3, 4, ...... (as Henny Youngman might have said, please!)

Now there are many subsets of the counting numbers. They can be the even numbers {2,4, 6, ...}, odd numbers {1, 3, 5, ...}, multiples of ten {10, 20, 30}, the set of squares {1, 4, 9, 16, 25, 36, 49, ...}, and even the set of counting numbers itself {1, 2, 3, 4, ...}.

But just how many subsets are there? Well, there is a theorem of math that you get more subsets than the elements in the set itself. For instance, a set of three numbers {1, 3, 299991} has a total of eight subsets: {1}, {3}, {299991}, {1, 3} {1, 299991}, {3, 299991}, {1, 3, 299991}.

But you said eight. You listed only seven.

Oh, yes. The empty set { } - also called φ - is a subset of any set. That makes eight.

In fact, it can be proven (via mathematical induction) that if a set has N elements, there are 2N subsets.

But what about a set with infinite numbers of elements like the counting numbers? How many subsets are there? Are you saying there are 2 subsets.

Why, no. How could any set have 2 subsets? How ridiculous! How absurd!

No, we are saying there are 2א‎0 subsets. א‎0 as everyone knows is the cardinality - that is the size of a countably infinite set. Or to put it another way, א‎0 is the type of infinity of the counting numbers.

But here's what's important. If א‎0 is countably infinite, then 2א‎0 is not only infinite but non-countably infinite. We call that type of infinity, א‎1. And indeed:

א‎1 = 2א‎0

Which means that no matter how large א‎0 is, then (and which you can prove with the diagonal argument) we know that:

א‎1 > א‎0

But what does that have to do with proof?

Well, remember. There are limits on the number of symbols you can use to prove theorems. After all, any proof must contain only a finite set of characters. Otherwise the proof would never end and you wouldn't prove anything. On the other hand, the number of symbols that are available for any particular proof is open ended. So at the most there must be no more than a countably infinite number of proofs.

Now let's go back to our subsets of all counting numbers. There we found א‎1 subsets. And each of these sets has some true statement associated with it. For instance, it is true that any particular number is or is not a member of that set. So the number of true mathematical statements must likewise be uncountably infinite.

But if we only have countably infinite theorems and yet uncountably infinite true mathematical statements, then there are too many true mathematical statements to prove!

So it seems there are truths without proofs.

On the other hand, note that what we've done is show there are some truths without proof. But we haven' given you a specific example of one.

That's where Kurt comes in.

In Media Res

We repeat: The true statements that Kurt was interested in were those of formal logic about numbers. Formal logic uses formulas to define and express relationships between numbers - hence the name. So to have a formal system you need 1) a group of symbols and 2) rules to manipulate the symbols. Fortunately, there was a system already in place for Kurt to use. That was the one we mentioned, the system of logic and numbers defined by Bertrand Russell and Alfred North Whitehead in their book Principia Mathematica.

Now, oddly enough what bogs people down about Kurt's paper is they start at the beginning. Yes, at the beginning. We mentioned that it's best to start about halfway through where he lists his definitions. That's what we'll do.

And Kurt starts off with a nice simple definition that everyone knows about. He defines division. That is, how to divide one number with another. But he only uses the symbols of formal logic. So Kurt's Definition #1 is:

y/x ≡ ∃z: y = x × z

This is read as follows (with a crib suppled):

y divided by x (y/x) is defined () by the formal statement "There exists some number z (∃z) such that (:) y equals x times z (y = x × z)."

Now note how much shorter the formal definition is. But here's where Kurt did something that was new. You can write the formal definition, which is

∃z: y = x × z

as a unique number. Yes, the formula can be written as or actually mapped into the set of counting numbers. But only, we must caution, a special subset of the counting numbers. Kurt - with a bit of pardonable hubris - called his numbers Gödel numbers.

Now to write a Gödel number, you do this. First you must assign some numbers to the primitive symbols of the formal language. For instance, the first dozen symbols can be:


To be honest this isn't Kurt's original numbering system. He used the highly simplified set that Bertie and Alfred created. Doing so avoids redundancies. For instance, saying "x is not equal to y" in the original symbols would be ¬(x = y). With out symbols you could also write this as x≠y. For now we'll assume we can handle redundancies.

Next, to actually represent an equation as a number, you take the numbers we've defined above and write them as exponents. That is, you raise them to a power. But the numbers you raise them to - that is the base of the exponent - must be the series of increasing prime numbers. So for our equation:

∃z: x = z × y

... you can represent the method using symbols as:


Or by substituting the numbers:


This is a pretty big number. In fact it is equal to


The particularly interesting characteristic of this number - and any Gödel number - is they are unique. No two formulas give the same Gödel number. But more to the point, you can factor a Gödel number back to the original series of primes and exponents. You simply start off dividing the number by 2. Then you keep dividing the answer by 2 until you get a number not divisible by 2. The number of times you divided by two is the first exponent. You can now look up what symbol the number stands for.

Now take the number with all the 2's factored out and then start dividing by 3. Keep it up until the number is no longer divisible by three. You have the next exponent and you can convert that to the symbol. Continuing dividing the numbers by the increasing series of primes, and eventually you will have recovered all your exponents and hence been able to reconstruct your original formula.

What you ask is the point? What is this except creating a code for disguising formulas?

Look at what Kurt is doing. Because all of his definitions and derivations are ultimately about numbers, he is sticking with the language of the formal system. And he isn't mixing things up. For instance, remember that using the symbols for the exponents gives you the strange expression:


But such an expression isn't allowed in the formal system. So by transforming the exponents to the corresponding number Kurt creates a perfectly good number than can now be used in equations about numbers.


And yet it still represents the original equation, too!

In mapping the equations about numbers to numbers themselves, Kurt can represent discussions about numbers as equations made up of numbers. He is not departing from the formal language and so will be able to avoid the type of fallacy that invalidates a lot of the famous logical "antimonies", such as the Liar's Paradox.

Kurt Gödel

Liar's Paradox

So we've completed with Definition #1. Now for Definition #2.

Kurt's Nested Definitions: Some Examples

Kurt's second definition was how to define a prime number (he has to do this to use his Gödel numbers).

We of course know what a prime numbers is. A prime number is a positive integer that is not equal to 1 and is not divisible by any numbers except itself and one.

To put this in the formal language, Kurt came up with:

Prim(x) ≡ ¬(∃z < x & [z ≠ 1 & z ≠ x & x/z]) & x > 1

which we read as saying:

x is a prime if there does NOT exist some number z which is not equal to one and z is not equal to x and x is divisible by z AND x is greater than 1.

This seems to be a bit stilted and artificial way to define something, but you'll see that this is nothing more than saying a number is prime if it is not equal to one and is not divisible by any other number except 1 and itself. This is the standard textbook definition of a prime number.

But note that this definition - that is, Definition #2 - uses Definition #1. That is Definition #1 is nested in Definition #2. This, though, is done purely for convenience and isn't necessary. For example without our first definition, we could still write Definition #2 in the formal language:

¬(∃z < x & [z ≠ 1 & z ≠ x & (∃q: x = zq)]) & x > 1

(The new variable, q, would of course have a Gödel number of its own.)

We can express our new definition in ordinary language:

Prim(x) ≡ "x is a prime number."

But although we can express Prim(x) in our conversational language, it can be written entirely in the formal language. That also means Prim(x) has its own unique Gödel number. We'll call it g2

g2:      Prim(x)

The next definition, Definition #3, incorporates Definition #2. It has two parts.

0Prx ≡ 0

(n + 1)Prx ≡ εy [y < x & Prim (y) & x/y & y > nPrx]

Here the symbol ε means we select the minimum value of y which makes the statement true.

The first part, 0Prx ≡ 0, means the zeroth prime number that is a prime factor of x is zero.

But Part 2 is a bit more long winded. This is read as:

The (n + 1)th prime number in x is the minimum value of y such that y is less than or equal to x and y is a prime number and x is divisible by y and y is greater than the previous prime number in x.

This simply means that nPrx is the nth prime number to appear in the number x.

For Definition #4, Kurt defines the familiar factoral function

0! ≡ 1

(n + 1)! ≡ (n + 1). n!

And for Definition #5 Kurt gives us:

Pr(0) ≡ 0

Pr(n + 1) ≡ εy [y < {Pr (n)}! + 1 & Prim(y) & y > Pr(n)]

To put this in perhaps not plain English, this simply means that the n + 1 prime number is the smallest number such that it is less than the factoral of the previous prime number plus 1 (thus setting an upper bound) and is a prime and it is greater than the previous prime number.

Which means (yawn) that Pr(n) is the nth prime number.

Enough Already!

As Kurt would say "Diese Beispiele werden genug!" That is, enough examples, already! So we'll jump ahead.

What Kurt did was to continue making definitions by

1) Using primitive symbols from the formal system

2) Using his new definitions that are based on the symbols and/or their Gödel numbers.

3) Doing whatever else he needs to do to create his definitions.

The thing to remember is that each definition could be written in terms of the primitive symbols and each has a unique Gödel number. Gödel numbers can also be used simply as numbers and in doing so keeps everything in terms of our formal system.

Now at this point, we should mention that sometimes Kurt uses the term "formula" when he should say the "Gödel number" of the formula. But other times, he does use the word number when he means number. We'll try to keep things clear.

Kurt's definitions continue past the concept of prime numbers and the n-th prime number to where he defines creating variables, defining different variable types, combining symbols to produce formulas, the process of putting parentheses at various places in a formula, combining formulas to produce larger formulas, and replacing parts of formulas with other variables or formulas. Eventually he even reaches the point where his formulas stand for the process of implying that certain formulas or groups of formulas lead to another formula. Each of these definitions represents a formula expressible in the primitive symbols of the formal language, and so each has a Gödel number. Since Kurt is following the rules for making formulas, all his formulas are proper and correct within the mathematical system of Bertie and Alfred.

Continuing, but not Ad Infinitum

Eventually Kurt reaches Definition #31:

Sb[x, v, y]

Now you have to follow this next bit carefully. Sb[x, v, y] is defined as the formula - actually the Gödel number - you get when you take the formula with Gödel number x and replace the variable with Gödel number v with the number y.

We'll break that down.

Sb[x, u, v] is the Gödel number that you get when you take

The formula with Gödel number x

And replace the variable with Gödel number v

With the number y

But Kurt doesn't stop here. He keeps going. He creates more definitions. At Definition #45, he gives us a formula


where xBy states that the formula (or formulas) with Gödel number x is a proof of the formula with Gödel number y.

xBy: x is a proof of y

And now, finally after much weary plodding, we end up with the last definition, Definition #46:

Bew(x) ≡ ∃y: yBx

which says

Bew(x) is defined as "There exists some (Gödel) number y such that the (Gödel) number y is the proof of the formula (with Gödel) number x."

Or in plain English:

The formula with Gödel number x is a provable formula.

At this point, x is still a variable. That is, it has not been assigned a number (i. e., a formula). So we can't say whether it's true or false. But certain Gödel numbers will make the formula true or false. For instance, the equation:

0 = 0

has the Gödel number of

223552 = 24300


So the statement


is indeed true.

Kurt's Final Formula(s)

At this point we need no new definitions. We just need to use the ones we have to make a new and very interesting formula. We do this by going back to our earlier Definition #31.

Sb[x, v, y]

which as we said is the formula - actually the Gödel number - you get from the formula with Gödel number x by replacing the variable with Gödel number v with the number y.

But let's look at the specific case:

Sb[y, 19, y])

This is the Gödel number for the formula you get when you take the formula with Gödel number y and replace the variable with Gödel number 19 with the number y.

At this point you may guess - correctly it turns out - that we have carefully chosen our values. Note that the number 19 just happens to be the Gödel number for the variable y. As you'll see this is necessary.

But Sb[y, 19, y]) is a Gödel number. Ergo, it is a number that you can substitute for a variable in a formula about numbers. So let's put THIS number into a new formula, the negation of Bew(x), which is ¬Bew(x)

Then we get

¬Bew(Sb[y, 19, y])

Yes, this is the formula for the statement "The formula with Gödel number Sb[y, 19, y] is not provable.

But for the present y is still a variable. It has no value and so the new formula is not true or false.

But this formula - like all of them - does indeed have a Gödel number. We'll call it n:

n: ¬Bew(Sb[y, 19, y])

Are we done? As Big Jake said, "Not hardly!" Now we'll replace the variable y in this formula with the Gödel number of the formula itself. That is, with the number n.

And we have

¬Bew(Sb[n, 19, n])

What we have is this. ¬Bew(Sb[n, 19, n]) is the formula we got when we took the formula with Gödel number n and replaced the variable with Gödel number 19 - which was y - with the number n.

And this formula, like all of them, has its own Gödel number. We'll call it G

G: ¬Bew(Sb[n, 19, n])

Now we're done.

Sort of.

The Big G

Note that at this point there are no longer any variables. We just have numbers. So it is now meaningful to ask if this statement is true or false. But how do we do that?

First we ask just what is G?

Well, we could go back and put in the primitive symbols in the definitions and come up with a humongous number. It would probably be too big to write down in any reasonable time - like the number 999 that Robert Ripley wrote about. Besides, we'd make so many mistakes that it wouldn't even be correct.

Or we can reason what this Gödel number is. We do that by considering just how we got it.

Well, G is the Gödel number you get when you take the formula with Gödel number n and replace the variable with Godel number 19 with the number n.

Hm. This sounds awfully familiar.

Didn't we just say that Sb[n, 19, n] is the Gödel number you get when you take the formula with Gödel number n and replace the variable with Gödel number 19 with the number n?

Yes, we did say that.

But doesn't that mean Sb[n, 19, n] is the same as G!

Yep, that's true.

Sb[n, 19, n] = G

But doesn't that mean that we can now write:

G: ¬Bew(G)

Indeed (to quote Shakespeare).

In other words, the formula with Gödel number G states that the formula with Gödel number G isn't provable!

You got it.

You mean that we - or rather Kurt - has developed a perfectly legitimate formula that denies its own provability?

That's exactly what Kurt did and what we now have.

The Big Question.

But hold on. Kurt created - or rather he found - a formula that says it can't be proven. But he doesn't say if it's true or false.

Which is it?

Well, let's pause a minute. If G is indeed not provable, then it must be true. After all, that's what it says.

On the other hand, if G is provable, that means we can prove a non-provable statement.

Hanh? What did you say?

If G is provable,we can prove a non-provable statement.

Doesn't that mean if G is provable, we can prove a false statement?

Yes. That's what it means.

But first, let's point out, proving a false statement is not the same thing as proving a statement to be false. You do the latter all the time in math.

For instance, if I say "For every x, x is equal to x + 1" that is a false statement. And you can (though we won't) prove this statement is indeed false.

But we are not proving the statement "For every x, x is equal to x + 1". That would mean we can prove a false statement is true!

In other words, if we prove a false statement, then we have an inconsistent system. And the problem with inconsistent systems is that nothing is true and nothing if false. Or rather everything is true and everything is false at the same time. Inconsistent systems must be rejected by anyone who distinguishes truth from falsity. (To show you what can happen with an inconsistent system, click here.)

An Inconsistent System

So what does this mean about our statement that ¬Bew(G) is not provable?

Well, if our numbering system is consistent, then, we can indeed write statements that are non-provable. But that's what the formula says! That it's not provable! So as long as our system is consistent, then the statement saying G can't be proven is true!

And in 1936, five years after Kurt's paper appeared, the German mathematician and logician Gerhard Gentzen, proved Bertie and Alfred's number system was indeed consistent.

Since the system is consistent, and Kurt's deductions are valid, Kurt's statement that ¬Bew(G) is not provable is in fact true!

But wait a minute. If the system is consistent, that means we can't prove ¬Bew(G). But we just did! So didn't we just prove what we said we can't prove?

Working Within the System

In the System

Well, no. We didn't do exactly what we said we couldn't do. That's because when Kurt defined the formula


he did so based on the definition that x must be a formula or series of formulas that are 1) either an axiom of the system or 2) can be deduced from an axiom or a previously proven formula. In other words, xBy and all other formulas [including ¬Bew(G)] refer to proofs within the system.

But our own "proof" - that the specific ¬Bew(G) is true - was not from a formal proof within the system. We were reasoning outside the system, albeit correctly. So we proved something was true although it couldn't be proven within the system.

What Kurt Didn't Do

Now for some people, once you see what Kurt did, it's kind of a let down. You become a bit suspicious as whether what he did was all it's cracked up to be. I mean, he showed there was a formula that couldn't be proven as long as it was a formula that did nothing more than state that it - the formula itself - couldn't be proven! How can this be said to be anything you could prove? Aren't we even muddling with the definition of "formula" in mid-proof so to speak?

Well, not quite - provided you realize we are talking about a formal system. In a formal system our formulas are subject only to the rules of construction. A formal system might have some everyday interpretation, but it is not necessary. A proper formula - that is a well-formed formula is simply one constructed by the rules.

So as long as Kurt was following the rules, what he made was indeed a bonafide formula. It doesn't have to make sense to us. But more to the point, just because we didn't realize there were these strange "I-can't-be-proven" formulas in mathematics, that doesn't mean they aren't there. And the reason we can't even see how to begin a proof of such an oddball formula is because there is no proof. That is, although it is a correct formula, it cannot be derived from the axioms and the rules of deduction.

So we can say that Kurt did not prove there are Great Unknown Truths That Can't Be Proven. He proved that if you have a sufficiently complex number system - that is a system as "rich" as that devised by Bertie and Alfred - then if you follow their rules you can create legitimate well-formed formulas of elementary number theory that are not provable within the system.

Or look at it this way. The goal of mathematicians in the early 20th century had been to find a set of axioms from which you could derive all the correct statements about numbers. But to derive the axioms you have to come up with a universal definition of the concept of a number. But Kurt's theorem essentially showed that there is not and can't be an axiomatic system that will define exactly what a number is. Axiomatic systems, we must point out, define things in terms of properties and characteristics but do not actually define the basic terms (remember in your geometry that "point" and "line" are undefined). Without a universal definition of number, some formulas may not be provable in some systems but may be in others.

For instance, in 1929, the mathematician Mojzesz Presburger devised a system of arithmetic that was shown to be 1) consistent and 2) complete. That is, you could only prove statements that were true and all of the true statements could be proven. Furthermore this "Presburger's Arithematic" was decidable This means there is an actual automatic procedure (algorithm) for proving that a statement is true or false. One drawback to Presburger arithematic is you could only add numbers, not multiply them. It seems strange that adding numbers once doesn't cause problems, but adding them a set number of times does. But that's the way it goes.

In the end, the legitimate doubts were not about the technical correctness of what Kurt did but instead were questions about the importance of Kurt's Theorem for mathematicians who work in fields other than logic. Some research mathematicians point out that what is amazing is not how much Kurt's theorem changed mathematics, but how little it changed it. In fact, most mathematicians go through their entire careers with scarcely a glance at what Kurt did, thank you.

True, since 1931 there have been "real" equations about numbers that have been shown to be without proof in certain systems. But this doesn't mean they have no proofs and indeed some of the non-provable theorems have been proven. Others, though, like Collatz's Conjecture (which you can fiddle with on an Excel spreadsheet if you click here) have yet to be proven in any system.

Actually, the Polish mathematician (and co-inventor of the H-bomb), Stanislaw Ulam (who knew Kurt personally) said he always felt Kurt himself had doubts about the theorem. Did he actually find a new principle regarding the foundations of mathematics? Or was his famous theorem just one more of the logical paradoxes, albeit in clever disguise? Today most people accept it was the former, and the question probably worried Kurt more than anyone else.

Stanislaw Ulam

Stanislaw thought Kurt was worried.


World of Mathematics, James R. Newman (Ed.), 4 Vols., Simon and Shuster, 1956. This was - amazingly - a best seller and so first editions are easily found. The costs range from a bit pricey - but not out of line for a four volume set - to actually quite cheap. Sadly a bit dated but a good history - albeit a bit eclectic - of mathematics.

Godel's Proof, James R. Newman and Ernest Naegel, New York University Press, 1958 (later edition, 2001). The chapter from the World of Mathematics published as a small book.

Collected Works, Volume1: Publications 1929-1936, Kurt Gödel, Oxford University Press, 1986. The first volume of Kurt's Collected Works. A bit on the pricy side.

"On formally undecidable propositions of Principia Mathematica and related systems", Kurt Gödel, An on-line translation which updates Kurt's symbols and adds some additional explanations.

On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Kurt Gödel, Dover, 1992. One of the early reprints of Kurt's paper in an English translation. Itself a reprint of an earlier translation.

Incompleteness: The Proof and Paradox of Kurt Gödel, Rebecca Goldstein, Norton & Company (2005). An account of Kurt's famous theorem. Also discusses some of Kurt's personal life and philosophy.

Gödel's Theorem - An Incomplete Guide to Its Use and Abuse, Torkel Franzén, A K Peters, (2005). A readable book making sense of and also showing the nonsense in what some people say about Godel's theorem. A good book to remind people that Godel's theorems are about - we must again emphasize - formal mathematical systems not the U. S. Constitution, not the Bible, and not the Koran.

"Does Gödel Matter? The romantic's favorite mathematician didn't prove what you think he did", Jordan Ellenberg, Slate, A review of a book about Gödel's theorem where the reviewer points out that the importance of Gödel's theorem can be overstated. What is amazing is not how much Kurt's theorem changed what mathematicians do in their work, but how little it changed it.

"Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science", Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, 2006, John W. Dawson, p. 339. A brief paper also stating that outside of logic the effect of Gödel's theory on the field of mathematics has been slight. A personal CooperToons opinion is if it has been slight, it hasn't been negligible.

"Does Gödel's Theorem Matter to Mathematicians?", Gina Kolata, Science, Vol. 218, pp. 779-780 (1982). Kind of an answer to the question whether Gödel's theorem is simply a logician's trick and isn't a "real" mathematical proof. This paper shows some examples that are real mathematics but for one reason or another can't be proven - again it must be stressed - within their system.

Who Got Einstein's Office? Eccentricity and Genius at the Institute for Advanced Study, Edward Regis, Perseus Books (1987). The first chapter is about Kurt and arguably is the best chapter of the book.