Yes I agree. And it’s cool that Cantor himself came up with this proof. It also serves as the standard technique for getting rid of countably many pesky problems. For example in Cantor’s diagonal argument, we are listing the decimal representations of real numbers, but some real numbers have two distinct representations. For example .5 = .49999… So when we form the antidiagonal, how do we know that even if it’s not on the list, its OTHER representation is?
The way this is usually handled is that we vigorously wave our hands (that part is essential) and say, “There are only countably many such pesky dual-representations so it doesn’t matter.” A thoughtful person might respond, “How do you know it doesn’t matter?” Our example shows how to prove that the dual representations don’t matter.
I don’t think any of us are in a position to do that! He was a great man in multiple endeavors. I don’t know much about him, but why do you dislike him? Is it the pipe?
How does that change your estimation of Russell?
There is no question that type theory is making a comeback as a potential foundation for math. The drive in this direction is from automated checking of proofs. There’s a big movement called homotopy type theory (HOTT) that’s the buzzphrase and Wiki page to know.
One thing I know from type-theoretic approaches to foundations is that they are associated with denial of the law of the excluded middle. I know very little about this entire area. It makes sense that this idea would gain currency in our age of computers; since there are many sets of natural numbers such that neither they nor their complement are computable. So neither is “true” in a world where truth is whatever can be determined by an algorithm.
The mathematical philosophy of all this goes under the name of intuitionism (if it’s classic 1930’s Brouwer type) or neo-intuitionism (if it’s more recent).
h
Yay! Me too! I had a vague idea about it before and now it’s beautifully simple.
What leads you to your interest in type theory? Just curious. Well if HOTT eventually gains majority mindshare, I will think of that as Brouwer’s revenge. There is another alternative
foundation that’s made huge inroads into much of modern research-level math, Category theory. Attitudes toward foundations are a matter of historical contingency.