Well, let's agree to disagree on the recommendation of Manin's book. I think it's confusing, rambling and often downright unhelpful. The reason Godel's theorem

Well, let's agree to disagree on the recommendation of Manin's book. I think it's confusing, rambling and often downright unhelpful. The reason Godel's theorem is proved as (little other than) a corollary to Tarski's in Manin's book is that Manin presents a weaker, semantic version of Godel's theorem that is indeed little other than a corollary to Tarski's. See Manin's discussion of "Godel's argument" and particularly step (c) on p.255 of his book. Manin explains that Godel's proof doesn't use the assumption that D is a subset of T (all provable statements are true), but that he, Manin, doesn't think it's important to care about that, so he presents the theorem this way. In the form Godel proved it, the theorem doesn't require any semantic assumptions. Manin is entitled to his own spin on what is and isn't important about the Incompleteness Theorem, but it should be apparent to you that his presentation uses an assumption that Godel's theorem in its general form doesn't require. It's interesting (where by interesting I mean "weird, and goes toward explaining my opinion of Manin's book") that Manin nowhere even deigns to mention Godel's Second incompleteness theorem, the one about axiomatic systems being unable to prove their own consistency. Now if you were to take up a better book than Manin's, say Smullyan's Godel's Incompleteness Theorems, and study the proof of the second incompleteness theorem, you'd find out that its proof requires a syntactic proof of the first theorem, the proof that Manin says isn't important. This is because proving the second theorem entails formalizing the proof of the first theorem inside the axiomatic system itself, and you can't do that with a proof that uses semantic arguments and talks about true and false theorems (why? because of Tarski's undefinability of truth!). Think of that what you will.