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 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 need to include functorality, sheaf 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 ? (I don't recall any example showing 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 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 proves 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 intuitionistic set theoy which cannot be well-pointed. For this purpose it is INDISPENSIBLE 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 topoi" (ed. Lawvere, Maurer, Wraith). Maurer was working in a topos and postulated an object U (a "universe") of this topos with ext : U >-> P(U) satisfying a few 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, namely

(\forall a : U) (\forall f : U^{ext(a)}) (\exists b : U)

(\forall y : U) (y \in ext(b) (\exists x \in ext(a)) y = 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) universes of this kind. A couple of years later Alex Simpson in his LiCS'99 paper took up Maurer's early insight (at least he refers to Maurer's paper) but weakened 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 class 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 universe 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 only 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 "predicative" case where replacement still holds. See also Aczel and Rathjen's work on CZF in this context which is much older than AST dating back to articles by Aczel in the late 70ies (and based on previous work by John Myhill).

Thomas Streicher

Dear Thomas, I'm glad that we've now started to talk a common language about Replacement, and am hopeful that it will be possible to come to some agreement, but I think that we are still some way off doing so. Since you have changed the Subject: line several times, I would like first to give some help to anyone who might be trying to follow this discussion from an archive in the future, by listing the Subject: lines of recent postings. Of course, they have "categories:" and "re:" added to them. Categorial foundations categorical formulations of Replacement Heyting algebras and Wikipedia I was partly wrong internal versus external question to Colin about uniqueness in his Replacement axiom replacement and iterated powersets replacement and the gluing construction replacing set theory the axiom scheme of replacement in category theory trying to answer some of Paul's questions When I was trying to understand replacement, ten years ago and more, I found, both from my own experience and in looking that the work of others, that it is easy to fall into one of two traps: (1) lack of rigour; using the words "external" or "meta-language" may indicate this; (2) lack of force; using the word "definable" may indicate this. You can talk rigorously about external or meta- things if you first set up a two-level formal system. Examples of such systems include (1) first order logic and set theory expressed within it; (2) first order logic and category theory expressed within it; (3) a category with an internal category; (4) a fibred category containing a universe in the sense that you and I discussed in the 1980s; (5) a pretopos or arithmetic universe with a class of small maps (algebraic set theory). A large part of the explanation for ideological conflicts between mathematicians is that they work in different OUTER systems. If they can agree on the outer system, they have an arena in which to compare their INNER systems. Reading between the lines of your posting suggests that you are not completely confident yourself of the rigour of your own account. One of the uses of a two-level system is to discuss logical questions such a consistency. For example, Godel's theorem is about truth and provability, which may be seen as facts about the outer and inner systems respectively. Andre' Joyal set this up in category theory by looking at the free arithmetic universe inside an arithmetic universe. The axiom-scheme of replacement seems to be about making the inner world agree with part of the outer one. I really do not have much idea of what you mean by statements like \forall n:N \exists i : X_{n+1} -> P(X_n) Iso(i). Nor do I understand similar statements to this in either "An elementary theory of the category of sets (extended version)" or "Exploring categorical structuralism" by Bill Lawvere and Colin McLarty respectively. It would help if you were all to give more "turorial" explanations of these things, and precise internal references to relevant papers and books, because these are often lengthy and largely devoted to simpler categorical structure than replacement. We agree, I believe, that fibred methods are they way that we can express in category theory ideas that the set theorists encode as sets of sets. Thus a display map p:X-->N captures the same idea as { {{x, {x, n}} | x in X & p(x)=n } | n in N }, or whatever hieroglyphics the set theorists would use. Similarly, the idea of a functor from a small category to a large one, say F:CC-->Set, can be captured as a discrete fibration p:FF-->CC. In order to have any chance of fitting the axiom scheme of replacement into our skulls, we have to take the technology (fibred category theory, for example) as read, even though it is rather difficult and complicated itself. The problem is that most accounts add replacement as a brief footnote to a lengthy treatment of more basic topics. My book is guilty of this, and so, with all due respect, are you, I believe. With regard to the example of the iterated powerset, the statement of yours that I quoted above claims to express this, but I do not understand the language. I would like you to translate it into the usual language of category theory, ie functors, pullbacks etc. I suspect that what you will come up with is the same as in my posting about this on Sunday afternoon. I accept that I have taken the technology of fibred category theory off the shelf to do this, but ********************************************************************* * I believe that I made a significant original contribution * * (in my book) by formulating the equation X_{n+1} = P(X_n) as * * a pullback along the structure map of a well founded coalegbra. * ********************************************************************* The example of the gluing construction illustrates the difficulty caused by treating replacment as a footnote to a more elementary theory. There is, as you say, no foundational difficulty in constructing the comma category arising from a functor U:AA-->SS. Although I have copied most of what I have to say about replacement in Section 9.6 of the book in these postings, I am not going to do so for my account of the gluing construction, as it is mathematically too complicated to do so. You will have to get the book itself and read section 7.7. The foundational issue about this construction is its application to consistency issues of various theories. In these, SS is a "semantic" model of the theory in question, maybe the universe "Set" in which we claim to live, and AA is the "syntactic" or "term" model. We have to be careful about calling AA the "free" or "initial" model, as this is exactly the foundational point. The gluing construction is the comma category (SS,U) whose objects are SS-maps of the form X-->U(Gamma), where Gamma is an object of AA and X one of SS. I use the letter Gamma because it is typically a context of the theory under study. One can show that (U,SS) typically inherits the structure of this theory, and pi_1:(SS,U)-->AA preserves it. Since (U,SS) is a model of the theory, whilst AA is the term model, there ought to be an interpretation functor [[-]]:AA-->(U,SS). We have no difficulty in saying what such a functor would be in substance, since we can express it as a fibration EE-->AA of small categories. However, this illustates the difficulty with the word "definable" - if you already had this fibration then there would be nothing left for Replacment to do. The problem is whether the functor or fibration exists. Now, as AA is the term model, we can use recursion over its well founded system of types, terms and proofs. For example, if we already know [[Gamma]] and [[Delta]], we can form the interpretation of the arrow type Gamma -> Delta as the exponential [[ Gamma -> Delta ]] = [[Delta]] ^ [[Gamma]]. However, this is not a valid form of recursion, since recursion defines new TERMS of pre-existing types. We want to form new TYPES. This involves the axiom scheme of replacement. ****************************************************************** * Again, I claim an original contribution in my book in * * recognising that this application of the gluing construction * * to logic requires the axiom scheme of replacement. * ****************************************************************** Notice that replacement is not only a scheme indexed by types, it is also parametric in the theory under study: each theory has its own replacement scheme. If the original theory was algebra, we can characterise the corresponding notion of replacement as what are variously known as dependent products, partial products or W-types. But also, the operation of formulating replacement turns one theory into another, so it can be iterated. Ten years ago, I briefly believed that this leads to inconsistency in ZF. I suspect that this is a necessary though not sufficient "rite of passage" - ie that, only after temporarily believing that it is inconsistent, can one claim to understand what the Axiom of Replacement says. Paul Taylor