As the topic of Replacement versus topos logic (i.e. higher order intuitionistic arithmetic) has come up (again) it might be appropriate to point at a paper of mine (which has been accepted for the proceedings of "From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics" (L.~Crosilla, P.~Schuster, eds.), Oxford University Press, forthcoming) and can be found at www.mathematik.tu-darmstadt.de/~streicher/NOTES/UniTop.ps.gz In this paper I discuss how to extend the notion of toposes in order to capture the relevant part of the set-theoretic Replacement Axiom. I suggest to add so called universes to toposes which allow one to quantify over small sets (the elements of the universe). This notion of universe has been developed (in a predicative setting) by Martin-Loef in the early 70ies and in the 2nd half of the eighties there was quite some activity to give semantics to such universes using categorical notions. Actually, the categorical notion of universe was introduced already in J. B'enabou "Problemes dans les topos" (Louvain-la-Neuve Report, 1973) My conclusion is that most of the uses of replacement are to define (by recursion) families of sets indexed by some index set (e.g. P^n(X) for n \in N) which is impossible in toposes. Alas, in my note it is not settled whether this notion of universe allows one to build models for IZF as in Joyal and Moerdijk's "Algebraic Set Theory" where they use a slightly different notion of universe (see dicussion on p.12 of my note for more details). Of course, I agree that for most mathematics higher order arithmetic suffices (and actually subsystems of 2nd order arithmetic suffice!). In classical mathematics theorems requiring Replacement are typically from Descriptive Set Theory as e.g. Borel Determinacy (BD). The situation is that ZF proves BD but Z (i.e. ZF without replacement) does not. However, for IZF (intuit. set theory) such examples are not known (Set validates BD but the realizability model for IZF does not!). However, there is a very nice example from Computer Science due to Alex Simpson in "Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory" In Annals of Pure and Applied Logic, 130:207-275, 2004 where he shows that relative to the axioms of SDT (Synthetic Domain Theory) IZF proves the existence of solutions of recursive domain equations whereas higher order arithmetic doesn't. (The reason is that for solutions of such recursive domain equations one has to construct by recursion families of domains which are not a priori contained in an already given domain). But for this pleasant example the existence of a universe (hosting all domains) would already be sufficient. But existence of solutions of domain equations cannot be formulated in the language of higher order arithmetic itself. Thus, from this point of view it is still open whether there exist (purely "mathematical") statements expressible in the language of higher order arithmetic (like e.g. Borel determinacy) which can be proved in IZF but not in intuit.(!) higher order arithmetic. I would be most grateful if anyone could tell me such an example! Thomas 23-Mar-2005 21:52:32 -0400,973;000000000000-00000000