On Tue, 10 Feb 2009, Greg Meredith wrote:
Categorically minded,
Many thanks for an interesting thread! Just out of curiousity, is the Conway construction clearly identified with the Dedekind reals? How does the construction fit into the constructivist debate?
Best wishes,
--greg
The trouble with the Conway construction is not that it's non- constructive, but that it isn't (in any reasonable sense) a construction of the reals. If you stop it at the point when it finally constructs the real numbers 1/3, \sqrt{2}, \pi and so on, then it has also succeeded in constructing lots of non-real numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how do you distinguish the numbers you want from the ones you don't? I did, in both my first Topos Theory book and the Elephant, borrow Conway's recursive definition of multiplication to give a constructively valid definition of multiplication for Dedekind reals. I'm not aware of anyone else who has done that; but it seems to me the only intellectually respectable way to do it. Peter Johnstone