I started studying the basics of category theory recently, and after seeing how a great deal of group theory could be described categorically, I began to wonder if it were possible to describe set theory, or set-theoretic concepts, without reference to elements, i.e., by only using sets and functions. For example, instead of saying $x\in S$, one could say that there is a map $f:0\to S$, where $0$ is a singleton. Similarly, one could describe the power set $\mathscr{P}(X)$ by saying that for any function $f:Y\to X$, there are functions $g:0\to \mathscr{P}(X)$ and $h:\mathscr{P}(X)\to X$ such that $f=hg$. Disjoint unions can be described as coproducts, and cartesian products can be described by means of a universal property. I was wondering if it were possible to describe all of naive set theory in this way, and if so, whether any attempts have been made to do so.
-
3$\begingroup$ While you ask specifically about "naive set theory" you might be interested in learning about the concept of a "topos." This is, roughly, a category which looks enough like the category of sets that you can think of it as a kind of generalized set theory. There is a vast literature on this subject: the books by Moerdijk and MacLane, Johnstone, and Goldblatt are three good places to start. $\endgroup$– Eric FinsterCommented Sep 24, 2010 at 22:55
2 Answers
Yes! Lawvere's Elementary Theory of the Category of Sets (ETCS) is probably just what you want. It is a characterisation of Set up to equivalence from category theoretic principles alone. Todd Trimble explains a lot of it in some blog posting that have now migrated to the nLab, see the links here. This is what can be called a structural approach to foundations: one cares less about membership as how sets related to each other by functions.
It isn't the only one, Mike Shulman has SEAR (Sets Elements And Relations) which takes the named entities as primitive. It relies a little more on dependent type theory. This isn't too scary, it just means you keep track of what sort of set your elements live in (so questions like, 'is $\pi = (sin:\mathbb{R} \to [0,1]$?', don't come up) Note that ETCS a priori isn't about elements, but they are recovered as in your question: maps $1 \to S$, but it is by the time one uses the axiom 'Set is well pointed' that this comes about. SEAR on the other hand has elements are primitive, but then turn out to be what you say once functions are defined and subsets an so on.
Both of these can be taken to include Choice or not (ETCS has Choice by default, but it isn't necessary). SEAR-C is what we call SEAR with Choice, and it is equivalent to ZFC, and SEAR is equiconsistent with ZF (but not equivalent).
ETCS is slightly weaker than SEAR, but this hasn't been explored too much.
One can also consider the variant on SEAR called SEPS, which uses as primitives Sets, Elements, Pairing and Subsets (pairing is like canonical categorical product - stronger than the usual product in that it is specified. I wouldn't be surprised that if, after all's said and done, it's functorial). This is equivalent to SEAR
-
$\begingroup$ Indeed, Lawvere's work is exactly the sort of thing I was looking for. Thanks! $\endgroup$ Commented Sep 25, 2010 at 13:39
One such attempt is Algebraic Set Theory. A good intro can be found in the book Algebraic Set Theory by Joyal and Moerdijk. The Algebraic Set Theory group at CMU maintains a very good collection of resources.
