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