From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4308 Path: news.gmane.org!not-for-mail From: Newsgroups: gmane.science.mathematics.categories Subject: Re: categorical formulations of Replacement Date: Fri, 14 Mar 2008 11:56:19 -0400 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1241019863 12699 80.91.229.2 (29 Apr 2009 15:44:23 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:44:23 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Fri Mar 14 20:25:54 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 14 Mar 2008 20:25:54 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JaJ7z-0007Dn-HE for categories-list@mta.ca; Fri, 14 Mar 2008 20:15:55 -0300 Content-Disposition: inline Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 72 Original-Lines: 124 Xref: news.gmane.org gmane.science.mathematics.categories:4308 Archived-At: The uncountability argument mentioned by Thomas does not apply because Colin's Replacement axiom does not say that "all" external families are representable, only those definable by formulas. Of course the statement is relatively simple only when 1 separates, but that is the case where much of the interest=20 in such axioms has concentrated: categories of pure Cantorian cardinals. Speculating about whether such principles yield anything for the more cohesive sets encountered in geometry and analysis, it develops that, although specifying the internal families is rather easy, explaining which formulas define the appropriate external families is not because of the=20 need to include functorality, sheaf=20 condition,etc. Concerning the 70s work of Cole,Osius,etal, they certainly constructed in lectures an equivalence between the categories of models of bZ and aETCS. Was it not published ?=20 (I don't recall any example showing=20 that the augmentation a was actually needed.) The statement that Replacement is weak seems to follow from using that word to refer to classes derived from an already=20 representable V, rather than the traditional meaning used by Colin, referring to arbitrary formulas. Bill On Thu Mar 13 22:34 , Thomas Streicher sent: >The Replacemnt axiom which Colin formulated in his article in Phil.Math. >only works for well-pointed categories. But even in this framework it is >too strong due to its requirement that every external family arises from an >internal one. So it fails for example for the model of ETCS arising from >a countable model of ZFC because there are only countably many internal >families over N whereas there uncountable many external families indexed >by (the global elements of) N. >A defect of the work from the 70ies (Cole, Osius at.al.) is that it just p= roves >equiconsistency of ETCS and bZ (bounded Zermelo set theory) and not an >equivalence between models of ETCS and bZ. > >I think that the more interesting question is what is a model of intuition= istic >set theoy which cannot be well-pointed. For this purpose it is INDISPENSIB= LE >to have in our category an object U of all sets. >This was first recognized and formulated by Christian Maurer in his paper >"Universes in Topoi" which appeared in the SLNM volume "Model theory and t= opoi" >(ed. Lawvere, Maurer, Wraith). Maurer was working in a topos and postulate= d an >object U (a "universe") of this topos with ext : U >-> P(U) satisfying a f= ew >axioms which ensure that U is a model for IZF (without saying so). >In particular, he has a clear formulation of the axiom of replacement, nam= ely > > (\forall a : U) (\forall f : U^{ext(a)}) (\exists b : U) > > (\forall y : U) (y \in ext(b) (\exists x \in ext(a)) y =3D f(x)) > >albeit in a somewhat less readable since he avoids the internal language >of the topos. > >This point of view was taken up later in the Algebraic Set Theory (AST) of >Joyal and Moerdijk whose work concentrated on CONTRUCTING (initial) univer= ses >of this kind. A couple of years later Alex Simpson in his LiCS'99 paper to= ok >up Maurer's early insight (at least he refers to Maurer's paper) but weake= ned >the ambient category to be a model for first order logic (as set theorists= do). >The main new ingredient of AST (and Alex's paper) is the assumption of a c= lass >of small maps giving (cum grano salis) a notion of "size" (like B'enabou's >calibrations but satisfying much stronger axioms) together with a notion of >small powerset functor P_s (depending on the class of small maps). A unive= rse >is then defined as a(n initial) fixpoint U of P_s which, of course, can't = be >small itself. > >A point which seems to have been overlooked in this latest discussion is >that Replacement per set is not very strong. It gets its usual strength on= ly >in presence of unbounded separation. See the paper by Awodey, Butz, Simpson >and me which appeared in last year's Bull.Symb.Logic (see also >http://homepages.inf.ed.ac.uk/als/Research/Sources/set-models-announce.pdf) >where we discuss this in more detail. The point is that around every topos >EE one can build a category of classes whose small "set" part is equivalent >to EE. The corresponding class theory BIST is thus conservative over topos >logic (with nno). > >Later on Awodey and his students have also studied the much weaker "predic= ative" >case where replacement still holds. See also Aczel and Rathjen's work on C= ZF >in this context which is much older than AST dating back to articles by Ac= zel >in the late 70ies (and based on previous work by John Myhill). > >Thomas Streicher > > >