Re: categorical formulations of Replacement

["Michael Shulman" <shulman@uchicago.edu>]

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