FOM: Alternatives to ZFC in actual use

[Joe Shipman]

Holmes has made the case that NFU provides a possible alternative
foundation for mathematics.  He admits its inferiority to ZFC, but
defends it as a successor to Russell's system that (in his more
intuitively acceptable axiomatization) allows one to develop a "naive"
set theory suitable for doing mathematics.  If Zermelo had not existed,
it is possible that something like NFU could have been considered more
seriously, although if it had been I am sure someone would have
"discovered" Zermelo's superior cumulative hierarchy eventually.

The most intriguing feature of NFU in my opinion is that natural
extensions of it entail large cardinals, as Solovay and Holmes have
shown.  Harvey Friedman argues that NFU is so unnatural compared to ZFC
that this doesn't really provide a better justification of those
cardinals.  The technical point is that with NFU you get an automorphism
of the universe for free, and if you make very natural assumptions about
this automorphism you get (consistency of) large cardinals; from ZFC you
have to postulate the automorphism first and then regularity properties
for it in order to get large cardinals.  The situation calls for
clarification; possibly the problem of consistency of NF may involve
large cardinals in a similar way.

But NFU is just an existence proof of alternative foundations.  I am
much more interested in whether alternatives and extensions to ZFC are
implicitly used in the actual public writings and utterances of
mathematicians.  We all know that set theorists freely use lots of
higher axioms, but anything they publish in a journal (as opposed to
presenting in a colloquium talk, for example) will always be carefully
framed within ZFC, by saying  "ZFC + X implies Y" rather than simply
assuming X and deriving Y.

What other examples are there?  ZFC is not really the upper limit of
what's accepted generally -- stronger set theories like Morse-Kelley set
theory are not doubted by anybody who doesn't already doubt ZFC.  But
has any piece of "ordinary" mathematics every been done in a way that
can be straightforwardly formalized in MK but *not* in ZFC?  (The proof
of Con(ZFC) in MK is not "ordinary mathematics").

I can think of only one real example outside of the logic/set
theory/f.o.m. community where assumptions that go beyond ZFC are
regularly made without much fuss.  This is in category theory, where
Grothendieck's "Universe" axiom (any set is contained in a "Universe",
which is another way of saying that inaccessibles form a proper class)
is sometimes used.  This is a useful axiom (I used it myself on the
f.o.m. a couple of months ago in my initial definition of an "eligible
cardinal").  While very weak as large cardinal axioms go (having less
consistency strength than a Mahlo or any axiom where there is an
inaccessible limit of inaccessibles), it goes significantly beyond ZFC,
MK, or any other textbook version of set theory.

Here is my question: was any statement of ordinary mathematics (that is,
a statement about sets of rank less than omega+omega) ever proved from
Grothendieck Universes, in which the Universe assumption was really
used?  (Statements that obviously imply Con(ZFC) don't count!)  Maybe
Barry Mazur, a FOM-digest subscriber, can help us out here.  If the
answer to this question is "Yes", then the special role of ZFC is called
into question; if the answer is "No", then why did Grothendieck bother?

-- Joe Shipman