FOM: ZF-based category theory

[Carsten Butz]

This mail is an appendix to my message from January 19, 1998. By
accident, it answers as well the question raised by Victor Makarov
whether or whether not ZFC is sufficient for mathematics. 
  The reason why I put up these things is that on this list there are
many people who are not that well-trained in set-theory. Those who
are can check their intuition and compare it to what I say below.
(The real reason for this posting was to clarify my  statement 
"any Grothendieck topos is an elementary topos".)

(1) ZF is perfectly suited to deal with ordinary mathematics. As
Steve Simpson mentioned, it is possible to develop whatever you want and
might need in ZF, and this includes analysis, algebra, topology, geometry, 
recursion theory, model theory, category theory, et cetera, et cetera,
et cetera (this list is taken from Simpson's mail).

(2) In particular, categories form a very simple mathematical
(2-sorted) structure ("Objects" and "Arrows").
Within ZF, we can form statements like 
  "for all categories( if ... then ??? )"
  "there exists a category with this or that property"
  etc.

(3) Being more precise, the quantifiers above refer to all categories
in a/the ZF-model. Such categories are usually called _small_. 
One way to read then the equivalence of higher order (intuitionistic)
type theories and elementary toposes (like in [Lambek-Scott]) is as
follows: 
  For any (small) type theory there is a (small) elementary topos
which models this type theory. Conversely, from any (small) elementary
topos we can extract a (small) higher order type theory. 

Here type theory refers to a theory in the "classical" sense, i.e.,
formulated in a language with set-many function and relation symbols,
and as well set-many axioms (i.e., a small collection of axioms).

(4) What ZF cannot do is to talk about classes, i.e., collections
that are too big to be (small) sets. Examples are model classes, varieties of
algebras, or categories of modules, or the collection of all sheaves
over some fixed topological space. As a concrete example, you cannot
make the one-to-one correspondence in (3) above into an equivalence of
categories. (Because there are too many type theories and too many toposes.)
  There are two ways out of this: (5) and (6) below.

(5) Most results you are interested in do not really need the
collection of all groups, or all sheaves on a topological space, but
only set many. And such results can be formalised perfectly within ZF.
>From this point of view, collections like large categories (or the
monster model in stability theory) are idealised objects, which
facilitate writing down our results, but are not really needed for
doing so.

(6) There is no real reason why we should not be able to form such big
collections of small sets. You are worried about paradoxes like
the one by Russell? An elementary analysis shows that that paradox
does not rely on the formation of the collection of all (small) sets,
but on the assumption that this collection _is_ a small set. 
  Of course, there is no guarantee that you do not run into other
difficulties, but intuitively you shouldn't: You can only encounter
trouble if you are not careful with your typing.

(7) To put (6) on a more mathematical base: The "cardinality" of the
universe of all (small) sets is a strongly inaccessible "cardinal".
>From this statement is should be clear that if ZFC (or even ZF) is
consistent so is

  ZFC + not there exists a strongly inaccessible cardinal.

On the other side, consistency of ZFC does not imply consistency of 
ZFC + there exists a strongly inaccessible cardinal.
(You can look this up in any better textbook on set-theory, like
[Kunen] or [Jech].)

(8) So what if we want to speak about a Grothendieck topos (which forms
a locally small category, i.e., the collection of objects is large,
but for each two objects the collection of arrows between them is
small)?
  In a formal ZF-based system this is best expressed in a model of (at
least) ZF + there exists a strongly inaccessible cardinal \kappa.
In our model, sets of cardinality less than \kappa are called small,
otherwise large. Given a small category equipped with a Grothendieck
topology (a site) you can form the category of all sheaves (functors) 
from the site which take as values small (!) sets. In our model, this
gives a large category with small Hom-sets, exactly as we wanted.
As well, it is within this setup that you should read the statement
that every Grothendieck topos is an elementary topos. 
  It should be noted that in such a setup you can formalise (3) as an 
equivalence of (large) categories.

(9) In the writings of the Grothendieck school, this is handled by
introducing various types of "universes" in which your collections
live: The small sets form one universe, the large sets another,
containing the first. 

(10) As you may have noticed, in this mail (and in the previous one) I
took a pretty conservative position. This was done to explain on the
basis of ZF what topos theory is, what it can do, and what you need to
treat it in a rigorous ZF-sense (nothing, if you talk about small
toposes, the ability to talk about large sets ("classes") if you want
to talk about Grothendieck toposes).
May be I should mention as well that you can do all this in an
intuitionistic environment: It doesn't matter whether your
meta-language is classical or intuitionistic. 
  
  All this does not affect the position Colin Mclarty takes on this
list. I still have to keep my promise and to come back to this in
another posting. 

Regards, Carsten Butz

Carsten Butz
Research Associate
Department of Computer Science, University of Aarhus (Denmark)
Research interests: Categorical logic, topos theory, homological algebra
WWW: http://www.brics.dk/~butz/