FOM: Cantor'sTheorem:LogicalFormIssues

[Robert Tragesser]

Robert Tragesser was egregiously
sloppy about the logical forms of
Cantor's Theorem, and therefore muddy
about the issue of constructive proof.
This posting attempts to correct matters.

M, a set
P[M], the set of all subsets of M.

Cantor's'Cantor's Theorem':
  Given a set M, the power of M is less than
the power of P[M].

Proposed closest (partial) logical analysis:

[CCT] (X)(EJ)(EK)[(J is the power of X) & ( K is
       the power of P[X]) & J<K]

This is likely what Tragesser had in mind.-It
would seem that a constructive proof of [CCT]
should provide a determinate procedure, given x,
finding the powers of X and P[X}, or, assuming,
as would be typical, the power of X is given,
for determining the power of P[X] from X and the
given power of X.

By contrast, there is a less loaded form of Cantor's
Theorem some variation on which seems to be what
fomers have had in mind, [LessLoadedCantor'sThm],

[LLCT] (X)(J)(K)[ if (J is a cardinal of X &
K is a cardinal of K), then K < J ]

What should a constructive proof of [LLCT]
provide over what a nonconstructive proof would provide?
This is hard to answer; but it in any case would not
be required to provide the definite cardinal; even
the requirement/fact that the cardinal of a set is
unique is not implicit in the statement oof the theorem.
N.B.: But it seems that it would be required that the
proofs of all the lemmas brought to bear on the proof
of [CT] be constructive proofs.

One finds generally two sorts of proofs of [CT]. ('[CT]'
for 'Cantor's Theorem', without regard to the formulation,
whether [LLCT] or [CCT]:

One is a proof via the general lemma below,
  where X is a set,
        P[X} is the set of all subsets of X,
        SbP[X} is any subset of P[X} (but it need not
be a proper subset, it could be that SbP[X] = P[X} ):

[GLmma] (X){ if there exists a 1-1 onto mapping m between
         SpP[X] & X, then there exists a subset u of X
         that is not an element of SbP[X] ].

In a proof going through [GLemma], the final steps
specialize the Lemma to SbP[X] = P[X], observing that
[GLmma] entails that SbP[X] is a proper subset of
P[X], but by hypothesis it is = P[X], concluding that
there can not exist a 1-1 onto mapping between X and
P[X}. An appeal to trichotomy yields the conclusion
to the theorem, given that not-( card P[X] < card X ).

[GLmma] is proved via a general "diagonal" construction.

The alternative, simpler proof of [CT], replaces the
general lemma by a special construction - it
assumes outright that SbP[X] is P[X], and applies
the diagonal construction used in the proof of the
general lemma to this case alone.

It is in the former case that the issue of a
constructive proof for [GLmma] arises. In that case,
the proof for [CT} would not be constructive
if the proof of [GLmma] is nonconstructive.

WHAT DO WE REQUIRE OF FROM A CONSTRUCTIVE PROOF
OF [GLmma]?  Some sort of rather determinate and
informative procedure by which to obtain a
subset u of X not an element of SbP[X], given:
X, the 1-1 onto mapping m, and SbP[X].

In order to insightfully and compellingly
spell out the details of what we
require of a constructive proof,
I think that we need an informal
and core notion "constuctive" (or "inutionistic",
though I think these have essentially
different provenances].  Such a proof must be
not only "locally" constructive, but constructive
all the way down to, and including, the axioms
and rules of logic.  They (axioms and rules
of logic) must be shown to be constructively meaningful.
Maybe this is problematic for IZF?

N.B., the proof of [CT} via the general lemma, though
less economical, is preferable to the logically
simpler proof, because it gives better understanding
(and is therefore more in the spirit of intuitionistic
interests).

Robert Tragesser
Westbrook, Conn 06498
rtragesser at hotmail.com
860 399 6305







_________________________________________________________________
Get your FREE download of MSN Explorer at http://explorer.msn.com