I'm not sure why pier25 was reminded, but Russell's type theory and Gödel's incompleteness theorem are closely related. They both arose in response to the foundational crisis in mathematics [1].
Russell stumbled onto Russell's paradox (among others) and it shook mathematicians' confidence that everything in math was built on top of a perfectly consistent and stable foundation. If you can define a set that it "the set of sets that don't contain themself" then what other kind of crazy talk can you say in math? How do you know proven things are true and false things can't be proven in the face of weirdness like that?
Russell tried to solve the problem by inventing type theory. Types stratify the universe of values such that "the set of sets that don't contain themself" is no longer a valid statement to make.
Meanwhile, Gödel went and proved that, sorry, no, math is not consistent and complete. There are statements that are true but which cannot be proven.
Russell stumbled onto Russell's paradox (among others) and it shook mathematicians' confidence that everything in math was built on top of a perfectly consistent and stable foundation. If you can define a set that it "the set of sets that don't contain themself" then what other kind of crazy talk can you say in math? How do you know proven things are true and false things can't be proven in the face of weirdness like that?
Russell tried to solve the problem by inventing type theory. Types stratify the universe of values such that "the set of sets that don't contain themself" is no longer a valid statement to make.
Meanwhile, Gödel went and proved that, sorry, no, math is not consistent and complete. There are statements that are true but which cannot be proven.
[1]: https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou...