categorical formulations of Replacement

categorical formulations of Replacement

[Paul Taylor]

Dear Thomas,

I'm glad that we've now started to talk a common language about
Replacement, and am hopeful that it will be possible to come to
some agreement, but I think that we are still some way off doing so.

Since you have changed the Subject: line several times, I would like
first to give some help to anyone who might be trying to follow this
discussion from an archive in the future, by listing the Subject:
lines of recent postings.  Of course, they have "categories:" and
"re:" added to them.

  Categorial foundations
  categorical formulations of Replacement
  Heyting algebras and Wikipedia
  I was partly wrong
  internal versus external
  question to Colin about uniqueness in his Replacement axiom
  replacement and iterated powersets
  replacement and the gluing construction
  replacing set theory
  the axiom scheme of replacement in category theory
  trying to answer some of Paul's questions

When I was trying to understand replacement, ten years ago and more,
I found, both from my own experience and in looking that the work of
others, that it is easy to fall into one of two traps:

(1) lack of rigour;  using the words "external" or "meta-language" may
indicate this;

(2) lack of force;  using the word "definable" may indicate this.

You can talk rigorously about external or meta- things if you first set
up a two-level formal system.  Examples of such systems include
(1) first order logic and set theory expressed within it;
(2) first order logic and category theory expressed within it;
(3) a category with an internal category;
(4) a fibred category containing a universe in the sense that
     you and I discussed in the 1980s;
(5) a pretopos or arithmetic universe with a class of small maps
     (algebraic set theory).

A large part of the explanation for ideological conflicts between
mathematicians is that they work in different OUTER systems.  If
they can agree on the outer system, they have an arena in which to
compare their INNER systems.  Reading between the lines of your
posting suggests that you are not completely confident yourself
of the rigour of your own account.

One of the uses of a two-level system is to discuss logical questions
such a consistency.  For example, Godel's theorem is about truth and
provability, which may be seen as facts about the outer and inner
systems
respectively.  Andre' Joyal set this up in category theory by looking
at the free arithmetic universe inside an arithmetic universe.

The axiom-scheme of replacement seems to be about making the inner world
agree with part of the outer one.

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.

It would help if you were all to give more "turorial" explanations of
these things, and precise internal references to relevant papers and
books, because these are often lengthy and largely devoted to simpler
categorical structure than replacement.

We agree, I believe, that fibred methods are they way that we can
express
in category theory ideas that the set theorists encode as sets of sets.
Thus a display map  p:X-->N  captures the same idea as
   { {{x, {x, n}}  |  x in X & p(x)=n } | n in N },
or whatever hieroglyphics the set theorists would use.

Similarly,  the idea of a functor from a small category to a large one,
say  F:CC-->Set,  can be captured as a discrete fibration   p:FF-->CC.

In order to have any chance of fitting the axiom scheme of replacement
into our skulls,  we have to take the technology (fibred category
theory,
for example) as read,  even though it is rather difficult and
complicated
itself.   The problem is that most accounts add replacement as a brief
footnote to a lengthy treatment of more basic topics.   My book is
guilty of this, and so, with all due respect, are you, I believe.

With regard to the example of the iterated powerset,  the statement of
yours that I quoted above claims to express this,  but I do not
understand the language.  I would like you to translate it into the
usual language of category theory, ie functors, pullbacks etc.

I suspect that what you will come up with is the same as in my posting
about this on Sunday afternoon.   I accept that I have taken the
technology of fibred category theory off the shelf to do this, but

*********************************************************************
*  I believe that I made a significant original contribution        *
*  (in my book) by formulating the equation X_{n+1} = P(X_n) as     *
*  a pullback along the structure map of a well founded coalegbra.  *
*********************************************************************

The example of the gluing construction illustrates the difficulty caused
by treating replacment as a footnote to a more elementary theory.
There is, as you say, no foundational difficulty in constructing the
comma category arising from a functor  U:AA-->SS.   Although I have
copied most of what I have to say about replacement in Section 9.6
of the book in these postings, I am not going to do so for my account
of the gluing construction, as it is mathematically too complicated
to do so. You will have to get the book itself and read section 7.7.

The foundational issue about this construction is its application to
consistency issues of various theories.   In these,  SS  is a "semantic"
model of the theory in question, maybe the universe "Set" in which we
claim to live,  and  AA  is the "syntactic" or "term" model.

We have to be careful about calling AA the "free" or "initial" model,
as this is exactly the foundational point.

The gluing construction is the comma category (SS,U) whose objects are
SS-maps of the form  X-->U(Gamma),  where Gamma is an object of AA and
X one of SS.   I use the letter Gamma because it is typically a context
of the theory under study.   One can show that  (U,SS)  typically
inherits the structure of this theory, and pi_1:(SS,U)-->AA preserves
it.

Since  (U,SS)  is a model of the theory,  whilst  AA is the term model,
there ought to be an interpretation functor   [[-]]:AA-->(U,SS).
We have no difficulty in saying what such a functor would be in
substance, since we can express it as a fibration  EE-->AA of small
categories.   However, this illustates the difficulty with the
word "definable" - if you already had this fibration then there
would be nothing left for Replacment to do.

The problem is whether the functor or fibration exists.   Now, as AA
is the term model, we can use recursion over its well founded system
of types, terms and proofs. For example,  if we already know  [[Gamma]]
and [[Delta]],  we can form the interpretation of the arrow type
Gamma -> Delta as the exponential
    [[ Gamma -> Delta ]]   =   [[Delta]] ^ [[Gamma]].

However, this is not a valid form of recursion, since recursion defines
new TERMS of pre-existing types.   We want to form new TYPES.  This
involves the axiom scheme of replacement.

******************************************************************
*  Again, I claim an original contribution in my book in         *
*  recognising that this application of the gluing construction  *
*  to logic requires the axiom scheme of replacement.            *
******************************************************************

Notice that replacement is not only a scheme indexed by types,  it is
also parametric in the theory under study:   each theory has its own
replacement scheme.   If the original theory was algebra,  we can
characterise the corresponding notion of replacement as what are
variously known as dependent products, partial products or W-types.

But also, the operation of formulating replacement turns one theory into
another, so it can be iterated.  Ten years ago, I briefly believed that
this leads to inconsistency in ZF.   I suspect that this is a necessary
though not sufficient "rite of passage" - ie that, only after
temporarily
believing that it is  inconsistent, can one claim to understand what
the Axiom of Replacement says.

Paul Taylor

Re: categorical formulations of Replacement

[Colin McLarty]

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

Re: categorical formulations of Replacement

[Michael Shulman]

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

Re: categorical formulations of Replacement

[wlawvere]

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

Re: categorical formulations of Replacement

[Colin McLarty]

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

categorical formulations of Replacement

[Thomas Streicher]

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