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?

  • 1
    $\begingroup$ You can see this post and the biblio in this one. See also in SEP the entry on Gödel's Incompleteness Theorems. An english translation of Gödel's paper is available in Van J.Heijenoort (ed.), 1967, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Harvard UP 1967. $\endgroup$ Apr 16, 2014 at 13:20
  • 1
    $\begingroup$ Of course, you can find it also in Kurt Gödel, Collected Works I. Publications 1929–1936, (S.Feferman et al. eds.), Oxford UP 1986. $\endgroup$ Apr 16, 2014 at 13:21
  • $\begingroup$ @MauroALLEGRANZA thanks for the references. I didn't notice that other question. About the relation between the two, i do not understand you comment. Any two true theorems are corollaries of each other. So is the First Incompleteness Theorem an easy corollary of the Second, a difficult corollary of the Second, or the Second cannot be used at all in a meaningful way to prove the First? $\endgroup$
    – Alexey
    Apr 16, 2014 at 13:41
  • $\begingroup$ The First can be obtained as a corollary of the Second. However, the Second is an order of magnitude harder, so that is not a helpful fact. $\endgroup$ Apr 16, 2014 at 13:43
  • $\begingroup$ This is what i thought: the First is an easy corollary of the Second. So, is this true? $\endgroup$
    – Alexey
    Apr 16, 2014 at 13:43

2 Answers 2


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.


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.

  • $\begingroup$ I think what's normally called Gödel's first incompleteness theorem is not Theorem VI but the generalisation he goes on to make. Theorem VI is only about his system $P$; the first theorem is usually taken to be of the form "For any theory which [like $P$] is primitively recursively axiomatized and defines every primitive recursive function ....". $\endgroup$ Apr 16, 2014 at 15:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.