[pier25]

Reminded me of Gödel's incompleteness theorems.

First incompleteness theorem

Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.

Second incompleteness theorem

For any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.

[igravious]

Honest question. What in the article prompted you to think about Gödel and his theorems? Why were you reminded?

[munificent]

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.

[1]: https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou...

[Jtsummers]

Probably this part from the article:

> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable.

[skywhopper]

I spent the whole article wondering when Gödel would be mentioned, and was disappointed that he wasn't given that the Incompleteness Theorem was at least partly a response to Russell's work, and because it applies directly to computer systems. The conclusions Gödel reached are asserted in the article but not cited which is weird given the other references.

[charlieflowers]

I was reminded of Godel too. For me, it was the part of the article that described Russell's finding of statements that led to paradox, such as "I am lying." If you're allowed to talk about "the set of all sets", then you can state things that can't be dealt with logically. That reminds me of Godel's Incompleteness theorem.

[coldtea]

For one, Godel used the same kind of self-referential statements described in the article ("this proposition is not provable" etc) and used math to create a kind of enumeration of propositions and have the proposition refer to itself.