[FOM] Pratt on categorical foundations

[David Roberts]

Dear all,

(this post is deliberately written in a lighthearted style - it is not
how I usually address this list or this topic)

On 20 February 2012 23:31, Harvey Friedman <friedman at math.ohio-state.edu> wrote:
> How would you compare the
> simplicity of categorical foundations versus set theoretic foundations?

this is the nub of the matter. I believe proponents of both sides use
different criteria, and it is difficult to see the benefits of a set
of axioms without working with them.

But I would like not to add fuel to the fire, but some facts to the
discussion. And, if I may be so bold, un-ask Friedman's question, or
at least ask it in a different form.

"How would you compare the simplicity of structural foundations versus
material foundations?"

or

"How would you compare the simplicity of structural set theory versus
material set theory?"

'Structural' and 'material' are more useful distinctions than 'set
theoretic' and 'categorical', most importantly because ETCS is, like
it or not, a theory of sets, and so are other category-based
foundations. Also, because there is a structural set theory which is
not categorical in nature, but which shares some essential features
which might endear it to those who like ETCS. But we shall return to
that in a moment.

But what do 'structural' and 'material' mean? I hear you clamouring.
The distinction is largely metamathematical, and like the judge said,
I know it when I see it.

Material set theories include ZF(C), NBG, MK and so on. They are
roughly characterised by the fact elements of sets have an independent
existence, or to put it another way, the existence of the global
membership predicate. (It is this global membership predicate than
makes structural set theories qua foundations attractive to me because
this is something that mathematics outside of traditional set theory
does not use - but I digress.) The strength of material set theories
is evident, so I don't need to explain them here. Take it as given I
appreciate material set theory (and the more so since I started
teaching myself forcing).

Structural set theories have the contrasting property that elements of
sets are only determined by the sets that contain them and what
functions there are. It is harder to pin down what precisely makes a
set theory structural, but as the name implies, it is akin to
Bourbaki's structuralism, where properties of structures should be
isomorphism invariant. In this case, since we are using sets,
properties that can hold of a set should be preserved by bijections (
for example the statement a \in B is not preserved by a bijection B
\cong C). ETCS is a structural set theory, as is Algebraic Set Theory,
which axiomatises a category of classes and 'small' maps-those with
all fibres sets. The third example I know of is what I want to present
here, and is due to Michael Shulman.

This theory is called SEAR (Sets, Elements And Relations), and is
equiconsistent with ZF. It has a natural extension called SEAR-C which
is equivalent to ZFC (in the sense that a model of one is a model of
the other).
The theory has three sorts as is evident from the name (as opposed to
ZF(C) which has one), and uses the language of dependent type theory.

The details are here (http://ncatlab.org/nlab/show/SEAR), but can be
summarised as follows - my exposition may well not do the theory
justice.

==Preliminaries

Elements are members of a set, and we can only quantify over the
elements belonging to a given set.
Relations are between a pair of sets, and we can only quantify over
relations between a given pair of sets.
We can say when a relation holds of a pair of elements, one from each
of the two sets
We can't compare things of different sorts (so we can't assert x = A
for x an element and A a set, and so on)
(Note: we can quantify over all sets)
Functions are relations which are functional in the usual sense.

==Axioms (which I shall give informally, and add comments about how
the category theory rises independently from them - such comments are
not part of the development)

0. There exists a set with an element
1. Axiom scheme of relational comprehension
2. Relations R between sets A and B correspond to sets 'R' equipped
with functions 'R' --> A and 'R' --> B such that certain expected
properties hold (when we define products, the resulting 'R' --> A x B
is injection)
3. Power set
4. Infinity
5. Collection
6. Choice - every total relation 'contains' a function

==

>From 0-2 we can define the category Set, and it is a well-pointed
Heyting category, while from 0-3 it follows that the category Set is a
well-pointed topos.

SEAR uses 0-5, while SEAR-C adds 6. Nothing in these axioms depends on
category theory.

I hope this contributes light to the discussion, and not heat.

Cordially,

David Roberts

PS Once someone asked for a fully formal definition of the axioms of
ETCS - they can be found here
http://ncatlab.org/nlab/show/fully+formal+ETCS