Editing Cantor's theorem (section)

==Proof==
Cantor's argument is elegant and remarkably simple. The complete proof is presented below, with detailed explanations to follow.

{{math theorem|name=Theorem (Cantor)|math_statement=Let <math>f</math> be a map from set <math>A</math> to its power set <math>\mathcal{P}(A)</math>.  Then <math>f : A \to \mathcal{P}(A)</math> is not [[surjective]].  As a consequence, <math>\operatorname{card}(A) < \operatorname{card}(\mathcal{P}(A))</math> holds for any set <math>A</math>.}}
{{math proof| <math> B=\{x \in A \mid x \notin f(x)\}</math> exists via the [[axiom schema of specification]], and <math> B \in \mathcal{P}(A) </math> because <math> B \subseteq A </math>. <br> Assume <math> f </math> is surjective. <br> Then there exists a <math>\xi \in A</math> such that <math>f(\xi)=B</math>. <br> From &nbsp;''for all'' <math>x</math> ''in'' <math>A \ [ x \in B \iff x \notin f(x) ]</math> , we deduce &nbsp;<math>\xi \in B \iff \xi \notin f(\xi) </math> &nbsp;via [[universal instantiation]]. <br> The previous deduction yields a contradiction of the form <math>\varphi \Leftrightarrow \lnot \varphi</math>, since <math>f(\xi)=B</math>. <br> Therefore, <math>f</math> is not surjective, via [[reductio ad absurdum]]. <br> We know [[injective function|injective maps]] from <math>A</math> to <math>\mathcal{P}(A)</math> exist. For example, a function <math>g : A \to \mathcal{P}(A)</math> such that <math>g(x) = \{x\}</math>. <br> Consequently, <math>\operatorname{card}(A) < \operatorname{card}(\mathcal{P}(A))</math>. ∎}}

By definition of cardinality, we have <math>\operatorname{card}(X) < \operatorname{card}(Y)</math> for any two sets <math>X</math> and <math>Y</math> if and only if there is an [[injective function]] but no [[Bijective Function|bijective function]] from <math>X</math> {{nowrap|to <math>Y</math>.}} It suffices to show that there is no surjection from <math>X</math> {{nowrap|to <math>Y</math>}}. This is the heart of Cantor's theorem: there is no surjective function from any set <math>A</math> to its power set. To establish this, it is enough to show that no function <math>f</math> (that maps elements in <math>A</math> to subsets of <math>A</math>) can reach every possible subset, i.e., we just need to demonstrate the existence of a subset of <math>A</math> that is not equal to <math>f(x)</math> for any <math>x \in A</math>. Recalling that each <math>f(x)</math> is a subset of <math>A</math>, such a subset is given by the following construction, sometimes called the [[Cantor's diagonal argument|Cantor diagonal set]] of <math>f</math>:<ref name="Dasgupta2013">{{cite book|author=Abhijit Dasgupta|title=Set Theory: With an Introduction to Real Point Sets|year=2013|publisher=[[Springer Science & Business Media]]|isbn=978-1-4614-8854-5|pages=362–363}}</ref><ref name="Paulson1992">{{cite book|author=Lawrence Paulson|title=Set Theory as a Computational Logic |url=https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-271.pdf|year=1992|publisher=University of Cambridge Computer Laboratory|page=14}}</ref>

:<math>B=\{x\in A \mid x\not\in f(x)\}.</math>

This means, by definition, that for all <math>x\in A</math>, <math>x\in B</math> if and only if <math>x\notin f(x)</math>. For all <math>x</math> the sets <math>B</math> and <math>f(x)</math> cannot be equal because <math>B</math> was constructed from elements of <math>A</math> whose [[Image (mathematics)|images]] under <math>f</math> did not include themselves. For all <math>x\in A</math> either <math>x\in f(x)</math> or <math>x\notin f(x)</math>. If <math>x\in f(x)</math> then <math>f(x)</math> cannot equal <math>B</math> because <math>x\in f(x)</math> by assumption and <math>x\notin B</math> by definition. If <math>x\notin f(x)</math> then <math>f(x)</math> cannot equal <math>B</math> because <math>x\notin f(x)</math> by assumption and <math>x\in B</math> by the definition of <math>B</math>.

