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 |- Ato 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

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<=>~[]GThus, 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".

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.

(P1) For every sentence A, If T |- A, then T |- []AIn 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:

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.If T is consistent, then G is not a theorem of 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

To see how this follows, we must look a bit closer at the Thm-predicate. Thm(x) is defined asIf T is omega-consistent, then ~G is not a theorem of T.

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.

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=>~[]GBy (P1) and (2) we have

(3) T |- [](G=>~[]G)(3) together with (P3) yield

(4) T |- []G=>[]~[]GBut from (P2) we also have

(5) T |- []G=>[][]GCombining (4) and (5) and using the definition of Con

(6) T |- []G => ~Conand thus_{T}

(7) T |- Conand finally, using (7) and (1),_{T}=> ~[]G

(8) T |- ConWe can now conclude that T |-Con_{T}=> G

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 |- AThat 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.