From this point of view I think one can hardly insist that HAH is the ultima ratio as it prevents us from proving meaningful statements which can be
I want to take up the discussion on ``toposes vs. sets'' from another point of view. Over the years a few questions have accumulated and I'd be interested in the opinion of the experts. As Bill Lawvere has pointed out in his reply to the original question there are several meanings in which one can understand the relation ``toposes vs. set theory''. One such distinction is static sets vs. variable sets and one can hardly deny that the latter are of enormous importance for understanding modern mathematics from a conceptual point of view. That's probably what most categorists have in mind when they defend categories as superior to traditional set theory. Another argument probably is that the official language of axiomatic set theory is most inconvenient for actual formalisation of mathematics. One knows that in principle one always can eliminate function symbols in favour of relation symbols but that leads to an explosion of length of formulas and ends in something fairly uncomprehensible.Thus, categorists and also quite a few logicians are in favour of formal systems based function application and predication instead of using just one single relation \epsilon besides equality because function application and predication are the basic constitutents of actual mathematical statements and, moreover, appear most naturally from the categorical notion of topos. In the end this amounts to the point of view that HAH (Higher Order Arithmetic), the internal language of the free topos with NNO, is the formal system which is most suitable for formalizing mathematics (if one wants to embark on such an endeavour at all). Well, but there are some reasons why HAH may be considered as non-sufficient at least from a logical point of view. As Zermelo-Fraenkel set theory ZF(C) and, actually, already Zermelo's Set Theory Z(C) prove the consistency of HAH and accordingly they are non-conservative extensions of HAH. Well, one might argue that this lack of conservativity only affects "meta-statements" and not ``real mathematical statements''. Even hard boiled set theorists would admit that "99% of modern mathematics can be formalised in HAH" (such a statement for Zermelo's Z(C) instead of HAH can be found e.g. in Kunen's monograph on set theory). However, there do exists natural mathematical statements which can be formulated in the language of HAH but proved only in ZF though they are fairly different in character from ``meta-statements''. A typical such example is Borel Determinacy (BD) saying that for every Borel set X in Baire space either player or opponent has a winning strategy for the game G_X where in each step each player plays a natural number and in the end (after \omega steps) player has won if and only if the resulting sequence of numbers lies in X. formulated in HAH. Of course, one might still have in mind an open-ended axiomatization of HAH where one adopts an axiom, as e.g. BD, whenever convenient. This seems to be the attitude for example in SDG where one postulates by need axioms ensuring the existence of particular functions such as cos and sin instead of constructing them via some series. It seems to me that such an attitude is absolutely ok as long as one is interested only in appropriate formalism for expressing mathematical facts and not in the strength of axiomatizations. However, if one wants to arrive at a formal system which allows one to derive (in principle) "all current mathematics" then I think one has to accept that HAH is not satisfactory simply because it is too weak. On the other hand it still is the case that traditional syntax of ZF is not very convenient as a formalisation of mathematical practice. Therefore, it might be worthwhile to look for formal systems of a type-theoretic character equiconsistent to ZF(C) and including ZF(C) via translation. Well, such a language is available, namely the so-called "Calculus of Inductive Constructions" an impredicative type theory with an infinite hierarchy of universes. This is described in Werner, Benjamin Sets in types, types in sets. Theoretical aspects of computer software (Sendai, 1997), 530--546, Lecture Notes in Comput. Sci., 1281, Springer, Berlin, 1997. ftp://ftp.inria.fr/INRIA/Projects/coq/Benjamin.Werner/zfc.ps.gz where one also can find (sketches of) proofs of the meta-theoretic properties mentioned above. The reason why systems like the "Calculus of Inductive Constructions" are as strong as ZF(C) is that they allow one to define FAMILIES of TYPES by structural recursion. which is precisely what the set theoretic axiom of replacement is good for. However, type theoretic language does bring this to the point more clearly than the set-theoretic axiom of replacement which is often used in mathematical practice to formulate the image of a function f : A -> B namely as { f(a) | a \in A} which certainly has to be considered as sort of an overkill because this can be formulated in HAH as well. The real strength of the axiom of replacement is used when defining `images of functions without a codomain' as e.g. families of sets indexed by some inductive type (e.g. an ordinal). The very purpose of type-theoretic universes is to provide a codomain for such `functions without codomain'. According to these observations I get the impression that what topos logic is missing is a concept of universe which allows one to define by recursion not only families of objects but also families of types. I want to conclude my remarks with a pointer to a recent paper by Alex Simpson on Solving Domain Equations in Models of Intuitionistic Set Theory (to be found at http://www.dcs.ed.ac.uk/home/als/Research/rde.ps.gz) where in the last paragraph of section 5 (p.12) he gives a counterexample to the claim that in a topos satisfying the usual axioms of SDT (Synthetic Domain Theory) one always can solve domain equations. The reason is that the topos considered there doesn't allow one to construct certain N-indexed families. (This is a style of argument well-known from the usual proofs in set theory showing that Z(C) is weaker than ZF(C)!) I hope that it has got clear from my formulations that I am not at all ``anti-category''. However, I always found it most confusing when in some texts on toposes I read the statement that the logic of toposes coincides with intuitionistic set theory. I think that most classically trained logicians get immediately puzzled by such statements because they know very well that set theory is stronger than type theory and, therefore, feel sort of repelled by such oversimplifying statements. Moreover, during the 90ies there have been developed fascinating categorical accounts of constructive set theory by Joyal, Moerdijk, Simpson, Butz and Palmgren. I think it would be an interesting question to clarify the relation between this account and the one by universes. Thomas Streicher