Mathematical logic and foundations Proof
Proof of Cantor's theorem
Proof
Cantor's argument is elegant and remarkably simple. The complete proof is presented below, with detailed explanations to follow.
By definition of cardinality, we have for any two sets and if and only if there is an injective function but no bijective function from to . It suffices to show that there is no surjection from to . This is the heart of Cantor's theorem: there is no surjective function from any set to its power set. To establish this, it is enough to show that no function (that maps elements in to subsets of ) can reach every possible subset, i.e., we just need to demonstrate the existence of a subset of that is not equal to for any . Recalling that each is a subset of , such a subset is given by the following construction, sometimes called the Cantor diagonal set of :
This means, by definition, that for all , if and only if . For all the sets and cannot be equal because was constructed from elements of whose images under did not include themselves. For all either or . If then cannot equal because by assumption and by definition. If then cannot equal because by assumption and by the definition of .
Equivalently, and slightly more formally, we have just proved that the existence of such that implies the following contradiction:
Therefore, by reductio ad absurdum, the assumption must be false. Thus there is no such that ; in other words, is not in the image of and does not map onto every element of the power set of , i.e., is not surjective.
Finally, to complete the proof, we need to exhibit an injective function from to its power set. Finding such a function is trivial: just map to the singleton set . The argument is now complete, and we have established the strict inequality for any set that .
Another way to think of the proof is that , empty or non-empty, is always in the power set of . For to be onto, some element of must map to . But that leads to a contradiction: no element of can map to because that would contradict the criterion of membership in , thus the element mapping to must not be an element of meaning that it satisfies the criterion for membership in , another contradiction. So the assumption that an element of maps to must be false; and cannot be onto.
Because of the double occurrence of in the expression "", this is a diagonal argument. For a countable (or finite) set, the argument of the proof given above can be illustrated by constructing a table in which
- each row is labelled by a unique from , in this order. is assumed to admit a linear order so that such table can be constructed.
- each column of the table is labelled by a unique from the power set of ; the columns are ordered by the argument to , i.e. the column labels are , ..., in this order.
- the intersection of each row and column records a true/false bit whether .
Given the order chosen for the row and column labels, the main diagonal of this table thus records whether for each . One such table will be the following:
The set constructed in the previous paragraphs coincides with the row labels for the subset of entries on this main diagonal (which in above example, coloured red) where the table records that is false. Each row records the values of the indicator function of the set corresponding to the column. The indicator function of coincides with the logically negated (swap "true" and "false") entries of the main diagonal. Thus the indicator function of does not agree with any column in at least one entry. Consequently, no column represents .
Despite the simplicity of the above proof, it is rather difficult for an automated theorem prover to produce it. The main difficulty lies in an automated discovery of the Cantor diagonal set. Lawrence Paulson noted in 1992 that Otter could not do it, whereas Isabelle could, albeit with a certain amount of direction in terms of tactics that might perhaps be considered cheating.
Where this leads
3 pages build on this one.
Further reading
- Wikipedia, page 341442, revision 1356713544, Cantor's theorem, section Proof. adopted
About this page
| Tag | 2WPGB3N4A7 |
|---|---|
| URI | m2://2WPGB3N4A7 |
| Kind | proof |
| Writing | W0 stub |
| MSC | 03E10 |
| Proves | Cantor's theorem |
| Changed | 4 November 2026 |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
- edge uses out: each node that the argument needs (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.
What links here
No page links to this page yet.