Could not include topos theory - contents
basic constructions:
strong axioms
further
The Elementary Theory of the Category of Sets , or ETCS for short, is an axiomatic formulation of set theory in a category-theoretic spirit. As such, it is the prototypical structural set theory. Proposed shortly after ETCC in (Lawvere 65) it is also the paradigm for a categorical foundation of mathematics.^{1}
The theory intends to capture in an isomorphism invariant way the notion of a (constant) ‘abstract set’ whose elements lack internal structure and whose only external property is cardinality with further external relations arising from mappings. The membership relation is local and relative i.e. membership is meaningful only between an element of a set and a subset of the very same set.^{2}
More in detail, ETCS is a first-order theory axiomatizing elementary toposes and specifically those which are well-pointed, have a natural numbers object and satisfy the axiom of choice. The theory omits the axiom of replacement, however.
The idea is, first of all, that traditional mathematics naturally takes place “inside” such a topos, and second that by varying the axioms much of mathematics may be done inside more general toposes: for instance omitting the well-pointedness and the axiom of choice but adding the Kock-Lawvere axiom gives a smooth topos inside which synthetic differential geometry takes place.
The axioms of ETCS can be summed up in one sentence as:
The category of sets is the topos which
is a well-pointed topos
has a natural numbers object
and satisfies the axiom of choice.
For more details see
Erik Palmgren (Palmgren 2012) has a constructive predicative variant of ETCS, which can be summarized as:
$Set$ is a well-pointed $\Pi$-pretopos with a NNO and enough projectives (i.e. COSHEP is satisfied). Here “well-pointed” must be taken in its constructive sense, as including that the terminal object is indecomposable and projective.
Modern mathematics with its emphasis on concepts from homotopy theory would more directly be founded in a similar spirit by an axiomatization not just of elementary toposes but of elementary (∞,1)-toposes. This is roughly what univalent homotopy type theory accomplishes – for more on this see at relation between type theory and category theory – Univalent HoTT and Elementary infinity-toposes.
Instead of increasing the higher categorical dimension (n,r) in the first argument, one may also, in this context of elementary foundations, consider raising the second argument. The case $(2,2)$ is the elementary theory of the 2-category of categories (ETCC).
Todd Trimble has a series of expositional writings on ETCS which provide a very careful introduction and at the same time a wealth of useful details.
Todd Trimble, ZFC and ETCS: Elementary Theory of the Category of Sets (nLab entry, original blog entry)
Todd Trimble, ETCS: Internalizing the logic (nLab entry, original blog entry)
Todd Trimble, ETCS: Building joins and coproducts (nLab entry, original blog entry)
ETCS grew out of Lawvere’s experiences of teaching undergraduate foundations of analysis at Reed college in 1963 and was originally published in
A more or less contemporary review is
A longer version of Lawvere’s 1965 paper appears in
An undergraduate set-theory textbook using it is
Lawvere explains in detail his views on constant and variable ‘abstract sets’ on pp.118-128 of
See also ch. 2,3 of
On the anticipation of ‘abstract sets’ in Cantor:
A short overview article on ETCS:
An informative discussion of the pros and cons of Lawvere’s approach can be found in
Palmgren’s ideas can be found here:
For the relation between the theory of well-pointed toposes and weak Zermelo set theory as elucidated by work of J. Cole, Barry Mitchell, and G. Osius in the early 1970s see
Peter Johnstone, Topos Theory , Academic Press New York 1977 (Dover reprint 2014). (sections 9.2-3)
Barry Mitchell, Boolean Topoi and the Theory of Sets , JPAA 2 (1972) pp.261-274.
Gerhard Osius, Categorical Set Theory: A Characterization of the Category of Sets , JPAA 4 (1974) pp.79-119.
For a careful comparative discussion of its virtues as foundation see foundations of mathematics or the texts by Todd Trimble referred to below. ↩
See Lawvere (1976, p.119) for a detailed description of the notion ‘abstract set’. It has been pointed out by John Myhill that Cantor’s concept of ‘cardinal’ as a set of abstract units should be viewed as a structural set theory and a precursor to Lawvere’s concept of an ‘abstract set’. This view is endorsed and expanded in Lawvere 1994. ↩