FOM: anti-foundation and the category of sets

[Stephen G Simpson]

Allen Hazen Sun 11 Jun 2000 16:32:11 +0800 comments on my theorem
about the category of (well-founded) sets being the same as the
category of (non-well-founded) Aczel sets.

 >     If I understand it correctly, the idea is this:
 >     (a) On the categorical approach, sets of the same cardinality are
 > indistinguishable.  [...]

Yes, that is the idea.  It is almost trivial, really.  I used global
choice only in order to implement the idea in a specific way, to get
an actual isomorphism of categories.

 > The relative consistency of global choice [...] seems to require
 > only part of the machinery of an ordinary forcing proof:
 > conditions, but no generic.   ...

Actually, Solovay's proof of relative consistency of global choice
uses the machinery of forcing and genericity as well.  It is used in
verifying that the axioms of ZFC continue to hold when we expand the
language by throwing in the global choice operator as an additional
primitive.

See also Colin McLarty's posting of Tue 13 Jun 2000 12:46:32 -0500,
where McLarty asks whether one can obtain an explicitly defined
isomorphism between C and C*.  I conjecture that one cannot do so
provably in NBG.  Of course one can do so easily under appropriate
set-theoretic assumptions such as V=L which provide a global choice
function.

McLarty also elaborates a number of other highly relevant
distinctions.  In particular, McLarty is correct in pointing out that,
despite my theorem, the notion of a binary relational structure being
well founded is ``definable in categorical set theory'' (i.e.,
first-order definable in first-order the theory of the category of
sets and mappings).  What seems to be missing in categorical set
theory is not well foundedness as such, but rather a nice treatment of
the idea of a set being an element of another set which is an element
of another set etc.

This leads back to the question that I was originally trying to
address: Why is it that well foundedness plays such a large and
fruitful role in set-theoretic foundations (and in inner models,
forcing, large cardinals, etc), while at the same time playing a very
minor or almost nonexistent role in the category-theoretic or
structuralist way of organizing particular branches of mathematics?
Mathias has emphasized this contrast in his Danish lectures, which I
hope he will soon make available to FOM readers.

-- Steve