Cantor's theorem and diagonal argument

[fredrik-bakke]

From what I could gather from online sources, what is referred to as "Cantor's diagonal argument" in the library is actually a generalization of the diagonal argument that is known as "Cantor's theorem", and it seems "Cantor's diagonal argument" should be reserved for the uncountability of sequences in types equipped with two distinct elements.

This PR also makes a series of miscellaneous corrections:

• The maybe monad is not a modality
• Countable sets* as opposed to countable types
• Fix #concept invocation for logical equivalences
• Move some lemmas from countable-sets that were actually about the maybe monad

In addition, this PR adds

• A bunch of links and #concept invocations with Wikidata identifiers
• The classical Cantor's theorem
• Cantor's diagonal argument
• The cantor space is uncountable

[fredrik-bakke]

I am tempted to suggest moving Cantor's theorem to set-theory, but since it makes no assumptions on the indexing type the choice is less obvious. Cantor's diagonal argument should for sure be in set-theory though.

[EgbertRijke]

I am not quite sure if I follow you here.

In Über eine elementare Frage der Mannigfaltigskeitslehre, Cantor proves that there cannot be a bijection from X to 2^X. He uses what is now known as a general technique called the diagonal argument. I have trouble seeing why "Cantor's diagonal argument" should only refer to a specific instance of that argument.

Which sources say that?

[fredrik-bakke]

@EgbertRijke While I cannot read German, the following two English translations of "Über eine elementare Frage der Mannigfaltigskeitslehre"

1. https://www.math.stonybrook.edu/~tony/archive/336s20/documents/cantor.html
2. https://www.researchgate.net/publication/335364685_A_Translation_of_G_Cantor's_Ueber_eine_elementare_Frage_der_Mannigfaltigkeitslehre

demonstrate Cantor's argument as follows. They consider given a set $X$ with two distinct elements $x,y \in X$, $x \neq y$. From this, they demonstrate that there are uncountably many sequences on $X$. I.e., elements of $ℕ \to X$. Or indeed pick any infinite $A$ to replace $ℕ$.

This is also what Wikipedia refers to as Cantor's diagonal argument

• https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument

In Wikipedia's article on Cantor's theorem, the theorem is described as a generalization of Cantor's diagonal argument that apply to arbitrary $A$.

• https://en.wikipedia.org/wiki/Cantor%27s_theorem

Interestingly, Wikipedia's article on Cantor's theorem only cites Über eine elementare Frage der Mannigfaltigskeitslehre, in which the proof given in the Wikipedia article doesn't seem to appear. Again, I cannot read German so I may be wrong on this. Still, we can observe two decidedly distinct flavors of argument. One, referred to as "Cantor's diagonal argument" considers infinite sequences of elements from a set with at least two elements, while "Cantor's theorem" considers the powerset of an arbitrary set.

[fredrik-bakke]

If I have convinced you, I am more than happy to formalize a new file on Cantor's diagonal argument. Or, if you know German and can tell me that Cantor indeed demonstrates that no function $A \to \mathcal{P}(A)$ may be surjective in the above-mentioned article, then I will concede. Either way further citations are needed.

[EgbertRijke]

I think I simply did not know that "Cantor's diagonal argument" is used to a specific instance of the diagonal argument. I thought it referred to the style of argument, of which Cantor has given the first (few?) examples, so it feels counterintuitive that it only refers to an instance.

I agree that "Cantor's theorem" states that there is no surjection from any set to its power set. (There are constructively a few different ways to state this, eg with X -> Prop and X -> 2, but in all cases we should call them Cantor's theorem).

Note that we also have a file on Lawvere's fixed point theorem, which generalizes Cantor's diagonal argument (or perhaps in wikipedia's reading, Cantor's theorem).

I looked up how Jech refers to it in his Set Theory textbook, and he simply speaks of "diagonalization" for the method, and he attributes the theorems that |X| < |2^X| and |N| < |R| to Cantor, but doesn't call the second theorem "Cantor's diagonal argument".

[fredrik-bakke]

Right. What set me down this path was a bit of a rabbit hole while I was preparing for class today which I will spare you the details of. 😅

Anyways, then I think we agree. I'll try and explain the terminology and add the necessary citations. In the meantime, I'll mark this PR as a draft.

[EgbertRijke]

Great!

To be clear, I don't think the PR needs much more work. It is fine as it is and I'm glad you're taking this on. I just needed to know what was behind this pull request, as it looked a bit strange at first glance.

[fredrik-bakke]

Alright, I've added the file with what I perceive to be a faithful formalization of Cantor's original diagonal argument. @EgbertRijke

[EgbertRijke]

This is a very nice pull request, clearly a lot of work has gone into making all these improvements and including all the references. A big thanks!

[EgbertRijke]

You can enable auto-merge whenever you're done with this PR

[fredrik-bakke]

Thanks!