[FOM] How analogous are categorial and material set theories?

[Neil Barton]

Dear All,

[I also sent this mail to the categories mailing list, so I apologise if
you receive a duplicate. I'm keen to get a wide range of people's
viewpoints.]

I'm very interested in how categorial and material set theories interact,
and in particular the advantages of each.

It's well-known that categorial viewpoints are good for isolating schematic
structural relationships. We can look at sets through this lens, by
considering a categorial set theory like ETCS (possibly augmented, e.g.
with replacement). A remark one sometimes finds is that once you have
defined membership via arrows from terminal objects, you could use ETCS for
all the purposes to which ZFC is normally put.

My question is the following:

(Q) To what extent can you ``do almost the same work'' with a categorial
set theory like ETCS vs. a material set theory like ZFC?

Just to give a bit more detail concerning what I'm thinking of: Something
material set theory is reasonably good at is building models (say to
analyse relative consistency), or comparing cardinality. However, there's
no denying that for represented abstract relationships the language is
somewhat clunky, since the same abstract schematic type can be multiply
instantiated by structures with very different set-theoretic properties.
So, to what extent can a categorial set theory like ETCS supply the good
bits of the fineness of grain associated with material set theories, whilst
modding out the `noise'?

For example, the following is easily stated in material set theory:

1. \aleph_17 is an accessible cardinal.

In material set theory, it's easy to define the aleph function and then
state that the 17th position in this function can be reached by iterating
powerset and replacement. But I wouldn't even know how to talk about
specific sets of different cardinalities categorially. I suppose you could
say something in terms of isomorphism between subobjects, and then
exponentials, but it's quite unclear to me how the specifcs would go. Is
that an easily claim to state (and prove) in ETCS?

2. How would you state that {{}} and {\beth_\omega} are very different
objects? Set-theoretically, these look very different (just consider their
transitive closures, for instance). But category-theoretically they should
look the same---since they are both singletons they are isomorphic. So is
this a case where their different set-theoretic propeties are considered
just `noise', or where ETCS just wouldn't see a realtionship, or where ETCS
can in fact see some of these properties (and I'm just missing something)?

3. How would ETCS deal with model theory and cardinality ascriptions? (This
links to a question asked earlier on the categories mailing list concerning
theories in category theory, and whether from the categorial viewpoint we
should be taking notice of this at all.) For instance, it's an interesting
theorem (for characterising structure) that a first-order theory
categorical in one uncountable power is categorical in every uncountable
power (Morley's Theorem). But I have no idea how one might formalise this
in something like ETCS---I know of Makkai and Reyes textbook (which I am
currently reading) on categorial logic (where theories are represented by
categories and models by functors), but I don't see how you could get
categoricity-in-power claims out of the set up there. Can this be done?

Any help and/or discussion would be greatly appreciated!

Best Wishes,

Neil

-- 
Dr. Neil Barton
Postdoctoral Research Fellow
Kurt Gödel Research Center for Mathematical Logic
University of Vienna
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20171124/67c05b54/attachment-0001.html>