Equivalently, and slightly more formally, we have just proved that the existence of <math>\xi \in A</math> such that <math>f(\xi )=B</math> implies the following [[contradiction]]:

:<math>\begin{aligned}
\xi\in B &\iff \xi\notin f(\xi) && \text{(by definition of }B\text{)}; \\
\xi \in B &\iff \xi \in f(\xi) && \text{(by assumption that }f(\xi)=B\text{)}. \\

\end{aligned}</math>

Therefore, by [[reductio ad absurdum]], the assumption must be false.<ref name="Priest2002"/> Thus there is no <math>\xi \in A</math> such that <math>f(\xi )=B</math> ; in other words, <math>B</math> is not in the image of <math>f</math> and <math>f</math> does not map onto every element of the power set of <math>A</math>, i.e., <math>f</math> is not surjective.

Finally, to complete the proof, we need to exhibit an injective function from <math>A</math> to its power set.  Finding such a function is trivial: just map <math>x</math> to the singleton set <math>\{x\}</math>.  The argument is now complete, and we have established the strict inequality for any set <math>A</math> that <math>\operatorname{card}(A) < \operatorname{card}(\mathcal{P}(A))</math>.

Another way to think of the proof is that <math>B</math>, empty or non-empty, is always in the power set of <math>A</math>. For <math>f</math> to be [[Surjective function|onto]], some element of <math>A</math> must map to <math>B</math>. But that leads to a contradiction: no element of <math>B</math> can map to <math>B</math> because that would contradict the criterion of membership in <math>B</math>, thus the element mapping to <math>B</math> must not be an element of <math>B</math> meaning that it satisfies the criterion for membership in <math>B</math>, another contradiction. So the assumption that an element of <math>A</math> maps to <math>B</math> must be false; and <math>f</math> cannot be onto.

Because of the double occurrence of <math>x</math> in the expression "<math>x\in f(x)</math>", this is a [[Cantor's diagonal argument|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 <math>x</math> from <math>A=\{x_1 ,x_2 , \ldots \}</math>, in this order. <math>A</math> is assumed to admit a [[Total order|linear order]] so that such table can be constructed.
# each column of the table is labelled by a unique <math>y</math> from the [[power set]] of <math>A</math>; the columns are ordered by the argument to <math>f</math>, i.e. the column labels are <math>f(x_1),f(x_2)</math>, ..., in this order.
# the intersection of each row <math>x</math> and column <math>y</math> records a true/false bit whether <math>x\in y</math>.
Given the order chosen for the row and column labels, the main diagonal <math>D</math> of this table thus records whether  <math>x\in f(x)</math> for each <math>x\in A</math>. One such table will be the following:
<math display="block">\begin{array}{cccccc}
& f(x_1) & f(x_2) & f(x_3) & f(x_4) & \cdots \\
\hline
x_1 & {\color{red} T} & T & F & T & \cdots \\
x_2 & T & {\color{red} F} & F & F & \cdots \\
x_3 & F & F & {\color{red} T} & T & \cdots \\
x_4 & F & T & T & {\color{red} T} & \cdots \\
\vdots & \vdots & \vdots & \vdots & \vdots & \ddots
\end{array}</math>
The set <math>B</math> constructed in the previous paragraphs coincides with the row labels for the subset of entries on this main diagonal <math>D</math> (which in above example, coloured red) where the table records that <math>x\in f(x)</math> is false.<ref name="Priest2002">{{cite book|author=Graham Priest|title=Beyond the Limits of Thought|year=2002|publisher=Oxford University Press|isbn=978-0-19-925405-7|pages=118–119}}<!--note that the page numbers differ between the OUP and CUP editions of Priest's book!--></ref> Each row records the values of the [[indicator function]] of the set corresponding to the column. The indicator function of <math>B</math> coincides with the [[logical negation|logically negated]] (swap "true" and "false") entries of the main diagonal. Thus the indicator function of <math>B</math> does not agree with any column in at least one entry. Consequently, no column represents <math>B</math>.

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 (theorem prover)|Otter]] could not do it, whereas [[Isabelle (proof assistant)|Isabelle]] could, albeit with a certain amount of direction in terms of tactics that might perhaps be considered cheating.<ref name="Paulson1992"/>