Sound formal systems with sufficiently expressive languages are incomplete

In chapter 5, Peter Smith uses a counting argument to prove that sound axiomatized formal theories (AFTs) that can express a good amount of arithmetic are incomplete. In short: since their set of theorems is effectively enumerable but their set of true sentences is not, the two sets must be different. In a sound theory, the theorems are all true. Therefore, some truths must remained unproved in such theories.

Let's start with a definition. The language of an AFT of arithmetic is sufficiently expressive if and only if:

1. It can express quantification over numbers, and
2. It can express every effectively decidable two-place numerical relation.

Now, to the pivotal theorem of this chapter: