Using the Gödel sentence to prove the incompleteness theorem

Suppose we have a formal theory T in which "a certain amount of arithmetic" can be formalized. In this theory we can also talk about the language and theorems of T itself, through a coding or "Gödel numbering". This means that formulas (sentences) and proofs in T correspond to natural numbers, and properties of formulas and proofs correspond to properties of the corresponding natural numbers. These latter properties can be formulated in purely arithmetical terms, and thus expressed in T. By using the correspondence, we can then interpret certain formulas in T as assertions about proofs and formulas.

Without going into any details regarding how such a correspondence can be established, I will use the notation #A to denote a numeral (i.e. expression denoting a natural number) corresponding to the formula A in the language of T.

I will also use the notation

T |- A

to mean that the sentence A is a theorem of the theory T.

A bit of logical notation will be used: instead of "if and only if", I will use the double arrow, <=>. Thus if A and B are two formulas in the language of T, A<=>B is another such formula, the meaning of which is "A if and only if B". Also, ~ will be used for logical negation, so that the meaning of ~A is "it is not the case that A".

Gödel's proof makes essential use of what is called the diagonal lemma for T. This is a general result about T stating that for every formula B(x) with one free variable x - meaning that B(x) asserts something about the unspecified number x - a formula A (known as a fixpoint for B(x)) can be constructed such that

