nLab ETCS

Idea

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 64) it is also the paradigm for a categorical foundation of mathematics.¹

The theory intends to capture in an 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. (See Lawvere (1976, p.119) for a detailed description of the notion ‘abstract set’.^{2 3 4 5})

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 much of traditional mathematics naturally takes place “inside” such a topos of constant sets, and second that this perspective generalizes beyond ETCS proper to toposes of variable and cohesive sets by varying the axioms: 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.

That is, ETCS locates the category of sets by the well-pointedness axiom as the discrete zero point on a ‘continuous’ range of toposes eligible for foundations. In particular, whereas ZF mainly provides ‘substance’ for mathematics, ETCS lives as a special type of form within the continuum of mathematical form itself.

Definition

The axioms of ETCS can be summed up in one sentence as:

Definition

The category of sets is the topos which

1. is a well-pointed topos

2. has a natural numbers object

3. and satisfies the axiom of choice.

For more details see

• fully formal ETCS.

A constructive view

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.

A contemporary perspective

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’s exposition of ETCS

Todd Trimble has a series of expository 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)

Related entries

• fully formal ETCS
• ETCS with elements
• structural set theory
• Zermelo Fraenkel set theory
• Cohesive Toposes and Cantor's "lauter Einsen"
• axiom of replacement
• ETCC
• practical foundations of mathematics
• foundations of mathematics
• ETCR
• Mostowski set theory

References

ETCS grew out of Lawvere’s experiences of teaching undergraduate foundations of analysis at Reed college in 1963 and was originally published in

• William Lawvere, An elementary theory of the category of sets , Proceedings of the National Academy of Science of the U.S.A 52 pp.1506-1511 (1964). (pdf)

A more or less contemporary review is

• C.C. Elgot, Review, JSL 37 no.1 (1972) pp. 191-192.

A longer version of Lawvere’s 1964 paper appears in

• William Lawvere, Colin McLarty, An elementary theory of the category of sets (long version) with commentary , Reprints in Theory and Applications of Categories 11 (2005) pp. 1-35. (TAC)

An undergraduate set-theory textbook using it is

• William Lawvere, Robert Rosebrugh, Sets for Mathematics , CUP 2003. (web)

Lawvere explains in detail his views on constant and variable ‘abstract sets’ on pp.118-128 of

• William Lawvere, Variable Quantities and Variable Structures in Topoi , pp.101-131 in Heller, Tierney (eds.), Algebra, Topology and Category Theory: a Collection of Papers in Honor of Samuel Eilenberg , Academic Press New York 1976.

See also ch. 2,3 of

• William Lawvere, Variable Sets Entendu and Variable Structure in Topoi , lecture notes University of Chicago 1975.

On the anticipation of ‘abstract sets’ in Cantor:

• William Lawvere, Cohesive Toposes and Cantor's "lauter Einsen", Philosophia Mathematica 2 no.3 (1994) pp.5-15. (pdf)

A short overview article on ETCS:

• Tom Leinster, Rethinking set theory arXiv.

An insightful and non-partisan view of ETCS can be found in a section of:

• Andreas Blass, Yuri Gurevich, Why Sets ? , Bull. Europ. Assoc. Theoret. Comp. Sci. 84 (2004) 139-156. (draft)

An extended discussion from a philosophical perspective is in

• Colin McLarty, Exploring Categorical Structuralism , Phil. Math. 12 (2004) 37-53.

• Øystein Linnebo, Richard Pettigrew, Category theory as an autonomous foundation, Phil. Math. 19 (2011) 227–254 (doi:10.1093/philmat/nkr024, preprint version (pdf))

For a more recent review from a critical perspective containing additional recent references see

• Solomon Feferman, Foundations of Unlimited Category Theory: What Remains to be Done , Review of Symbolic Logic 6 no.1 (2013) 6-15. (pdf)

An informative discussion of the pros and cons of Lawvere’s approach can be found in

• Jean-Pierre Marquis, Kreisel and Lawvere on Category Theory and the Foundations of Mathematics . (pdf-slides)

Palmgren’s ideas can be found here:

• Erik Palmgren, Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets, Annals of Pure and Applied Logic 163 10 (2012) 1384-1399 (2009) [doi:10.1016/j.apal.2012.01.011, arXiv:1201.6272]

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) 79-119.

---

1. For a comparative discussion of its virtues as foundation see foundations of mathematics , the texts by Todd Trimble or the informative paper by McLarty (2004). ↩

2. 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. ↩

3. R. Dedekind's views are also anticipating ‘abstract sets’ e.g. Bernstein reports in Dedekind’s works vol.3 (1932, p.449) that Dedekind gave as his intuition of a set: “a closed bag, containing determinate things that one can not see and of which one knows nothing beyond their existence and determinateness”. ↩

4. The first axiomatic set theory without primitive membership relation $\in$ was presumably proposed by A. Schoenflies in 1920: he modeled elements of sets as indecomposable subsets. See A. Schoenflies, Zur Axiomatik der Mengenlehre , Math. Ann. 83 (1921) pp.173-200; and Bemerkung zur Axiomatik der Grössen und Mengen , Math. Ann. 85 (1922) pp.60-64. ↩

5. The first axiomatic set theory based on the notion of function was von Neumann‘s 1925 version of what later became the set based NBG theory of classes. ↩