Elementary Theory of the Category of Sets (ETCS)

Origin. F. William Lawvere, "An elementary theory of the category of sets" (PNAS, 1964), written the year after his thesis and rejected by referees who could not see that it was a set theory. Lawvere and Rosebrugh's Sets for Mathematics (2003) is the textbook; Tom Leinster's "Rethinking set theory" (2014) is the readable case for it. The structural alternative to the cumulative hierarchy.

Models. ZFC says what a set is made of: membership is primitive, and every set's identity is fixed by its elements, which are themselves sets, all the way down. ETCS says what a set does: the primitives are functions and composition, an element is a map from a one-element set, and nothing is asked about what a set contains beyond what its maps to and from other sets reveal. The question "is 3 ∈ 7?" has an answer in ZFC and is not well formed here.

Formalism.

Language: A category: objects, arrows, composition, identities. No membership relation. x ∈ A is not a primitive.

Elements as maps: An element of A is an arrow 1 → A from a terminal object. Two arrows f, g : A → B are equal iff they agree on all elements — which is the axiom that 1 is a generator.

The axioms (a well-pointed topos with NNO and choice):

Finite limits exist (terminal object, products, equalizers)
Exponentials exist: B^A, so the category is cartesian closed
A subobject classifier Ω exists: subsets are maps A → Ω
A natural numbers object exists
Every epi splits (the axiom of choice)
1 is a generator (well-pointedness)
Ω has exactly two elements (Boolean, so classical logic)

Strength: ETCS is bi-interpretable with BZC — bounded Zermelo with choice: Zermelo's axioms with separation restricted to bounded formulas, plus choice. Weaker than ZFC: no replacement. ETCS + replacement (as a categorical axiom scheme) is bi-interpretable with ZFC.

What changes in practice: No global membership: elements of different sets are not comparable. No cumulative hierarchy: sets are not built in stages. Isomorphic sets are interchangeable — structural invariance is automatic rather than a convention. Functions are primitive; ZFC's coding of a function as a set of ordered pairs is unnecessary.

Symbols.

Symbol	Unicode	Name	Meaning
Ω	U+03A9	Omega / Subobject classifier	Subsets as maps to it
∈	U+2208	Membership	Primitive in ZFC; not a primitive here
→	U+2192	Arrow	A function, the primitive notion
↠	U+21A0	Epimorphism	Surjection; the choice axiom says every one splits
ω	U+03C9	Omega	Rank index, as in the model V_{ω+ω} of Zermelo set theory
ℵ	U+2135	Aleph	Cardinal notation; ℵ_ω is not provably a set in ETCS
1	—	Terminal object	Elements are arrows out of it
B^A	—	Exponential	The set of functions A → B
N	—	Natural numbers object	Induction, categorically
BZC	—	Bounded Zermelo + choice	ETCS's bi-interpretable partner
ETCS+R	—	ETCS with replacement	The version bi-interpretable with ZFC

Metatheory. Bi-interpretability with bounded Zermelo set theory with choice is the result that makes ETCS a set theory rather than a manifesto: Cole, Mitchell and Osius established in the early 1970s that models of ETCS and models of BZC translate into one another, preserving all theorems about sets, so the choice between membership and maps is one of presentation and not of content. McLarty showed that adding a categorical replacement scheme yields ETCS+R, bi-interpretable with ZFC. The strictness of the inclusion is checkable: ZFC proves the consistency of Zermelo set theory, since V_{ω+ω} is a model of it, so ZFC proves Con(ETCS) and ETCS is strictly weaker. ETCS is finitely axiomatizable, unlike ZFC, which requires the infinite schemes of separation and replacement. Booleanness is not an independent commitment: every well-pointed topos is two-valued and Boolean, so the axiom that Ω has exactly two elements is a consequence of well-pointedness rather than an addition, and by Diaconescu's theorem the choice axiom would force it in any case. Independence results transfer — the continuum hypothesis is independent of ETCS, obtained by the same Boolean-valued and sheaf constructions.

Applies to. Foundations, as the structural alternative to the iterative conception. Category theory's relation to set theory. Type-theoretic foundations, where ETCS is the closest set-theoretic relative. Any argument about whether membership is fundamental or an artifact of a coding.

Limitations. Without replacement the theory is strictly weaker than ZFC, and the gap is not cosmetic: ℵ_ω is not provably a set, transfinite recursion of length beyond the bounded ranks is unavailable, and Borel determinacy — which Friedman (1971) showed requires ω₁ iterations of the power set — is unprovable. Well-pointedness is a severe restriction on models: the only toposes satisfying it are, in effect, categories of sets, so no sheaf topos, no presheaf topos and no realizability topos is a model of ETCS, and the theory therefore cannot serve as the internal language for the topos-theoretic constructions it resembles. Elements are global elements only, so generalized-element and Kripke–Joyal reasoning is unavailable. Choice is an axiom rather than an option, and with Booleanness forced by well-pointedness the theory admits no constructive variant without dropping both. Large cardinal axioms have no natural formulation in the arrows-only language, so the upper reach of set theory is out of view.