Consistent, sufficiently strong formal systems of arithmetic are incomplete

In Chapter 6, Peter Smith proves another incompleteness theorem. To place this theorem in context, let's review some definitions about axiomatized formal theories (or AFTs) from earlier posts.

Let T be some AFT.

• T is consistent iff (if and only if) there is no sentence φ such that T proves both φ and ¬ φ.
• T is sound iff every theorem that T proves is true according to the interpretation that is built into T's language.
• T is (negation-)complete iff for every sentence φ in T's language, T proves either φ or ¬ φ.
• T is decidable iff there is an algorithm that, given any sentence φ in T's language, determines whether or not T proves φ.
• If needed, go here to review what it means for T's language to express a numerical property P or a numerical relation R.
• If needed, go here to review what it means for T to capture a numerical property P or a numerical relation R. 
• If needed, go here to review what it means for T's language to be sufficiently expressive.

We'll use the following abbreviations: