Gödel's incompleteness theorems: where to learn? Is there a straightforward relation between the two?

Question

What would be a good textbook or paper to learn the proofs of the two Gödel's incompleteness theorems from?

I would prefer it to be as close to the original proofs as possible. I have not tried to look into the Gödel's original papers however because unfortunately i do not read German, and i am worried that the terminology of the 1930s might be somewhat different from the one currently used.

In addition, i have a simple question: do i understand correctly that the First Incompleteness Theorem is a straightforward corollary of the Second?

Answer 1

What would be a good textbook or paper to learn the proofs of the two Gödel's incompleteness theorems from? I would prefer it to be as close to the original proofs as possible.

For the first theorem, my Introduction to Gödel's Theorem is closer to Gödel's original line of proof then many textbooks.

In more detail, Gödel's 1931 proof uses facts about so-called primitive recursive functions: these functions are a subclass of the computable numerical functions, i.e. a subclass of the functions which a suitably programmed computer could evaluate (abstracting from practical considerations of time and available memory).

A more general treatment of the effectively computable functions (arguably capturing all of them) was developed a few years later, and this in turn throws more light on the incompleteness phenomenon; but you don't really need this additional generality.

So, there's a choice to be made. Do you look at things in roughly the historical order, learning a little about the primitive recursive functions, introducing theories of formal arithmetic and learning how to prove initial versions of Gödel's incompleteness theorem before moving on to look at the general treatment of computable functions? Or do you start off looking at more of the general theory of computation first, before turning to the incompleteness theorems later? Some very good textbooks like those by Boolos, Burgess and Jeffrey, or by Epstein and Carnielli, do things the second way. My book goes the first way around. You pays your money and you takes your choice.

For the second theorem there is no original proof. Gödel in his 1931 paper just states the theorem, arm-waves at how it might be proved, and planned to write a second part of the paper filling in some details. Later he told Bernays how to do it (while they were travelling across the Atlantic together), and Bernays wrote up the first published version of a proof of the second theorem for a certain system of arithmetic in Hilbert and Bernays. That proof is pretty heavy going, and there are nicer later versions, e.g. in Boolos's Logic of Provability, or sketched out in my book.

As to the relation between the two, basically the second-theorem is proved by showing that the argument for the first theorem (which is in one sense quite elementary) can itself be coded up in arithmetic. So there is a good sense in which the second theorem is derived by thinking formally about the (informal) argument for the first theorem. But once you've got the second theorem, which immediately shows that $Con(T)$ is undecidable in suitable theory $T$, you've got another witness to the first theorem, that suitable $T$ has undecidable sentences. In that sense, the second theorem implies the first.

Answer 2

See Kurt Gödel, Collected Works. Volume I : 1929-1936.

English translation of : Uber formal unentscheidbare Satze der Principia mathematica und verwandter Systeme I (1931), page 144-on.

Section 2 , page 173 :

Theorem VI. For every $\omega$-consistent recursive class $k$ of FORMULAS there are recursive CLASS SIGNS $\tau$ such that neither $v Gen r$ nor $Neg (v Gen r)$ belongs to $Flg(k)$ (where $v$ is the FREE VARIABLE of $r$).

This is the First Theorem.

Section 4 , page 191 :

The results of Section 2 have a surprising consequence [emphasis added] concerning a consistency proof for the system $P$ (and its extensions), which can be stated as follows :

Theorem XI. Let $k$ be any recursive consistent class of FORMULAS; then the SENTENTIAL FORMULA stating that $k$ is consistent is not $k$-PROVABLE; in particular, the consistency of $P$ is not provable in $P$, provided $P$ is consistent (in the opposite case, of course, every proposition is provable [in $P$]).

The proof (briefly outlined) is as follows: [...]

See also the Introductory Note by Stephen Cole Kleene, page 186 :

In Section 4, the final Theorem XI is Gödel's famous "second incompleteness theorem". [...] So Gödel claims that the formula (*) [...] is provable in $P_k$ (or as he puts it, [...] is $k$-PROVABLE). [...]

A demonstration that (*) is provable was given in Hilbert and Bernays (1939), pages 283-340.

Of course, in a textbook presentation of the above results, it is possible to rearrange them in different ways, according to "didactical" necessity.