Peter Smith's overview of Gödel's incompleteness theorems

Finally! As was my initial goal, I now turn my attention to Peter Smith's book on the proof of Gödel's incompleteness theorems (by the way, I own the first edition of his book; so that is the one I will be referring to). I did not expect to spend that much time on Nagel and Newman's book. But it was worthwhile in getting the big picture.

Chapter 1 is an introductory and user-friendly discussion of topics that were mentioned in earlier posts, such as basic arithmetic, formal systems, (in)completeness, consistency, the statement of Gödel's incompleteness theorems and some of their implications. Therefore, in this post, I will just highlight the points where Smith provides new information or has a different perspective.

1. Smith makes the distinction between proving a theorem and deriving a theorem in a formal system. While "prove" and "derive" can be seen as synonyms, "proved" is often interpreted as "proved to be true," whereas "derived in a formal system" just means "resulting from the application of inference rules starting from axioms" without any assumption that the theorems of the system are true. If the axioms of the system are all true (in some interpretation) and its rules of inference are truth-preserving, then the theorems of the system are all true. In this case, we say that the system is sound. In general, however, soundness is not a required feature of formal systems. So the term "derive" is more neutral with respect to truth than the term "prove."
2. Smith makes another, more important distinction between two types of completeness, also related to the concept of truth. He defines negation completeness, which is different from semantic completeness that we discussed here. A formal system is negation complete if, for every well-formed formula (or wff) w in the system, either w is a theorem or ¬ w is a theorem. In other words, every wff of the formal system is decidable (either it or its negation is a theorem). Notice that negation-completeness is independent of the truth of the theorems in the system. Each and every theorem in a negation-complete system could be false and every truth may be a non-theorem in this system. In contrast, Nagel and Newman framed the first incompleteness theorem in terms of semantic completeness, whereby all true statements are theorems. While these two types of completeness can be related to each other through the concept of soundness, it appears to be worthwhile to keep the distinction in mind.
3. Smith presents a slightly different perspective on the first theorem and the "incompletability" of formal systems of arithmetic. Recall how adding Gödel's sentences (as axioms) to a formal system cannot make it complete, since a Gödel sentence can always be constructed for such an augmented formal system. Repeating this process of augmentation will yield an infinite number of increasingly strong (yet still incomplete) formal systems and associated Gödel sentences. None of these Gödel sentences can be derived in the original formal system. Therefore, there is an infinite number of true Gödel sentences that the original formal system cannot derive.
4. Smith makes a good point regarding the second theorem: what would be the value of a proof of consistency of F within F, even if such a proof could be obtained? Recall point 1 above: finding a derivation of a theorem T in F does not mean that T is true. In fact, as we already argued, if a formal system is inconsistent, it derives every single wff and its negation, including the wff that "states" it own consistency! In other words, a proof of this wff would not provide much support for its truth. So the fact that this proof does not exist does not appear to be such a negative result. So the impact of the second theorem must lie elsewhere: indeed, if an augmented formal system (with added axioms, see point 3 above) is consistent, then so is the initial formal system, since removing axioms cannot introduce inconsistencies. Furthermore, if a formal system could prove the consistency of an augmented version of itself, it could prove its own consistency as well. Therefore, a formal system cannot prove its own consistency nor the consistency of any richer formal system, which is a serious blow to Hilbert's programme, whose goals included finding finitary proofs of consistency for non-finitary systems. 
5. Smith describes how to mirror arithmetic within set theory, which implies that no formal system for set theory can be negation complete, using a reduction similar to those we discussed in relative proofs of consistency.