Buy from Amazon

Raymond Smullyan
Godel's incompleteness theorems
The book starts off with a look at the mathematics of self reference, leading to Tarski's theorem of the nonrepresentability of the set of true sentences of a system. Smullyan then moves on to the proof of Gödel's first incompleteness theorem. He first does this in a system including axioms for exponentiation (following Gödel's proof) and then shows how these axioms aren't in fact necessary. The book moves on to questions of consistency of arithmetic, including ωconsistency, leading to a proof of Gödel's second incompleteness theorem. The final two chapters relate these result to the type of mathematical puzzles that Smullyan is best known for.
The book isn't for those without some previous experience in mathematical logic. The reader is rather thrown in at the deep end, and there are certainly simpler ways of presenting this material. However, it would be useful for those wanting consise but rigorous proofs of Gödel's incompleteness theorems without getting distracted by their set theoretic forms, or the details of model theory.