the true reason of the incompleteness of formal systems

Question

A 3/4 year ago, I read Gödel's beautiful paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme 1". There is one thing, I never understood.

In a footnote, Gödel says the following:

"Der wahre Grund für die Unvollständigkeit, welche allen formalen Systemen der Mathematik anhaftet, liegt, wie im zweiten Tell dieser Abhandlung gezeigt werden wird, darin, dass die Bildung immer höherer Typen sich ins Transfinite fortsetzen lässt, während in jedem formalen System höchstens abzählbar viele vorhanden sind. Man kann nämlich zeigen, dass die hier aufgestellten unentscheidbaren Sätze durch Adjunktion passender höherer Typen (z. B. des Typus $\omega$ zum System $P$) immer entscheidbar werden. Analoges gilt auch für das Axiomensystem der Mengenlehre"

Meltzer's translation renders this in English as:

"The true source of the incompleteness attaching to all formal systems of mathematics, is to be found — as will be shown in Part II of this essay — in the fact that the formation of ever higher types can be continued into the transfinite (cf. D. Hilbert 'Über das Unendliche', Math. Ann. 95, p. 184), whereas in every formal system at most denumerably many types occur. It can be shown, that is, that the undecidable propositions here presented always become decidable by the adjunction of suitable higher types (e.g. of type $\omega$ for the system $P$). A similar result also holds for the axiom system of set theory."

Famously, Gödel never published part 2 of his paper.

Is the theorem which states that the undecidable propositions presented by Gödel become decidable by the adjunction of suitable higher types proved by someone? Has someone formulated Gödel's idea more precisely? Is there any research in this area?

Answer 1

I think the main idea here is that, if you have a reasonably strong formal system $T$ (so that the incompleteness theorems apply to it) and you then strengthen it to a "higher type" system $T^+$ in which you can talk about (and quantify over) subsets of the universe that $T$ describes (so that second-order concepts from the point of view of $T$ are first-order from the point of view of $T^+$) and if $T^+$ has suitable comprehension axioms, then $T^+$ will be able to formalize a definition of truth for the language of $T$ and prove that the axioms of $T$ are true and that formal deduction preserves truth. Thus, $T^+$ can prove the consistency of $T$ and, as a consequence, prove the usual Goedel sentence of $T$.

Typical examples are: (1) $T$ is Peano arithmetic and $T^+$ is second-order arithmetic. (2) $T$ is Zermelo-Fraenkel set theory and $T^+$ is Morse-Kelley class theory. (3) (the example Goedel mentioned) $T$ is type theory with an $\omega$-indexed hierarchy of types and $T^+$ is type-theory with an $(\omega+1)$-indexed hierarchy of types.