Content deleted Content added
Paradoctor (talk | contribs) →top: irrelevant detail here, that's what the link is for |
→When A is countably infinite: Added "Indeed," to the beginning of a sentence so that the sentence does not start with a mathematical symbol, as is often accepted as bad style. I think this does not change the meaning of the sentence |
||
| (5 intermediate revisions by 5 users not shown) | |||
Line 38:
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
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>. 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> 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 column 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>.▼
# 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>
▲
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"/>
Line 49 ⟶ 63:
:<math>\mathcal{P}(\mathbb{N})=\{\varnothing,\{1, 2\}, \{1, 2, 3\}, \{4\}, \{1, 5\}, \{3, 4, 6\}, \{2, 4, 6,\dots\},\dots\}.</math>
Indeed, <math>\mathcal{P}(\mathbb{N})</math> contains infinite subsets of <math>\mathbb{N}</math>, e.g. the set of all positive even numbers <math>\{2, 4, 6,\ldots\}=\{2k:k\in \mathbb{N}\}</math>, along with the [[empty set]] <math>\varnothing</math>.
Now that we have an idea of what the elements of <math>\mathcal{P}(\mathbb{N})</math> are, let us attempt to pair off each [[element (math)|element]] of <math>\mathbb{N}</math> with each element of <math>\mathcal{P}(\mathbb{N})</math> to show that these infinite sets are equinumerous. In other words, we will attempt to pair off each element of <math>\mathbb{N}</math> with an element from the infinite set <math>\mathcal{P}(\mathbb{N})</math>, so that no element from either infinite set remains unpaired. Such an attempt to pair elements would look like this:
| |||