From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1595 Path: news.gmane.org!not-for-mail From: Alex Simpson Newsgroups: gmane.science.mathematics.categories Subject: Re: Reality check Date: Fri, 04 Aug 2000 12:16:52 +0100 Message-ID: <200008041116.MAA28030@cuillin.dcs.ed.ac.uk> References: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1241017955 31999 80.91.229.2 (29 Apr 2009 15:12:35 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:12:35 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Fri Aug 4 12:50:40 2000 -0300 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA02692 for categories-list; Fri, 4 Aug 2000 12:50:36 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: exmh version 2.1.1 CVS 2000/03/22 In-Reply-To: Message from Martin Escardo of "Fri, 04 Aug 2000 11:23:36 BST." <14730.39336.321672.460059@mosstowie.dcs.st-and.ac.uk> Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 7 Original-Lines: 42 Xref: news.gmane.org gmane.science.mathematics.categories:1595 Archived-At: 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