Theory of Computation

2.11 UNPROVABILITY FROM UNSOLVABILITY

This section draws from background developed in Section 1.1 and in particular in Subsection 1.1.1. Nevertheless, we will need to indulge in some repetition here, aiming to make this section self-sufficient on one hand, and, on the other, making the underlying logic that we use and discuss here more formal than we managed to get away with so far,¹⁰¹ since in the present section logic will not be just a tool, but primarily will be an object for study—precision is called for!

We will prove here a semantic version of Gödel’s first incompleteness theorem that relies on computability techniques. In this form the theorem states that any “reasonable” axiomatic system that attempts to have as theorems precisely all the “true” (first-order) formulae of formal arithmetic¹⁰² will fail to be complete in this sense: There will be infinitely many true formulae that are not theorems. Imitating Cantor’s separation of infinities of sets, between “small” (enumerable) and “large” (non-enumerable) we will show that the set of true formulae of arithmetic is “computably large” (non c.e., indeed, productive) while the set of provable formulae is “computably small” (c.e.). Thus the two cannot coincide.

The qualifier reasonable could well be replaced by practical: One must be able to tell, algorithmically, whether or not a formula is an axiom—how else can one check a proof, let alone write one? “True” means true in the standard interpretation of the abstract symbols ...