Re: categorical formulations of Replacement

[Colin McLarty <colin.mclarty@case.edu>]

Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
Friday, March 14, 2008 7:55 am

writes

> The Replacement axiom which Colin formulated in his article in
> Phil.Math.only works for well-pointed categories. But even in this
> framework it is
> too strong due to its requirement that every external family arises
> from an internal one.

What do you mean by an "external family"?  Do you mean every family that
the mathematician looking at the model from outside it would recognize,
or every family defined by a relation in the first-order language?

Are you just invoking the Skolem paradox in a categorical setting?

What is the axiom scheme "too strong" to do?

> 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.

Before I can comment I have to ask, do you mean equivalence between
models, or between the categories of models?  Exactly what is it that
you want but feel that work does not prove?

Is it just that you prefer to think about a different question?  As
you put it:

> I think that the more interesting question is what is a model of
> intuitionistic set theory which cannot be well-pointed. For this
> purpose it is INDISPENSIBLE to have in our category an object U
> of all sets.

You must use these words differently than I do.  We normally say every
topos is a model of intuitionistic set theory.  Many are not
well-pointed yet have no object of all sets.

Synthetic Differential Geometry (in the full, topos version, not
Synthetic Infinitesimal Analysis as in Bell's book) is one of the
best-known axiomatic extensions of the elementary topos axioms.  It has
no well-pointed models yet its usual models have no object U of all sets.

> A point which seems to have been overlooked in this latest
> discussion is
> that Replacement per set is not very strong. It gets its usual
> strength only in presence of unbounded separation.

That is in an intuitionistic setting.  In classical logic, unbounded
replacement implies unbounded separation.  The "replacing set theory"
thread was about replacing ZFC, which has classical logic.

You cite the very nice work you have done Steve Awodey, Carsten Buts,
and Alex Simpson.  But that work does not aim (just) at axiomatizing the
classical universe of sets.  There are different questions here.

best, Colin