Gödel on the “True Reason” for Incompleteness

Question

In footnote 48a of his famous paper on incompleteness, Gödel writes:

[T]he true reason for the incompleteness inherent in all formal systems of mathematics is that the formation of ever higher types can be continued into the transfinite (see Hilbert 1926, page 184), while in any formal system at most denumerably many of them are available. (Gödel 1931a, trans. van Heijenoort)

I have a fairly good grasp of his theorems and their proof, but this remark is rather opaque to me (and the sentences that follow it didn’t help). Perhaps I don’t have a sufficient understanding of the theory of (higher) types, which usually plays little role in modern expositions of Gödel’s theorems.

Could somebody explain, in more detail and in modern terms, what Gödel was trying to communicate?

Answer 1

A fairly complete answer can be found in the following references (mainly the first one):

• "Gödel and Set Theory", Kanamori, Bull. Symbolic Logic, June 2007
• "Infinity in Mathematics: Is Cantor Necessary?", Feferman, Philosophical Topics, Fall 1989
• "Kurt Gödel", Kreisel, Biographical Memoirs of the Fellows of the Royal Society

I will summarize the main points.

Gödel is referring to Russell's theory of types, as expounded in Principia Mathematica (and note the mention of P.M. in the title of Gödel's paper). This divided the mathematical universe into levels: numbers (type 0), sets of numbers (type 1), sets of sets of numbers (type 2), etc.

In 1932, Gödel expanded on footnote 48a in a passage quoted by Kanamori:

If we imagine that the system $\mathcal{Z}$ is successively enlarged by the introduction of variables for classes of numbers, classes of classes of numbers, and so forth, together with the corresponding comprehension axioms, we obtain a sequence (continuable into the transfinite) of formal systems that satisfy the assumptions mentioned above, and it turns out that the consistency ($\omega$-consistency) of any of those systems is provable in all subsequent systems.

Here $\mathcal{Z}$ is basically Peano Arithmetic in its modern formulation. Adding all these types, as contemplated in the 1932 passage, would essentially give us Russell's system---except that Russell does not continue types into the transfinite.

The closest modern comparison to Russell's type hierarchy is the cumulative hierarchy of ZFC. But there are two crucial differences. First, Russell does not allow "mixed" types: no putting numbers and sets of numbers into the same class. Also, Russell's types go up only through the finite levels.

Okay, what does this have to do with incompleteness? The simplest modern illustration: Con(PA) can be proved in second-order arithmetic. As Gödel noted in the 1931 paper, his undecidable proposition follows from Con(PA)---hence the second incompleteness theorem, that PA does not prove Con(PA). Second-order arithmetic cannot prove its own consistency, but you can prove it consistent inside third-order arithmetic. And so on.

These consistency proofs rely on the ability to formalize "truth" for one system in a system of the next higher type. Kanamori summarizes the meaning of the footnote 48a and the 1932 passage this way:

The salient points of these passages is that the addition of the next "higher type" to a formal system leads to newly provable propositions of the system; the iterative types can be continued into the transfinite; and in set theory, new propositions become analogously provable from "axioms of cardinality".

There is much more in the references, including connections to Gödel's work on the constructible hierarchy. I will mention only that in Gödel's paper "What is Cantor's Continuum Problem?", he expressed the hope that large cardinal axioms might decide CH. Such axioms are a natural evolution of the type hierarchy into the transfinite.