From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4309 Path: news.gmane.org!not-for-mail From: Colin McLarty Newsgroups: gmane.science.mathematics.categories Subject: Re: categorical formulations of Replacement Date: Fri, 14 Mar 2008 09:52:28 -0400 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019863 12701 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 1JaJ6N-00076a-K0 for categories-list@mta.ca; Fri, 14 Mar 2008 20:14:15 -0300 Content-Language: en X-Accept-Language: en Content-Disposition: inline Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 73 Original-Lines: 62 Xref: news.gmane.org gmane.science.mathematics.categories:4309 Archived-At: Thomas Streicher Friday, March 14, 2008 7:55 am writes > The Replacement 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. What do you mean by an "external family"? Do you mean every family that the mathematician looking at the model from outside it would recognize, or every family defined by a relation in the first-order language? Are you just invoking the Skolem paradox in a categorical setting? What is the axiom scheme "too strong" to do? > A defect of the work from the 70ies (Cole, Osius at.al.) is that it > just proves > equiconsistency of ETCS and bZ (bounded Zermelo set theory) and not an > equivalence between models of ETCS and bZ. Before I can comment I have to ask, do you mean equivalence between models, or between the categories of models? Exactly what is it that you want but feel that work does not prove? Is it just that you prefer to think about a different question? As you put it: > I think that the more interesting question is what is a model of > intuitionistic set theory which cannot be well-pointed. For this > purpose it is INDISPENSIBLE to have in our category an object U > of all sets. You must use these words differently than I do. We normally say every topos is a model of intuitionistic set theory. Many are not well-pointed yet have no object of all sets. Synthetic Differential Geometry (in the full, topos version, not Synthetic Infinitesimal Analysis as in Bell's book) is one of the best-known axiomatic extensions of the elementary topos axioms. It has no well-pointed models yet its usual models have no object U of all sets. > 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 only in presence of unbounded separation. That is in an intuitionistic setting. In classical logic, unbounded replacement implies unbounded separation. The "replacing set theory" thread was about replacing ZFC, which has classical logic. You cite the very nice work you have done Steve Awodey, Carsten Buts, and Alex Simpson. But that work does not aim (just) at axiomatizing the classical universe of sets. There are different questions here. best, Colin