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 entseheidbar werden. Analoges gilt auch für das Axiomensystem der Mengenlehre"

(I can't speak english good enough, to translate this)

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

Is the theorem (I just quoted) proved by someone? Has someone formulated Gödel's idea more precisely? Is there any research in this area?