[FOM] Re: Excluded middle & cardinality of the reals
Peter.Schuster at mathematik.uni-muenchen.de
Wed Jun 30 06:31:41 EDT 2004
As Andrej expected, there already is a constructive proof that the
reals are not countable, and this is done with countable choice.
The earliest reference I know is Errett Bishop's "Foundations of
Constructive Analysis", but I bet that this was known before.
The proof actually says a little bit more, that for every sequence
of reals there is a real which is bounded away from each member
of the given sequence. So there's no need to reinvent the wheel.
Another question is whether countable choice is really necessary.
>From fom-bounces at cs.nyu.edu Mon Jun 28 22:22:54 2004
>To: fom at cs.nyu.edu
>From: Andrej Bauer <Andrej.Bauer at andrej.com>
>Date: Mon, 28 Jun 2004 09:32:03 +0200
>Subject: [FOM] Re: Excluded middle & cardinality of the reals
>>"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
>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 :-)
More information about the FOM