FOM: Cantor'sTheorem & Paradoxes & Continuum Hypothesis

[Marcin Mostowski]

Of course you are writting about two Cantor theorems

1. for each set A, A /= P(A) - they are not equicardinal.

2. for each set A, card(A) < card(P(A)).

Theorem 1, as Andrej Bauer has observed can be easily proved constructively.
The scheme of the proof is the same as those of classical proofs of
irrationallity of 2, 3, 5, and so on. We prove "not p" just by assuming p
and justifying the contradiction on the basis of our assumption. Then we
prove "if p then contradiction", which is a good translation for
intuitionisic negation. Recall that theorem 1 is a negative statement.

On the other hand theorem 2 is a positive statement, proof of which (without
the Axiom of Choice) would essentially depend on our definition of
card(..) - "the cardinal number of". For instance if you have the following

Lemma for each sets A, B: card(A) < card(B) iff there is an injection f:
A -> B, but there is no such bijection.

then you can get from the proof of theorwem 2 as from theorem 1 as follows:
define f(x) = {x}, it is an injection A -> P(A), but by theorem 1 there is
no such bijection.

It seems to me that your dubts are of slightly different nature. The first
proof like that of theorem 1 was invented  by Pitagoreans for irrationality
of 2, more precisely incommessurability of the side and the diagonal of a
square. It was probably  the first proof in mathematics of something what
cannot be oserved or mesured, in this sense it was a new intelectual tool
for penetrating our reallity. OK, advise your students to think in this way.

Marcin Mostowski