Cantor's theorem
For finite sets, Cantor's theorem can be seen to be true by simple enumeration of the number of subsets.
The theorem is named for Georg Cantor, who first stated and proved it at the end of the 19th century.
Cantor's theorem had immediate and important consequences for the philosophy of mathematics.
For instance, by iteratively taking the power set of an infinite set and applying Cantor's theorem, we obtain an endless hierarchy of infinite cardinals, each strictly larger than the one before it.
The complete proof is presented below, with detailed explanations to follow.
This is the heart of Cantor's theorem: there is no surjective function from any set
, such a subset is given by the following construction, sometimes called the Cantor diagonal set of
implies the following contradiction: Therefore, by reductio ad absurdum, the assumption must be false.
Finally, to complete the proof, we need to exhibit an injective function from
The argument is now complete, and we have established the strict inequality for any set
For a countable (or finite) set, the argument of the proof given above can be illustrated by constructing a table in which Given the order chosen for the row and column labels, the main diagonal
constructed in the previous paragraphs coincides with the row labels for the subset of entries on this main diagonal
[3] Each row records the values of the indicator function of the set corresponding to the column.
coincides with the logically negated (swap "true" and "false") entries of the main diagonal.
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.
For instance, in our example the number 2 is paired with the subset {1, 2, 3}, which contains 2 as a member.
Other natural numbers are paired with subsets that do not contain them.
Using this idea, let us build a special set of natural numbers.
is selfish because it is in the corresponding set, which contradicts the definition of
maps to a subset of natural numbers that contains
Cantor's theorem and its proof are closely related to two paradoxes of set theory.
In order to distinguish this paradox from the next one discussed below, it is important to note what this contradiction is.
[1] As a point of subtlety, the version of Russell's paradox we have presented here is actually a theorem of Zermelo;[4] we can conclude from the contradiction obtained that we must reject the hypothesis that RU∈U, thus disproving the existence of a set containing all sets.
This was possible because we have used restricted comprehension (as featured in ZFC) in the definition of RA above, which in turn entailed that Had we used unrestricted comprehension (as in Frege's system for instance) by defining the Russell set simply as
, then the axiom system itself would have entailed the contradiction, with no further hypotheses needed.
[4] Despite the syntactical similarities between the Russell set (in either variant) and the Cantor diagonal set, Alonzo Church emphasized that Russell's paradox is independent of considerations of cardinality and its underlying notions like one-to-one correspondence.
[5] Cantor gave essentially this proof in a paper published in 1891 "Über eine elementare Frage der Mannigfaltigkeitslehre",[6] where the diagonal argument for the uncountability of the reals also first appears (he had earlier proved the uncountability of the reals by other methods).
Ernst Zermelo has a theorem (which he calls "Cantor's Theorem") that is identical to the form above in the paper that became the foundation of modern set theory ("Untersuchungen über die Grundlagen der Mengenlehre I"), published in 1908.
