New version of this book

Incompleteness theorem

This discussion of Gödel 's proof does not follow Gödel 's constructions or formulation. It is extremely informal and uses understanding of computer programs to make the ideas that underly Gödel 's results more easily accessible to a contemporary audience.

Recursive functions are good because we can, at least in theory, compute them for any parameter in a finite number of steps. As a practical matter being recursive may be less significant. It is easy to come up with algorithms that are computable only in a theoretical sense. The number of steps to compute them in practice makes such computations impossible.

Just as recursive functions are good things decidable formal systems are good things. In such a system one can decide the truth value of any statement in a finite number of mechanical steps. Hilbert first proposed that a decidable system for all mathematics be developed. and that the system be proven to be consistent by what Hilbert described as `finitary' methods.[16]. In response to this challenge Gödel developed his famous theorems known as the first and second incompleteness theorems. These show no such formalization is possible for non trivial consistent systems.[16]. He went on to show that it is impossible for such systems to decide their own consistency unless they are inconsistent. Note an inconsistent system can decide every proposition because every statement and its negation is deducible. When I talk about a proposition being decidable I always mean decidable in a consistent system.

One key to Gödel 's proof is the `Gödel numbering  ' of all the statements in a formal system. This is an algorithm to assign a unique integer to every statement in the language. Today this is simple and intuitive. Today we convert computer programs and just about everything else to Gödel numbers as we store them as bit patterns in computers. In Gödel 's time it was a stroke of genius. Gödel numbering things is often thought of as an abstract mathematical idea, but it is both extremely common and immensely practical.

Once we have Gödel numbered the statements in a formal system we can think of the system as a recursive process for enumerating the numbers that correspond to provable statements in the system. If a system is strong enough to define any recursive function it must be strong enough to define itself as a recursive process. That is within the formal system we can define a recursive process that enumerates the Gödel numbers of all the statements that can be proven in the system. Kleene  points out that Gödel 's proof constructs within the formal system S he is working with a statement that says ``I am unprovable in S''(128)[16]. Of course if this statement is provable in S then S is inconsistent. So any system strong enough to model itself in this way and to construct this statement must be either incomplete or inconsistent. It turns out that this is almost any nontrivial formal system.

How do we construct this self referencing statement. Gödel 's proof does this in detail and is complex for this reason. We can understand informally how to do this construction by understanding that a formal system, S, can model itself as a computer program, , that outputs the Gödel numbers of theorems. (Today we think of programs as outputting text like the text of theorems but this is still Gödel numbering. The text is output as ASCII character codes or another bit pattern coding for characters.) The statement that a particular theorem is provable is the statement that will output a particular number. The Gödel number for the statement does not output x will not ordinarily be x. However, by using a sort of diagonalization technique, we can construct a statement that says what we want.

Let us define to be the statement that if x is the Gödel number of a statement in system S with one free integer variable then is true. We are treating x as both the Gödel number of a statement () and an integer. We apply the statement to this integer by setting y in to x. This is straightforward although a formal proof requires construction of the Gödel numberings and other details. Assume a is the Gödel number of . is the statement we want. It asserts that it cannot be derived from S. If we could derive it from S it would be false and thus we would have a contradiction. Thus is true. Note we have just derived from the assumption that S is consistent. This implies that we cannot prove the consistency of S within S itself. If we could we could derive and this would imply that is false. This result is Gödel 's second incompleteness theorem  .

Gödel 's proof is another in the history of proofs based on self reference going back to the ancient liar's paradox. The essential new ideas are Gödel numbering of statements and modeling a formal system within itself as a computer program to enumerate theorems (or Gödel numbers of theorems).

Another way to prove Gödel 's first incompleteness theorem 

is to use the result that we cannot in general decide for a recursive function F if some number x is in the range of F, i.e. there is a set that is recursively enumerable but not recursive. We proved the existence of such a set in the previous section and gave the example of the halting problem for computer programs. A formal system that is strong enough to state the halting problem for all programs cannot be decidable. There are statements of the form program x never halts that are true but not decidable in the system. If all such statements were formally decidable then we could decide the halting problem by enumerating all theorems. Eventually (in a finite time) one of the theorems would be that the program does halt or that it does not halt.

New version of this book