T |- A<=>B(#A)

Thus, it is provable in T that A is true if and only if its Gödel number has the property B(x). This is achieved by constructing, through some general method, a formula A which "says of itself that it (i.e. its Gödel number) has the property B(x)". The construction of A thus uses some mechanism for self-reference. Indeed, Gödel proved the diagonal lemma by formalizing the self-referential statement

The result of substituting "The result of substituting x for 'x' in x has property P" for "x" in "The result of substituting x for 'x' in x has property P" has property P.

To prove his incompleteness theorems, Gödel used a particular predicate Thm(x), the meaning of which is "x is the Gödel number of a theorem of T". It is convenient to introduce a further bit of notation, and write []A for the formula Thm(#A). Thus []A is a formula which says that A is a theorem of T. This notation can be iterated, so that [][]A is a formula which says that []A is a theorem of T. We will see later how this iteration is useful.

Using the []-notation we can now define what is meant by a Gödel sentence G for T. This is any sentence G which satisfies

(1) T |- G<=>~[]G

Thus, G is a sentence which "says of itself that it is not a theorem of T", and it is provable in T that G is true if and only if it is not a theorem of T. (A technical comment.) That there is such a sentence G is a special case of the diagonal lemma. For the proof of Gödel's theorem, it doesn't matter which such sentence G is used. Thus we often speak of simply "the Gödel sentence G of T".

A semantic version of the first incompleteness theorem

Now suppose all theorems of T are in fact true. Then, from (1), we conclude that the Gödel sentence G is undecidable in T, that is, neither G nor ~G is a theorem of T. For G is true if and only if it is not a theorem of T, and since all theorems of T are true, it follows that G cannot be a theorem of T. Since G is not a theorem, it is in fact true, again using the fact that G is true if and only if it is not a theorem of T. Thus ~G isn't a theorem of T either, since ~G is false.

Thus we have the following version of the first incompleteness theorem: Let T be a formal theory for which the Gödel numbering and diagonal lemma can be carried through, and all axioms - and hence theorems - of which are true. Then T is incomplete, i.e. there are sentences in the language of the theory- as exemplified by the Gödel sentence G for T - which can neither be proved, nor refuted in the theory.

Gödel's version of the first incompleteness theorem

Gödel in fact proved a somewhat different formulation, which does not rely on all theorems of T being true. For his argument, he used a further property of the Thm-predicate, namely that basic facts about provability can be proved in T. More specifically, he established the following principle for the theories T that he dealt with:

(P1) For every sentence A, If T |- A, then T |- []A

In other words, if A is a theorem of T, then it is provable in T that A is a theorem of T.

Using (P1) Gödel proves the following:

If T is consistent, then G is not a theorem of T.

The argument is simple. (Note that it does not involve the notion of truth.) Suppose G is a theorem of T, i.e. T |- G. Then, by (P1), it follows that T |- []G. But by (1) and T |- G it also follows that T |- ~[]G. Thus T is inconsistent, that is, some statement and its negation are both provable in T.

To prove that ~G is not a theorem of T either, we must make some further assumption regarding T. (Mere consistency is not enough for this conclusion.) What Gödel did was to introduce the assumption that T is what he called omega-consistent. This means that there is no formula A(x) such that A(n) is provable for each numeral n, while "for every x, A(x)" is disprovable in the theory. Omega-consistency implies consistency in the ordinary sense, since everything is provable in an inconsistent theory. (A technical comment on this terminology.) Using this notion we can show

If T is omega-consistent, then ~G is not a theorem of T.

To see how this follows, we must look a bit closer at the Thm-predicate. Thm(x) is defined as

There is a y such that Prf(y,x)

Here Prf(y,x) is a predicate meaning "y is (the Gödel number of) a proof in T of the formula (with Gödel number) x". Every particular assertion of the form Prf(n,#A), where n is any numeral, is decidable in T, so that the following holds:

If P is a proof in T of A, then T |- Prf(#P,#A)

If n is not a numeral corresponding to the Gödel number of a proof in T of A, then T |- ~Prf(n,#A)

Now if ~G were a theorem of T, then (by the defining property of G) it would be provable in T that there is a y such that Prf(y,#G). However, since G is not in fact a theorem of T if T is consistent, there is no proof in T of A, and therefore ~Prf(n,#G) is provable in T for every numeral n. This makes T omega-inconsistent.

Gödel's second incompleteness theorem

The second incompleteness theorem for T states that a particular formula, Con_T, meaning "T is consistent", is not a theorem of T, if T is in fact consistent.

The basic idea behind the proof of this is the following: the proof of the first incompleteness theorem shows that if T is consistent, then G is not provable in T. (Thus here it is essential to use the version of the theorem proved by Gödel.) But this first incompleteness theorem, we find on inspection, is provable in T itself. So if the consistency of T were provable in T itself, then G would also be provable in T, which it isn't (for consistent T).

To carry out this argument in detail - which was only done by Bernays and Hilbert some years after Gödel's paper first appeared - we need to establish the following principles concerning the proof predicate Thm:

(P2) For every sentence A, T |- []A=>[][]A

(P3) For all sentences A and B, T |- [](A=>B)=>([]A=>[]B)

Here => is the if-then connective: "A=>B" means "if A then B".

Note that what is stated in principle (P2) is that each instance of the principle (P1) is provable in T itself. (P3) states that for each instance of modus ponens, it is provable in T that this instance of modus ponens holds for T. Here modus ponens is the rule whereby B is inferred from A and A=>B. Establishing (P2) and (P3) requires a great deal of formal manipulation, which is why the details are usually skipped in proofs of Gödel's theorem.

Using (P1)-(P3) together with (1) (and a little logic in T) we can carry out a rigorous version of the proof of the second incompleteness theorem:

By (1) we have

(2) T |- G=>~[]G

By (P1) and (2) we have

(3) T |- [](G=>~[]G)

(3) together with (P3) yield

(4) T |- []G=>[]~[]G

But from (P2) we also have

(5) T |- []G=>[][]G

Combining (4) and (5) and using the definition of Con_T, we get

(6) T |- []G => ~Con_T

and thus

(7) T |- Con_T => ~[]G

and finally, using (7) and (1),

(8) T |- Con_T => G

We can now conclude that T |-Con_T does not hold for consistent T, since this would imply T |- G.

Henkin's problem and Löb's theorem

The Gödel sentence G says of itself that is unprovable in T, and by reflecting on the meaning of G we can conclude that it is true and unprovable in T, assuming every theorem of T to be true. It occurred to Leon Henkin to form another sentence H which says of itself that it is provable in T, and ask whether this sentence H is provable in T or not.

In this case we aren't helped in any obvious way by reflecting on the meaning of H: all we get is that H is provable in T if and only if it is true, which on the face of it is compatible both with H being true and provable in T, and with H being false and not provable in T.

Löb solved this problem by proving the following strengthening of Gödel's second incompleteness theorem, known as Löb's theorem:

If T |- []A=>A then T |- A

That is, if it is provable in T that A is true if provable in T, then in fact A is provable in T. In particular, the Henkin sentence H is provable in T, since it is provable in T that H is true if provable in T. Note that Gödel's second incompleteness theorem is a special case of Löb's theorem, obtained by letting A be a logical contradiction.

Löb proved the theorem by an ingenious construction generalizing the proof of Gödel's second theorem. (Löb's argument is given here.) The following simple proof, which infers Löb's theorem from Gödel's second theorem, was discovered only some years later (by Kreisel): Suppose T |- []A=>A. Let T' be the theory obtained by adding ~A as a new axiom to T. In this theory T', ~[]A is provable, i.e. it is provable in T' that A is not provable in T. But that A is not provable in T is the same as saying that T' is consistent. Thus the consistency of T' is provable in T'. But by Gödel's second incompleteness theorem, this means that T' is inconsistent, i.e. A is in fact provable in T.

Rosser's improvement of Gödel's theorem

Rosser introduced a variant of the Gödel sentence which allowed him to improve on the result by eliminating the assumption of omega-consistency. For the Rosser sentence R, we can prove that if T is consistent, then neither R nor ~R is provable in T. Informally, the meaning of R is "if this sentence is provable in T, then there is a smaller proof in T of its negation".