Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT:
The reason is that you have to know in advance that a binary sequence isn't going to end in an infinite string of 1's; by excluding those sequences, you make the question "Is x < 1/2?" decidable, which is not constructively true of either the Cantor reals or the Dedekind reals.
I had always been somewhat dissatisfied intuitively by the idea of excluding sequences of the form 01111.... It seemed more natural to identify them with those of the form 10000.... However I just assumed that these were equivalent approaches. Your point about making x < 1/2 decidable is a good one. I'm now convinced that it is better to identify than delete. Identification can be accomplished spatially, but perhaps it is more elegant to do so localically, namely by removing the open set that separates the two halves to be glued together. In a T0 space, doing so will identify the points anyway. However in the situation [0,1)[1,2) of my previous messages where there is no point on the left adjacent to the point 1 on the right, identification of points is not an option. The only remaining concern then is whether there's an open set separating [0,1) and [1,2). Finality should eliminate spurious open sets that have no reason to stick around. Vaughan