[FOM] Re: Excluded middle & cardinality of the reals

[Andrej Bauer]

>"Michael Carroll" <mcarroll at pobox.com>
>
> So Kelley's proof, that the reals are uncountable, relies on the law of the
> excluded middle's dictate that partial subsets do not exist.  I was
> surprised to see this. Should I not have been?

I would assume the constructive people have answered this question.
Perhaps someone out there knows: is there a known constructive proof
that the set of reals (any kind of reals) is not countable? It is
certainly constructively consistent to assume that the reals form a
_sub_countable set (a subset of a countable set), e.g. in Recursive
Mathematics.

I see how to prove constructively that the reals are not countable
(using countable choice), but before trying to write down the proof,
I'd prefer to hear that I am not reinventing the wheel :-)

Andrej Bauer

Department of Mathematics and Physics
University of Ljubljana
Slovenia
http://andrej.com