FOM: Cantor's theorem

[William Tait]

Stuart Shapiro wrote

>I have not yet followed the details of this most interesting thread 
>concerning Cantor's theorem.  It might be noted that Bishop himself 
>mentions and proves Cantor's theorem in *Foundations of constructive 
>analysis*.  As I recall, he gives the usual gloss on the theorem 
>(that the real numbers are not countable), and he gives a standard, 
>diagonal argument.  To be sure, Bishop might have been mistaken 
>about what is and what is not constructively acceptable, but this 
>citation is certainly evidence that the proof is constructively 
>kosher (assuming my memory is correct--I have not had a chance to 
>check this, and I wanted to get this out before the thread goes 
>cold.  Sorry if someone already pointed this out).

Stuart, the discussion up to now has referred to Cantor's 1890 proof 
that there are more 2-valued functions on a set M then there are 
elements of M. (The diagonal argument) You are referring to his 1974 
proof that the real numbers in an interval are not countable (an 
argument by nested intervals). The former argument is constructive, 
as a number of people on the list have affirmed. The latter is 
constructive, as you have noted.

Best regards,

Bill Tait