An Outline of the Proof of Gödel's Incompleteness Theorem
All essential ideas - without the final technical details

Informally, Gödel's Incompleteness Theorem states that in any consistent formalization of mathematics that is strong enough to define the concept of natural numbers, one can construct a statement that can be neither proved nor disproved within that system.

In our outline, we will try to demonstrate that the conclusion of Gödel's Theorem is valid for the formalization of mathematics based on axiomatic set theory. But a careful reader will notice that this is only a technical restriction.

What we show on this page is not a presentation of the proof that was written by Gödel himself. We present all the basic ideas that are necessary to understand what the theorem asserts and what it would take to write a proof.

Before we start we have to go through a brief review of how set theory is constructed and what theorems are.

We claim that any mathematical formula can be written in the alphabet

where

We don't claim that this alphabet is minimal. But we have chosen it for didactic reasons.

These are three examples of mathematical formulas: a:-O, ~(a:-O), /\(a)(~(a:-O)).

Notice that every mathematical formula is a string but not every string is a mathematical formula. In order to determine which strings are mathematical formulas we have to define a formal grammar.

We need to define a class of formulas for which it makes sense to ask whether it is a theorem or not. We will call such formulas statements.

Definition: A statement is a formula that has no free variables.

These are two examples of statements: O:-{O}, /\(a)(~(a:-O)).

We are now preparing for the definition of theorem. Recall that in set theory there are axioms and rules of inference. Axioms are carefully chosen statements and rules of inference are certain operations on strings.

The application of inference rules looks like this: given two strings /\(a)(~(a:-O)) and {O} we can use a rule of inference to derive the string ~({O}:-O) or given one string /\(a)(~(a:-a)) we can use another rule of inference to derive the string ~\/(a)(a:-a).

It will be very important for later arguments to bear in mind that

Now we are ready to define theorem.

Definition: p is a theorem if and only if
(1) p is an axiom
or
(2) there is a sequence p₁, ..., p_n where p₁, ..., p_n are theorems and we can derive p from p₁, ..., p_n by using rules of inference.

Now we are able to give a more precise statement of what we are trying to prove:

Now we are moving on to the proper part of our proof.

At this point, we will take the crucial step toward understanding the proof of Gödel's Incompleteness Theorem. We are going to identify each mathematical expression with a unique natural number. To this purpose, we will establish a way of encoding a string of symbols from the afore-mentioned alphabet into a natural number.

And the following defines by recursion how any string from our alphabet is encoded as a natural number:

Code[ sx ] = Code[ s ]*H + Code[ x ],

where #H = 10, s is a string, x is a symbol from our alphabet, and sx is the concatenation of s and x.

Examples:
#Code[ ~\/(a)(a:-a) ] = 87A0BA020B
#Code[ /\(a)(~(a:-O)) ] = 6A0BA8AO25BB
#Code[ {O,{O}} ] = 35C3544

Notice that if s is a string then Code[ s ] is a natural number and #Code[ s ] is only its hexadecimal notation.

It can be proved that we can define, in terms of set theory, a function T : |N -> {0,1} with the following property: if n is a natural number such that it encodes a theorem then T(n) = 1, otherwise T(n) = 0.

It would be a long and tedious job to actually construct such a function from the foundations of set theory. We will not do it here. But the following remarks may serve to convince oneself that it is possible.

The art of determining which statement is a theorem comes down to string operations. We can think of the hexadecimal notation of a number as a string. So we can define operations (like concatenation) on such "hexadecimal" strings by using simple operations on natural numbers like addition and multiplication. We can define rules of inference on these "hexadecimal" strings - still only by using operations on natural numbers. And finally, we can define which of these "hexadecimal" strings are "hexadecimal" theorems. Then we would have our function T.

We are going to introduce function A : |N -> |N. We will show how to determine A(n) for a given natural number n: in #n we replace all occurrences of the digit 0 with #Code[ n ] and what we get is #A(n).

At this point some readers may be a little confused by the fact that we write #Code[ n ]. It might be useful to have in mind that, for example, #Code[ 2 ] = Code[ {O,{O}} ] = 35C3544.

Notice that our function A has the following property: if n is a natural number which encodes a formula with the free variable a then A(n) encodes the same formula where each occurrence of a has been replaced by Code[ n ].

Notice also that our function A could in fact be defined without explicitly mentioning Code. But such a way would be long and tedious.

Before we move on to the culminating point, take your time to contemplate the fact that functions T and A are indeed ordinary functions which can be defined in terms of set theory.

Consider this mathematical formula T(A(a))=O. Let

m = Code[ T(A(a))=O ].

Consider the statement below.

T(A(m))=O

Contemplate the fact that the statement above is a real mathematical statement in set theory because the functions T and A are constructible in set theory and the natural number m is also precisely defined.

Notice that

(*) A(m) = Code[ T(A(m))=O ].

Suppose that T(A(m))=O is a theorem. Then by the property of function T, A(m) is not an encoded theorem. However, by (*) A(m) encodes T(A(m))=O, which is a theorem. Contradiction.
So we showed that T(A(m))=O is not a theorem.

Suppose that ~(T(A(m))=O) is a theorem. Hence T(A(m))=1 is a theorem. So by the property of function T, A(m) is an encoded theorem. However, by (*) A(m) encodes T(A(m))=O. So T(A(m))=O is a theorem. But we already had that ~(T(A(m))=O) is a theorem. Since we believe that axiomatic set theory is consistent, we have a contradiction.
So we showed that ~(T(A(m))=O) is not a theorem.

So we have finally constructed a statement in set theory such that it is not a theorem and its negation is not a theorem.