categories: Re: Characterizing FinSet up to equivalence

[S.J.Vickers@open.ac.uk]

> In defense of sets, I very much like them as a foundational concept, in
> considerable part because one can reach a larger audience by starting from
> sets than from sheaves.  I was impressed that anyone would dislike sets so
> much as to compare starting from them to standing in wet concrete until it
> sets (or were you just making a pun about sets, Steve?).

No, I was in earnest. Having over quite a few years now seen for myself the
possibilities of using constructive reasoning to _simplify_ mathematics, so
that it now seems very obvious, I get overquickly distressed when other
people still haven't seen it.

However, I should explain that I was not criticizing sets as pedagogic
foundations, where you start from when you're explaining to a large
audience, nor as (if I may use Paul Taylor's phrase) practical foundations,
since the naive concepts of sets (albeit non-classical ones) underly the way
one reasons in toposes. The parable about concrete concerned philosophical
foundations, trying to fix on classical set theory as the deep unifying
account of what mathematics depends on.

Maybe in any case Vaughan wasn't thinking so much about such philosophical
diversions.

There is a pragmatic message. There are a number of different
characterizations of finiteness. Classically they are all equivalent, but it
has been known to topos theorists for quite a while now that if you start
considering non-classical sets (such as sheaves) or computational structures
you find they are inequivalent.

My belief is that the explanations of the differences can be understood in
naive set theoretic terms, though to see why they are genuine differences
and not just presentational you need to know a bit more about sheaves and
such.

A particular message (really arising out of geometric logic) is that
finiteness is _structure_ on a set, and not just a property: How do you know
a set is finite? There is something there in its structure that tells you.
I've tried to bring this out in my paper "Strongly algebraic = SFP
(topically)", soon to appear in Math. Structures in Computer Science, and
also available through my web page http://mcs.open.ac.uk/sjv22. In
particular you see there discussed Kuratowski finiteness (you can list of
all the elements but can't necessarily remove duplicates), finite decidable
(in addition you can detect inequality between elements and so can remove
duplicates) and finite ordinals (there is a canonical list that thereby puts
an ordering on the elements).

Consequently, when giving (as Vaughan did) a categorical characterization of
finiteness, it's worth pausing to consider which kind of finiteness you are
characterizing. Some will be more fruitful than others in terms of how
successfully they can generalize to the non-classical sets - with some you
will be stuck in your concrete, with others you can explore further afield.
The particular one Vaughan described was closely tied to the classical set
theory, but that is a limitation that is not inherent in the broad questions
he was asking.

That's a bit more subtle than saying "finite sets" are now characterized,
and treating "finite sheaves" as an interesting topic of further study along
with "finite Abelian groups" and so on. There is virtue in finding answers
for "finite sets" that also apply to "finite sheaves".

> Mentioning categories on Steve Simpson's FOM mailing list typically brings
> on a diatribe from someone railing against categories.  It would be nice
> if one could mention sets on this mailing list without the analogous
response.

Sorry if I railed. The categories list has the big advantage that its
readership is very well informed about both sets and categories, and fully
in a position to base their opinions on the mathematics and not the railing.

All the best,

Steve Vickers.