### 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,^{101} 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^{102} 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 ...

Get *Theory of Computation* now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.