Re: categorical formulations of Replacement

[<wlawvere@buffalo.edu>]

The uncountability argument mentioned by
Thomas does not apply because Colin's
Replacement axiom does not say that
"all" external families are representable,
only those definable by formulas.

Of course the statement is relatively
simple only when 1 separates, but that
is the case where much of the interest 
in such axioms has concentrated:
categories of pure Cantorian cardinals.
Speculating about whether such principles
yield anything for the more cohesive
sets encountered in geometry and analysis,
it develops that, although specifying the
internal families is rather easy, explaining
which formulas define the appropriate
external families is not because of the 
need to include functorality, sheaf 
condition,etc.

Concerning the 70s work of Cole,Osius,etal,
they certainly constructed in lectures an
equivalence between the categories of models
of bZ and aETCS. Was it not published ? 
(I don't recall any example showing 
that the augmentation a was actually needed.)

The statement that Replacement
is weak seems to follow from using that word
to refer to classes derived from an already 
representable V, rather than the traditional
meaning used by Colin, referring to arbitrary
formulas.

Bill


On Thu Mar 13 22:34 , Thomas Streicher  sent:

>The Replacemnt 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. 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.
>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.
>
>I think that the more interesting question is what is a model of intuitionistic
>set theoy which cannot be well-pointed. For this purpose it is INDISPENSIBLE
>to have in our category an object U of all sets.
>This was first recognized and formulated by Christian Maurer in his paper
>"Universes in Topoi" which appeared in the SLNM volume "Model theory and topoi"
>(ed. Lawvere, Maurer, Wraith). Maurer was working in a topos and postulated an
>object U (a "universe") of this topos with ext : U >-> P(U) satisfying a few
>axioms which ensure that U is a model for IZF (without saying so).
>In particular, he has a clear formulation of the axiom of replacement, namely
>
>    (\forall a : U) (\forall f : U^{ext(a)}) (\exists b : U)
>
>        (\forall y : U) (y \in ext(b)  (\exists x \in ext(a)) y = f(x))
>
>albeit in a somewhat less readable since he avoids the internal language
>of the topos.
>
>This point of view was taken up later in the Algebraic Set Theory (AST) of
>Joyal and Moerdijk whose work concentrated on CONTRUCTING (initial) universes
>of this kind. A couple of years later Alex Simpson in his LiCS'99 paper took
>up Maurer's early insight (at least he refers to Maurer's paper) but weakened
>the ambient category to be a model for first order logic (as set theorists do).
>The main new ingredient of AST (and Alex's paper) is the assumption of a class
>of small maps giving (cum grano salis) a notion of "size" (like B'enabou's
>calibrations but satisfying much stronger axioms) together with a notion of
>small powerset functor P_s (depending on the class of small maps). A universe
>is then defined as a(n initial) fixpoint U of P_s which, of course, can't be
>small itself.
>
>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. See the paper by Awodey, Butz, Simpson
>and me which appeared in last year's Bull.Symb.Logic (see also
>http://homepages.inf.ed.ac.uk/als/Research/Sources/set-models-announce.pdf)
>where we discuss this in more detail. The point is that around every topos
>EE one can build a category of classes whose small "set" part is equivalent
>to EE. The corresponding class theory BIST is thus conservative over topos
>logic (with nno).
>
>Later on Awodey and his students have also studied the much weaker "predicative"
>case where replacement still holds. See also Aczel and Rathjen's work on CZF
>in this context which is much older than AST dating back to articles by Aczel
>in the late 70ies (and based on previous work by John Myhill).
>
>Thomas Streicher
>
>
>