FOM: Cantor's theorem

[Stewart Shapiro]

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