FOM: How not to use universes, queries

[Colin McLarty]

	There are two senses in which number theorists do not "really" use
Grothendieck universes. The obvious one is that, insofar as you only want
the number theoretic results, you know the actually occuring references to
universes are eliminable.

	But even the standard theorems of homology, which explicitly deal with
universe-sized sets, hardly need the full proof theoretic strength of
universes. I am interested in the chasm between the apparently small proof
theoretic strength of these theorems, and the vast strength of currently
known set theories proving them (i.e. proving them as conventionally stated,
with quantification in the set theory over large categories and functors). 

	A few years ago I published in JSL reasons for thinking NF will not help,
and these apply to any set theory with a universal set. A more promising
approach is to look for weaker fragments of Grothendieck's foundation, that
is weaker fragments of ZFC+(every set is a member of some universe). And
here I have some questions.

Take this definition of a "Grothendieck universe": a transitive set U which
is a model of all ZFC axioms except replacement; and furthermore given any
set x in U and any onto function f:x-->y where y is a subset of U, y is also
in U. (I.e. replacement holds for any subset R of UxU existing in the
ambient set theory. Not only for relations expressed by formulas.) 

        In ZFC, Grothendieck's axiom (every set is a member of a universe)
is equivalent to existence of a proper class of inaccessibles.

        One weakening is obvious. As MacLane points out, a single
Grothendieck universe suffices for all of Grothendieck's purposes. So we have

                        ZFC+(there is a universe)

Now, take Z (Zermelo set theory, with the separation axiom rather than
replacement) plus Choice and a universe:

                         ZC+(there is a universe)

Separation in Z is enough to prove replacement holds within the universe U,
and that includes all of "ordinary" mathematics. We just do not require it
to hold outside the universe. This theory certainly suffices also for
Grothendieck's approach to homology.

        How much weaker is ZC+(universe) than ZFC+(universe)?

        Is ZC+(universe) equivalent to ZC+(an inaccessible)? I believe it
is, but I might be implicitly using replacement without noticing.

        Of course we could also drop replacement from the definition of a
universe. Say a "Grothendieck weak-universe" is a transitive set U which
models ZFC except for replacement, and further every subset of an element of
U is also an element of U. 

        Is ZFC+(a weak-universe) really a weaker theory that ZFC+(a
universe) or does the strength of ZFC make extension by a weak-universe
equivalent to extension by a universe?