FOM: Categorical and Zermelo-style set theories

[Colin Mclarty]

Reply to message from kanovei at wminf2.math.uni-wuppertal.de of Tue, 10 Feb

Kanovei wrote of the "challenge axioms" for a topos suited to
classical analysis:    


    >To accomplish the picture, could a short formal 
    >declaration be attached, to explain the assumed 
    >role and importance of the proposed system for 
    >f.o.m ? 
    >
    >For instance the SET declaration would be that 
    >--------
    >set theory adequately presents all legitimate 
    >mathematical objects as sets, supports all known 
    >correct ways of mathematical reasoning, and 
    >converts all known mathematical theorems to 
    >theorems about sets (or: theorems of ZFC).
    >---------
    
    	This will do for my axioms as well, with one change: Where 
Kanovei says "theorems of ZFC" we will say "theorems of the 
elementary theory of the category of sets". (And again, I want
to be clear that when we talk about "my" axioms we mean only the
particular first order expression I posted. The axioms are
due to Lawvere and Tierney.)
    
    	Of course Kanovei's claim about "all legitimate
mathematical objects" needs some restriction and so does mine. 
ZFC does not give measurable cardinals, and so on. My axioms
are weaker than ZFC, strong enough for classical analysis. 
    
    	As I've mentioned before, there is a naive translation
between Zermelo-style set theory and categorical set theory:
Given any statement in categorical set theory, you get a statement
of Zermelo-style set theory simply by regarding the arrows as 
functions. 
    
    	Translating the other way is marginally harder, since the
sets of categorical set theory are more abstract than Zermelo's.
In short: a set in Zermelo-style theory has a membership tree,
which is set-membership construed as a relation on the transitive
closure of the set. Mostowski gave an order-theoretic description
of the relational isomorphism types which occur in this way.
Mostowski's description can be given in categorical set theory:
so every statement in Zermelo-style set theory can be rendered as 
a statement about Mostowski trees in categorical set theory.
    
    	Given strong enough axioms to support the theory of
Mostowski trees (which is not much), these translations exactly
preserve and reflect consistency. You can say exactly the same
things in either kind of set theory.     
    
    >(An optional 
    >part of this would be to explain why it is better 
    >than the set theoretic foundations.)
    
    	By "set theoretic foundations" Kanovei means Zermelo-style
set theory. The advantages I and others claim for categorical
set theory are familiar by now but here is a brief rehearsal. If
someone claims that one (or more) of these is not advantageous,
I'm not going to argue--I'll leave that to the "test of everyday
life":
    
1) Categorical set theory draws more on concepts needed in the
rest of math: finite limits, cartesian closedness et c. Zermelo-
style set theory rests on transfinitely iterated membership, 
ordinal induction, and others which are not much used in the 
rest of math. 

2) The sets of categorical set theory have exactly the structure
that is preserved by functions. In categorical set theory and 
Zermelo-style alike, functions preserve nothing but existence
and equality of elements: Given f:A-->B, for each element x of
A there exists a value fx in B, and if x=y in A then fx=fy in B.
In Zermelo-style set theories every element of a set has 
elements of its own et c. distinguishing it from every other set,
and a function f preserves nothing about that. In categorical
set theory, elements have no properties but existence and equality.

3) The categorical set theory axioms have many convenient fragments
(notably, the category axioms, finite limit axioms, topos axioms) 
of independent interest. And these axioms have a nice logical form
(which Peter Aczel has earlier discussed on fom).  

Colin