Dear all, I have been following the discussion on toposes vs. set theory on the network. The discussion has reminded me of a more ``pragmatic problem'' that a student of mine (B. Reus) had to face when formalising some variant of Synthetic Domain Theory in a very strong impredicative type theory : Calculus of Constructions with Inductive Types, Extensionality for Functions and Axiom of Unique Choice. This is almost topos logic : what is missing is the principle that equivalent propositions are equal but one has the further assumption of a small internal complete universe. Anyway, the ``pragmatic'' problem he had to face when actually working inside the formal system was HOW TO DEAL WITH SUBTYPES. Notice that the notion of subtype is not the object-oriented one from Computer Science but the good old-fashoned one from Logic. I will now explain more explicitely what I mean. If A is a type and P is a predicate on A then in everyday mathematics one does not hesitate to form the type { x : A | P(x) } . This, of course, is no problem in set theory BUT it definitely is a problem in higher order logic (HOL) because in the latter one does not have the possibility of ``subtype formation'' which allows one to turn a predicate into a type. Now it seems to me that topos logic is more expressive than type theory in the sense that it allows subtype formation. When one extends HOL by subtype formation then any subtype { x : A | P(x) } has to be accompanied by an inclusion map iota_A,P : { x : A | P(x) } >---> A (together with some axioms governing its use; actually, the only place where I could find them spelled out in detail is in some lecture notes by Wesley Phoa). The ``pragmatic'' problem now is that when a \in A and P(a) then one is not allowed to state a \in { x : A | P(x) } BUT ONLY iota_A,P(a) \in { x : A | P(x) } . Now when it comes to formalise arguments in HOL augmented by logical subtypes then notation gets really clumsy as one has to mention the subtype inclusions all the time. (Notice that in dependent type theory one can express { x : A | P(x) } as (\Sigma x : A) P(x) and iota_A,P is projection on the first argument (saliently assuming that propositions are ``proof-irrelevant'', i.e. any proposition considered as a type contains at most one element)). Now -- to my opinion the ``pragmatic'' superiority of (naive) set theory over HOL with subtypes is that one may omit all the ``iotas'' and what one writes down is much more concise. So it is precisely this notational convenience which makes naive set theory a better linguistic tool for communicating mathematical constructions and arguments. But notice that this sloppiness of omitting subtype inclusions renders the ``type-checking'' undecidable -- when one would insist on staying in a typed framework because in order to check whether 7653 \in { x : N | P(x) } one has to PROVE P(7653) which actually is a problem when P is not semidecidable, e.g. when P(x) is a Pi-0-1-formula (which e.g. states the consistency of the formal system in use). !! It is precisely this undecidability of type-checking which forces us to stick to an untyped universe despite the fact that in ordinary mathematical arguments one almost never exploits the strong comprehension principles of ZF(C) !! I am always puzzled by the following two slogans (1) Topos Logic corresponds to Set Theory (2) Topos Logic corresponds to Higher Order Logic which can be found in the topos-theoretic literature. It cannot be the case that both slogans are literally true as one can prove the consistency of Higher Order Logic inside Set Theory and therefore Set Theory must be more expressive than Higher Order Logic (unless one renders G"odel's Second Incompleteness Theorem to be wrong). The slogan I would have in mind would be Topos Logic corresponds to Higher Order Logic with Subtypes . Of course, from the point of view of proof-theoretic strength nothing is gained by adding Subtypes to Higher Order Logic (as this way one surely cannot prove more algorithms to terminate). So I can understand the slogan Topos Logic corresponds to Higher Order Logic in the sense that the logics are equiconsistent. I definitely would like to know from the experts in topos theory which of the correspondences (1) or (2) above is the intended one. Please, note that this question is not meant as a provocation but it simply is curiosity about what the acting person thought when slogans (1) and (2) were promoted (beginning of the 70s I presume). Finally, I would like to ask whether the following impression of mine is absolutely misleading : the correspondence between BZF and topos theory given in the book of Mac Lane and Moerdijk is a mere equiconsistency result saying that there is a nontrivial elementary topos iff there is a consistent model of BZF. If I remember correctly there are given 2 constructions : one turning a model of BZF into an elementary topos (easy) and a second more complicated one constructing a model of BZF from an elementary topos. But that does NOT give an EQUIVALENCE bewteen toposes and models of BZF as far as I can see. When I start with a topos E then I get a model M of BZF which in turn gives rise to a topos E_new but, in general, E and E_new will not be equivalent anymore. Right ?? Sorry for that lengthy and maybe shallow remarks but it is really this ``what I always wanted to know but never dared to ask'' sort of question(s) which I now dare to ask as the arena seems to have been opened already for ``fluffy'' questions. Thomas Streicher