Prof. Peter Smith of Cambridge University has posted sixteen chapters of his work-in-progress on Gödel’s incompleteness theorems and related mathematical/logical/philosophical goodness in PDF format, beautifully typeset using LaTeX.
I’ve read the first twelve chapters, which take you through Gödel’s first and second incompleteness theorems, Tarski’s theorem on the undefinability of truth, and (the most surprising result, IMO), Löb’s theorem.
You’ll need a background in symbolic logic to understand it. If you don’t know your ∀s from your ∃s, you’ll be lost.
Smith takes the opposite approach from Boolos and Jeffrey, taking you through Gödel’s theorems using only the apparatus of primative recursion, saving full-blown recursive function theory and other topics in computability theory for later.
It’s been a while (about seven years) since I’ve been through the material, but I learned a lot of stuff I didn’t pick up the first time around.
(þ Brian Weatherson.)