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 <i>that the undecidable propositions presented by Gödel become decidable by the adjunction of suitable higher types</i> proved by someone? Has someone formulated Gödel's idea more precisely? Is there any research in this area?