Re: categorical formulations of Replacement

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

Paul Taylor <pt08@PaulTaylor.EU>
Wednesday, March 19, 2008 8:05 am

Writes

> I really do not have much idea of what you mean by statements like
>       \forall n:N \exists i : X_{n+1} -> P(X_n)  Iso(i).
> Nor do I understand similar statements to this in either
> "An elementary theory of the category of sets (extended version)"
> or "Exploring categorical structuralism"
> by Bill Lawvere and Colin McLarty respectively.


As to replacement in ETCS:  ETCS is formulated in the first order
language (with equality) of category theory.  Take it as a one-sorted
language (arrows) with composition C(g,f;h).  It makes no principled
difference for our purposes but is extremely handy to also assume
constants 1 of set type (axiomatized as terminal) and "true" of function
type (axiomatized as an element of a truth value set) and partially
defined operators for say, pullbacks and the evaluation functions for
function sets.

ZF is formulated in the first order language (with equality) with
set-membership epsilon.  Replacement in ETCS like replacement in ZF is
an axiom scheme positing one axiom for each formula of a certain form in
the first order language of the theory.

ZF-replacement posits one quantified axiom for each formula Rxy with two
free variables (necessarily variables over sets, since that is what ZF
has, and if you like you may allow other variables as parameters).  The
axiom for Rxy says "For any set S, if R relates each element x\in S to a
unique set y then there is a set X whose elements are exactly those sets
y that are R-related to some x\in S."


ETCS posits one quantified axiom for each formula Rfy with f of arrow
type (the axiom will say f has domain 1 so f stands for some element of
a set) and y of set type.  The axiom for Rfy says "For any set S, if R
relates each function f:1-->S to a set y unique up to isomorphism then
there is an S-indexed set of sets X-->S where the fiber over each x is
isomorphic to the related set y."

The apparatus of discrete fibrations applies here and no doubt to good
advantage for serious work.  But very little is needed in stating the axiom
scheme.

Let me say again that my account of replacement is just Bill's from 1965
only cast as replacement rather than reflection since people are far
more familiar with replacement (and using the simplifications to ETCS
that came with elementary topos theory).

Colin