From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/102 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations Date: Sat, 21 Feb 2009 09:18:29 -0800 Message-ID: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1235285574 6139 80.91.229.12 (22 Feb 2009 06:52:54 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 22 Feb 2009 06:52:54 +0000 (UTC) To: categories@mta.ca Original-X-From: categories@mta.ca Sun Feb 22 07:54:09 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1Lb8Dx-0003d7-EK for gsmc-categories@m.gmane.org; Sun, 22 Feb 2009 07:54:01 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lb7jP-00062P-Nn for categories-list@mta.ca; Sun, 22 Feb 2009 02:22:27 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:102 Archived-At: Toby Kenney wrote: > Vaughan Pratt wrote in part: >> I could well imagine 1 and 2 turning out to be isomorphic, but I feel I >> would get a lot from seeing the proof of whichever way that goes. Thanks very much, Toby. I didn't (and still don't) have any intuition into what objects and morphisms are present in the free topos with NNO, but your proof will help me fill in the gaps in this neighborhood of it. On the one hand there are lots of objects one can talk about in language analogous to that characterizing the NNO, on the other there are also lots of morphisms one can talk about that identify those objects (up to isomorphism), and I'm still at the very early stage of learning how to walk along that ridge line without falling off one side or the other. Joyal and Moerdijk, Algebraic Set Theory, show how to construct sup-semilattices with sups up to a specified size S. Obviously not every topos with NNO supports every S, but presumably S = K (Kuratowski-finite) is always present. Your proof if correct shows that ts = t is too strong. What if I relax it to ts <= t and proceed as in J&M to construct the initial such object? Can you still construct your isomorphism, or do we end up with a weaker relationship? If the latter then we should have t(0) >= t(s(0)) = t(1) >= t(2) >= ... >= x for any natural number x. Obviously t(0) is minimal among all terms having at least one t, which should make t(0) the ordinal w. The one disconcerting thing here is that initiality has made t(0) an infinite sup even though I assumed only finite sups. I don't know whether this means that the methods of J&M can't construct this initial algebra, or that in every topos with NNO one can construct the requisite sup-semilattices with countable sups. I suppose it must be the latter. (I'm a complete novice here, as I've said before, so I hope people will be patient with my appalling ignorance of topos-theoretic techniques.) Vaughan