Re: Reality check

[Alex Simpson <als@dcs.ed.ac.uk>]

Martin writes:

>  > [Discussion about intuitionistic versions of Freyd's construction
>  > deleted.]

So, in response to that aspect:

Peter's motivation was to capture the signed binary interval rather 
than the binary one, a distinction that only exists in an 
intuitionistic setting. For (at least) this reason, his original 
definition was already intuitionistic (indeed his axioms were 
explicitly formulated in an intuitionistically appropriate form). 
The point I was making was that, given that one is already being 
sensitive to intuitionistic formulations, one also needs to be
equally careful about other aspects of the axiomatization (e.g. 
the definition of a suitable category of ordered sets). I was
curious to know which of the (apparently many) possible alternative 
definitions Peter had in mind.

It seems to me eminently plausible that Peter's construction works 
perfectly for the previously discussed intuitionistic linear orderings 
(I agree with Andrej about terminology - I took my terminology 
"pseudo ordering" from Peter Aczel). In fact, I would expect it to give 
the closed interval of Dedekind reals in any elementary topos with nno.
(Peter's proof that one obtains the signed-binary = Cauchy interval does 
indeed appear to use number-number choice.) I think that would be
a very nice result.

Peter, is this the sort of thing you're aiming at?

Alex

-- 
Alex Simpson, LFCS, Division of Informatics, University of Edinburgh
Email: Alex.Simpson@dcs.ed.ac.uk             Tel: +44 (0)131 650 5113
FTP: ftp.dcs.ed.ac.uk/pub/als                Fax: +44 (0)131 667 7209  
URL: http://www.dcs.ed.ac.uk/home/als