On Thu, Mar 13, 2008 at 9:34 PM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
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.
I do not understand what is meant by "external" here. What Colin and Osius's replacement scheme states is that every *definable* family of sets is internal. This is the same as the ZF replacement axiom: every *definable* function defined on a set is a set. Since there are only countably many logical formulas, there are only countably many definable families for them to define, so there is no problem with countable models.
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.
In Osius' paper "Categorical set theory" he does prove exactly this sort of equivalence, by adding a couple weaker extra axioms to ETCS and bZ relating to the existence of transitive closures and collapses. An account can also be found in Johnstone's "Topos Theory", chapter 9. Mike