 With regard to the Second Incompleteness Theorem, the argument relies in part on formalizing the proof of the First Incompleteness Theorem as we saw. This step is omitted in Gödel 1931. He planned to include the step in what would have been a second part II (see footnote 48a of Gödel 1931). But instead of writing it he turned to the continuum  problem.[13]  (Part II was to elaborate on other points too: the ‘true reason for incompleteness,’ and the applicability of the two theorems to other systems.) He perhaps did not feel compelled to attend to what looked like an exercise in formalization, relying instead on the informal argument to convince (in which it succeeded). However this step turned out to be somewhat non-trivial. As Kleene puts it in his introduction to Gödel 1931, of the informal presentation, “Certainly the idea of the argument for Theorem XI (consistency) was very convincing; but it turned out that the execution of the details required somewhat more work and care than had been anticipated.” (See pp. 126–141 of Gödel 1986.) Eventually a complete proof of the Second Theorem was given by Hilbert and Bernays in some seventy pages in their Hilbert and Bernays 1939. A much more compact treatment of the theorem was given by Löb in his Löb 1956, and subsequently Feferman, in his 1960 “Arithmetization of Metamathematics in a General Setting” (Feferman 1960/1961), gave a succinct and completely general treatment of both the First and Second Theorems. But see the supplementary document: