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.
 A: 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.
A: Besides Peter Smith's book (An Introduction to Gödel's Theorems, 2nd ed 2013, Cambridge UP), I suggest (see Wiki and SEP bibliographies) :

Raymond Smullyan, 1991, Gödel's Incompleteness Theorems, Oxford Univ.Press
Roman Murawski, 1999, Recursive Functions and Metamathematics: Problems of Completeness and Decidability, Gödel's Theorems, Kluwer A.P.
Torkel Franzén, 2004, Inexhaustibility: A Non-Exhaustive Treatment, Lecture Notes in Logic 16, A.K.Peters
Torkel Franzén, 2005, Gödel's Theorem: An Incomplete Guide to its Use and Abuse, A.K.Peters.

See also the textbook :

George Tourlakis, 2003, Lectures in Logic and Set Theory. Volume 1 : Mathematical Logic, Cambridge UP;

all the 2nd part of the book (from page 155 until 315) is dedicated to a detailed exposition of 1st and 2nd (and this is not easy to find in textbooks) Gödel's Incompleteness Theorems.
