Modern book on Gödel's incompleteness theorems in all technical details Is there a modern book on Gödel's incompleteness theorems that goes into each and every technical aspect of the proof of them (a classical one, if such exists)? I'm not interested in popular literature that constantly draws analogies with computers, printers, etc. I want the real thing. P.S. I also started reading Gödel's 1931 original paper, but thought that since then the proof could have become more elegant and simple.

There are several senses of "complete":

* If you want a complete discussion of the incompleteness theorems and their related computability and philosophical concepts, the best modern reference is Peter Smith's book _An Introduction to Gödel's Theorems_.

* If you want a complete technical proof of the theorems, but with little discussion of computability and without philosophical asides, then Smorynski's article "The incompleteness theorems" in the _Handbook of Mathematical Logic_ is an exceptional reference. This article includes quite general statements of the theorems and results on formalizing the incompleteness theorems into systems such as PRA. This paper was also mentioned in this answer. The paper is written as a reference paper in a research-level handbook, so the ideal reader needs to be prepared for exposition at that level.