FOM: Cantor's theorem: constructive?

[Fred Richman]

Robert Tragesser wrote:
 
> I would think that a constructive proof
> of this theorem would/should provide a rule
> for determining the cardinality of S(M)
> from that of M???

I don't see the basis for requiring that. Here are a couple of
analogies. 

  (1) The transitivity of inclusion of subsets of a set. It seems to
me that the usual proof is constructive. Would we deny this on the
grounds that we have no rule for determining whether a given element
of the set is in a given subset? Would we say that it is only
"relatively constructive"?

  (2) Nonzero (apart from zero) real numbers are invertible. Didn't
Brouwer recognize that as a constructive theorem? Yet we have no rule
for determining whether a given real number is nonzero.

Now Cantor defined "greater than" for cardinalities of sets in such a
way that this proof shows that the cardinality of the power set of M
is greater than the cardinality of M. Is the objection that his
definition is nonconstructive? Wouldn't it be equally plausible to say
that Brouwer's definition of a nonzero real number is nonconstructive?

--Fred