FOM: alternative foundations?

[holmes@catseye.idbsu.edu]

Hasan Keler (?) asked:

>   "ZFC is a foundation of the 99% of mathematics."
>But what is the remaining 1% ?
>And why is ZFC not a foundation of this 1% ?

I reply: 

There is a certain amount of mathematics done in set theories other
than ZFC.  I have written a textbook using NFU (Jensen's variant with
urelements of Quine's "New Foundations") though most of my work in set
theory has been "about" NFU in standard set theory (ZFC).  On the
other hand, all of my theorem proving work has been in a foundation
equivalent to NFU (the built in logic of my prover).  Most theorem
proving systems, for whatever reason, do not use ZFC as their
foundation: some use Church's simple theory of types (which is easily
modelled in ZFC, it must be noted, but this doesn't make it the same
as ZFC -- the logic of my prover is also fairly easily modelled in
ZFC).  Some provers (Nuprl, Coq) use constructive type theories (with
intuitionistic logic) as their foundations; these require one to do
mathematics in a style very remote from the practice of most
mathematicians (in comparison with these, the style of work in my
prover or in classical type theory based provers like HOL is much more
similar to standard mathematical practice).  Isabelle has a version
which uses ZFC as the foundation; Mizar uses an extension of ZFC with
many inaccessibles as its foundation.

The built-in logic of a theorem prover of sufficient strength is
certainly a foundation for mathematics in Simpson and Friedman's
sense, and a survey of this field shows that ZFC still does not hold
the field uncontested (in fact, it is usually NOT chosen).

There are other groups of mathematicians that use nonstandard set
theories; there is for example a group that works on the alternative
set theory of Vopenka.  There are people who work in nonstandard analysis
who use a set theory called IST (which is in a sense an extension of ZFC
but requires all infinite sets to have subclasses which are not sets).

There are of course strong extensions of ZFC, as with large cardinals.
There is work done in ZF without choice (e.g. ZF + AD).

Most of mathematics is not set theory and is currently "officially"
founded on ZFC.  It should be noted that the claim of ZFC to all of
this territory is not really all that strong; if it became fashionable
to switch to classical type theory or NFU, the changes in the main
body of mathematics would be minimal.  There are systems like bounded
Zermelo set theory (aka Mac Lane set theory -- a subsystem of ZFC) or
Ackermann set theory (also closely related to ZFC) to which almost all
of mathematics could be adapted with hardly a tremor.  A change to a
constructive viewpoint would have radical effects (and so is not
likely to happen); Vopenka's theory would (I think) have strange
effects and doesn't accomodate any cardinal greater than c (but most
of mathematics doesn't need any such cardinals); IST includes ZFC as a
subset but has a quite different conceptual basis: its adoption as an
official foundation would signal a change in mathematical outlook (but
would be easy from the standpoint of importing classical results
framed in terms of ZFC).  I don't regard any such events as likely --
not because of the superiority of ZFC but because of its established
position and the lack of any compelling reason to make any changes.
(Nor in fact do I regard any such events as particularly desirable).

The remainder cannot be identified with category theory, which is
generally founded on very mild extensions of ZFC.  Efforts in the
direction of "category theoretic foundations" do fall in the area of
alternative foundations, of course, but cannot lay claim to all of
category theory.

Thus Simpson:

The answer to this is that category theory *cannot* get around the
Russell paradox.  When category theorists speak of ``the category of
all categories'' (as they often do), they are whistling in the dark.

I comment:

As has already been pointed out on this list, "the category of all
categories" is not contradictory; this object exists (as a set
category) and contains itself in NFU.  But it doesn't have desirable
properties (for example, it is not cartesian closed).  Simpson
reproaches others quite freely for speaking vaguely -- let's be
careful about this, too.

This falls in the same category as common assertions that the
existence of the set of all sets is contradictory -- it is not.  One
needs something like Zermelo's axiom of separation to get a
contradiction from the universal set.  NFU and various other set
theories with restrictions on comprehension different from Zermelo's
do have universal sets, categories of all categories, and other such
beasts (but there is no free lunch -- these objects turn out not to
have all naively expected properties).

He continues:

In some FOM postings around May 11, 1999, I came up with a fairly
general argument which is a category-theoretic analog of the Russell
paradox.  The argument takes place in an informal ``naive category
theory'' setting and could easily be transplanted to a variety of
formal settings.  The argument concludes that, not only does ``the
category of all categories'' not exist, but there is no category of
categories containing *an isomorphic copy of* every category.

I comment:

of course, the point is that some of the assumptions in his naive
category theory setting do not hold in NFU.  It would be nice to see
precisely what these are.

Re the discussion between Bauer and Simpson:

I think Bauer has a point.  The concepts of category theory are much
more generally applicable than those of (say) group theory; it seems
clear to me that category theorists are doing something "foundational"
-- but not in a sense which competes with the sense in which set
theories are foundational (the advocates of "category theoretical
foundations" are being as wrong-headed as Simpson in this respect).

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.boisestate.edu
not glimpse the wonders therein. | http://math.boisestate.edu/~holmes