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:

The letter ...	stands for...
C	T is Consistent
S	T is Sound
N	T is Negation-complete
D	T is Decidable
E	T's language is sufficiently Expressive
G	T is sufficiently stronG

The new material in this post deals with the new property that appears in the last row of this table.

Recall that, in a previous post, we showed that any AFT that is sound and sufficiently expressive must be negation-incomplete, or, written in pseudo-propositional logic (this should really be a universally quantified formula):

Theorem 1: (S ∧ E) → ¬ N

Soundness, by itself, is not enough to ensure incompleteness. Neither is sufficient expressiveness. To ensure incompleteness, both properties are needed. However, it is possible to weaken one of these properties; and as long as we simultaneously strengthen the other property, we can still guarantee incompleteness.

Notice that soundness is stronger than consistency.  S → C holds because, if an AFT only proves true sentences, then it cannot prove both a sentence and its negation. However, consistency does not imply soundness. For example, an AFT could prove all of the false sentences and not be inconsistent, as long as it does not prove a single true sentence.

So, we can weaken the S condition down to the C condition. However, to ensure incompleteness, we will strengthen the E condition to the G condition, yielding:

Theorem 2: (C ∧ G) → ¬ N

All that is left to do is define the property G and give a proof sketch for this theorem.

We say that an AFT of arithmetic is sufficiently strong iff it captures all effectively decidable numerical properties. Recall that capturing a property is stronger than expressing a property.

Now, to prove theorem 2, we can use the following two lemmata:

Lemma 1: (C ∧ N) → D

which was proved in an earlier post, and

Lemma 2: (C ∧ G) → ¬ D

which states that "no consistent, sufficiently strong AFT is decidable." One way to prove this lemma is to assume that C, G and D are all true and exhibit a contradiction using Cantor's diagonalization method (a proof of this type was discussed in this post).

Finally, we can easily write a formal proof in propositional logic of Theorem 2, that is, N is false under the assumption that C ∧ G is true.

1. C ∧ G [Assumption]
2. (C ∧ G) → ¬ D [Lemma 2]
3. ¬ D [Modus ponens applied to 1 and 2]
4.  (C ∧ N) → D [Lemma 1]
5. ¬ D → ¬ (C ∧ N) [Contraposition of 4]
6. ¬ (C ∧ N) [Modus ponens applied to 3 and 5]
7. ¬ C  ∨ ¬ N [one of De Morgan's laws]
8. C → ¬ N [logical equivalence applied to 7]
9. C [simplification of 1]
10. ¬ N [Modus ponens applied to 8 and 9]

So, from C ∧ G, we derived ¬ N, that is:

Theorem 2: Consistent, sufficiently strong formal systems of arithmetic are incomplete.