From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4332 Path: news.gmane.org!not-for-mail From: "Michael Shulman" Newsgroups: gmane.science.mathematics.categories Subject: Re: internal versus external Date: Mon, 17 Mar 2008 20:14:58 -0500 Message-ID: References: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019876 12794 80.91.229.2 (29 Apr 2009 15:44:36 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:44:36 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Tue Mar 18 08:48:03 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 18 Mar 2008 08:48:03 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JbaCW-00059T-45 for categories-list@mta.ca; Tue, 18 Mar 2008 08:41:52 -0300 Content-Disposition: inline Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 96 Original-Lines: 27 Xref: news.gmane.org gmane.science.mathematics.categories:4332 Archived-At: On Sat, Mar 15, 2008 at 11:31 AM, Thomas Streicher wrote: > It might be the case that > any "syntactically definable" external family indexed by EE(1,X) arises from > some internal family a : A -> X though I don't see how to prove it. I thought this was exactly what Colin's version of the replacement axiom says. > The reason why I doubt that models of ETCS and bZ are equivalent is that when > going from a model of ECTS to a model of bZ is that one has to restrict to the > well-founded part. At least that's what I recollect from MacLane and Moerdijk's > exposition in their book. But I am ready to believe that adding wellfoundedness > axioms to ETCS can remedy this situation. Osius uses a different construction than M&M: instead of explicitly building "membership trees" he uses objects equipped with a transitive well-founded relation to represent transitive sets, and subobjects of them to represent arbitrary sets. In general you do have to add a "transitive representation" axiom to ensure that every object of the topos can be reconstructed from the resulting model of bZ---but this is unnecessary if you also assume choice, since then every object can be well-ordered and thus admits a transitive well-founded relation. Mike