axiom 1v. (∃u)(v ∀ (u(v) ≡ a))
on substituting for v or u any variables of types n or n + 1 respectively,
and for a a formula which does not contain u free. This axiom represents
the axiom of reducibility
"The system P of footnote 48a is Godel's
streamlined version of Russell's theory of types built on the
natural numbers as individuals, the system used in . The last
sentence ofthe footnote
KurtGodel[1931,p. 178] wrote of his comprehension axiom IV, foreshadowing
his approach to set theory, "This axiom plays the role of [Russell's]
axiom of reducibility (the comprehension axiom of set theory)."
"the axiom of reducibility is generally regarded as the grossest philosophical expediency "
from the collected works of godel volume 3
godel states 1939
"to be sure one must observe that the axiom of reducibility appears in
different mathematical systems under different names and forms"
the standford encyclopdeia of philosophy says of AR
many critics concluded that the axiom of reducibility was simply too ad
hoc to be justified philosophically
Such an axiom has no place in mathematics, and anything which cannot be
proved without using it cannot be regarded as proved at all.
This axiom there is no reason to suppose true; and if it were true, this
would be a happy accident and not a logical necessity, for it is not a
tautology. (THE FOUNDATIONS OF MATHEMATICS* (1925) by F. P. RAMSEY
Furthermore, it's openly acknowledged that Godel's theorem can only apply internally to a system in which proof comes from within the system.
What Godel did is invalid as he uses invalid axioms so you cant then say he proved anything
"A. Whitehead and B. Russell, Principia Mathematica, 2nd edition, Cambridge 1925. In particular, we also reckon among the axioms of PM the axiom of infinity (in the form: there exist denumerably many individuals), and the axioms of reducibility and of choice (for all types)"