FOM: anti-foundation and the category of sets

[Stephen G Simpson]

In May 2000 there were some interesting FOM postings about Aczel's
anti-foundation axiom, as an alternative to the familiar axiom of
foundation in ZFC.  It was said that the anti-foundation axiom may
suggest a broader or more general concept of set.  See in particular
Allen Hazen's posting of Wed, 31 May 2000 11:56:12 +0800.

There has also been much discussion, on FOM and elsewhere, contrasting
two pictures of the mathematical universe, presented by set theory and
category theory.  Call these pictures SET and CAT.  See especially
Chapter V of A.R.D. Mathias' forthcoming "Danish Lectures on the
Foundations of Mathematics", concerning a recent exchange of views
between Mathias and MacLane.  I am hoping that Mathias will soon give
FOM readers an opportunity to read an advance copy of the Danish
Lectures.

There is a link between these two discussion threads.  As Mathias and
other authors have noted, an important aspect of the SET/CAT contrast
is that, in the set-theoretic picture, well orderings and the axiom of
foundation play a key role, while in the category-theoretic or
structuralist picture, well foundedness almost completely disappears.

I now want to explain this link, by presenting a theorem.  The theorem
is trivial or at least very easy, but I find it illuminating.

THEOREM.  Let V be the standard intended model of ZFC.  Let V* be the
standard intended model of Aczel's theory 

       ZFC*  =  ZFC - foundation + anti-foundation.

Let C, C* be the category of all sets and mappings in V, V*
respectively.  Then: C and C* are isomorphic as categories.

REMARK.  This theorem means that the category of sets (i.e., the
standard example of a topos) cannot distinguish between (1) the
standard ZFC universe of well founded sets, (2) the alternative Aczel
or ZFC* universe of anti-well-founded sets.  This tends to explain the
observation of Mathias above.  The set-theoretic language (sets and
membership) is well equipped to discuss and use well foundedness, but
the category-theoretic language (sets and mappings) is not.  "Worauf
man nicht sprechen kann, darauf muss man schweigen."  ("Whereof one
cannot speak, thereof one must be silent.")

REMARK.  Aczel's anti-foundation axiom was mentioned in several talks
at the recent ASL 2000 meeting, including Rathjen's talk and the
presentation on Barwise's work.  In informal discussions at ASL 2000,
I tried out my theorem on various category theorists.  Some of them
believed it and some of them didn't.  In some cases I may not have
explained the theorem properly.  Steve Awodey seemed not only to
understand my theorem, but also to appreciate the point I was trying
to make with it.

Anyway, here is a proof of the theorem.  I hope FOM readers will
confirm or deny that this is correct.

PROOF.  I present only a proof sketch.  Note first that V is the
submodel of V* consisting of the well founded sets.  Futhermore, the
elements of V* are naturally interpreted in V as equivalence classes
of directed graphs without multiple edges, under bisimulation.  Thus
every set in z in V* has a cardinality card(z) in V.  In order to
prove the theorem, I shall assume the existence of a global choice
function, i.e., a class function F such that for every set z in V*,
F(z) is an element of z.  (Here I am using a well known theorem of
Solovay: NBG + global choice is a conservative extension of ZFC.)
Note also that, for each nonempty set in V, there are a proper class
of sets in V of the same cardinality.  And similarly for V*.  Thus,
using a global well ordering of V*, we can obtain a global bijection *
from V onto V*, such that card(x) = card(x*) for all x in V.  Then,
using global choice again, I can choose for each x in V a particular
bijection i_x from x onto x*.  Now, given a mapping f: x --> y in C
(i.e., in V), there is a unique f* : x* --> y* in C* (i.e., in V*)
such that

              f
         x  -----> y
         
         |         | 
     i_x |         | i_y
         |         | 
         v         v
    
         x* -----> y*
              f*

commutes.  It is straightforward to check that * : C --> C* is an
isomorphism of categories.  This proves the theorem.

-- Steve