Gödel’s Incompleteness Theorems

Have you ever thought that traditional mathematical reasoning could prove everything that is true about numbers? Or that we could prove, using traditional mathematical reasoning, that mathematics was free of contradictions? Well, think again. Gödel proved that these things are not possible. How did he do this?

Statement of the Two Theorems

Kurt Gödel is famous for the following two theorems:

Any formal system (with a finite axiom schema and a computationally enumerable set of theorems) able to do elementary arithmetic is either inconsistent or incomplete.
Any formal system able to express its own consistency can prove its own consistency if and only if it is inconsistent.

Proof of the First Theorem

Here's a proof sketch of the First Incompleteness Theorem. While the proof applies to any formal system of arithmetic, we'll formulate the proof sketch using a specific theory, namely Hofstadter's TNT (defined in Chapter VIII in GEB). We will use Hofstadter’s own Gödel numbering:

0 666	( 362	[ 312	∧ 161	∃ 333
S 123	) 323	] 313	∨ 616	∀ 626
a 262	< 212	+ 112	⊃ 633	: 636
' 163	> 213	• 236	~ 223	= 111

Let PP be the formula with free variables a and a' that asserts that a is the Gödel number of a proof whose last formula is a'. (Recall that proofs, like all formula sequences in TNT, are Gödel numbered by inserting the codon 611 between the encoding of each formula in the sequence.) Note PP is too long to write out in full, but it is well-defined and clearly exists.

Example: The following is a proof in TNT:

    ∀a:~Sa=0
    ~Sa=0

Therefore PP{S^{626262636223123262111666611223123262111666}0/a, S^{223123262111666}0/a'} is true.

Define the arithmoquinification of a formula A as the formula you get when you substitute the Gödel number of A for all free variables in A itself.

Example: The arithmoquinification of a = 0 is S^2621116660 = 0

Example: The arithmoquinification of (a • 0) = 0 is (S^{362262236666323111666}0 • 0) = 0

Example: The arithmoquinification of ∃ a' : a = (a' + a) is ∃ a' : S^{333262163636262111362262163112262323}0 = (a' + S^{333262163636262111362262163112262323}0)

Let AQ be the formula with free variables a'' and a' that asserts that the arithmoquinification of the formula with Gödel number a'' is the formula with Gödel number a'.

Example: AQ {S^2621116660/a'', S^{SUM(k ∈ 0..262111666, 123 × 10^3k+9) + 666111666}0/a'} is true

Example: AQ {S^2621116660/a'', SSSSSS0/a'} is false

Let U be the formula ~∃a:∃a':<PP ∧ AQ>. Call its Gödel number u.

Now let's arithmoquine U (it has one free variable, namely a''), resulting in a new formula which we will call G: ~∃a:∃a':<PP ∧ AQ{S^u0/a''}>.

What does G say?

There is no proof pair ending in the arithmoquinification of U, i.e.,
The formula whose Gödel number is the arithmoquinification of U is not a theorem of TNT, i.e.,
G is not a theorem of TNT, i.e.,
I am not a theorem of TNT, i.e.,
I am not provable in TNT.

Now we have one of two results:

Is G true? If so, then it is not provable but true, so TNT is incomplete.
Is G false? If so, then it is provable but false, so TNT is inconsistent.

Therefore, TNT cannot be both consistent and complete. Q.E.D.

Proof Sketch of the Second Theorem

You can find a sketch of a proof of the second theorem at Wikipedia.

What's the Big Deal?

These results were considered a big deal when they were first proven in the 1930s. At that time, many mathematicians thought that one could build a consistent, complete, and decidable formal system for number theory. But we now know that if a formal system becomes strong enough to formalize number theory, then it can also formalize statements about itself, and is subject to the usual paradoxes arising from self-reference. Or, in simpler terms, within a formal system for arithmetic, truth is a bigger notion than proof. You simply can't prove everything that's true about arithmetic using a formal system.

Things to Consider

Whether or not you find these theorems surprising, you should think about the following:

There are systems of logic that are consistent and complete, like the Propositional Calculus, but they aren't powerful enough to even express all mathematical facts.
Once we get a formal system with enough power to express interesting mathematical facts, it becomes self-referential and thus becomes unable to prove certain facts, and is thus incomplete.
In TNT, G is not a theorem, but neither is ~G. Note, however, that <G ∨ ~G> is a theorem of TNT. This makes us wonder whether the formal system reflects itself accurately (GEB, page 449).
In TNT, assuming we want it to be consistent, we must take G to be true but not a theorem. Now if we add it as an axiom, we remain consistent, but in this new, enhanced system, we can still compose a Gödelian sentence that asserts its own unprovability. And so on, forever. Truth in formal systems representing arithmetic is elusive. It is simply beyond proof.
How about asserting ~G as an axiom? This is explored starting on page 452 in GEB ("Supernatural numbers").
If we can't prove everything with formal systems, and we can't use formal systems to prove consistency (i.e., that mathematics has no contradictions), then are there other ways of doing mathematical reasoning beyond formal systems?
The two theorems only show that mathematics as we know it is not complete, nor can it prove its own consistency. They do not, in themselves, show it to be undecidable. Church and Turing did that a few years after Gödel proved his theorems.
Remember that the first incompleteness theorem does not show that truth transcends proof in general, but only in formal systems for arithmetic and similar theories.
Perhaps the "problem" here is with dualism. After all, TNT includes the propositional calculus, which is a bivalent logic. These logics don't "completely" handle self-referential forms like "This sentence is false" so of course they lead to incompleteness. If you feel that these incompleteness theorems are disappointing and limiting, you should abandon dualism.