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

[Peter Schuster]

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. 

Peter Schuster

http://www.mathematik.uni-muenchen.de/~pschust




>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
>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 :-)