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