A set is a collection of objects considered as a single thing. The set of vowels in English is {a, e, i, o, u}. The set of prime numbers less than 10 is {2, 3, 5, 7}. You already think in sets whenever you group things together: “the books on this shelf,” “the people in this room,” “the ingredients in this recipe.” Mathematics takes that everyday act of grouping and makes it precise.
The one question set theory asks about any object and any set is: does the object belong to the set, or not? This yes-or-no test is called membership, and it is the only primitive concept. The number 3 is a member of {2, 3, 5, 7}; the number 4 is not. From membership alone, set theory builds the operations that pervade the rest of mathematics: union (combine two sets), intersection (find what they share), subset (one set contained in another), power set (the set of all subsets), and function (a rule assigning each element of one set to an element of another).
The standard axiomatization is ZFC (Zermelo-Fraenkel with the axiom of Choice), which provides a foundation sufficient for most of classical mathematics. ZFC is formulated in first-order logic and assumes the law of excluded middle.
Alternative foundations exist. Constructive set theory (e.g., CZF) drops excluded middle and choice, aligning with constructive reasoning. Category-theoretic foundations replace membership with morphisms and universal properties, offering a structural rather than material account of mathematical objects. Homotopy type theory provides yet another foundation, in which types play the role of spaces and equality carries homotopical content.
The formal architecture of this vault does not use set theory as its foundation. Instead, it builds on Heyting algebras and type theory. This choice reflects a commitment to constructive reasoning and to an algebraic treatment of logic, in which the structure of judgements is given by lattice operations rather than by set membership.
Georg Cantor originated set theory in the 1870s through his work on infinite cardinalities. Ernst Zermelo and Abraham Fraenkel formalized the axioms in the early twentieth century in response to the paradoxes (Russell’s, Burali-Forti’s) that arose from naive set-theoretic reasoning.
Related concepts
- Relation — defined as a set of ordered pairs
- Function — a relation where each input has exactly one output
- Proof — set theory provides one of the standard axiomatic foundations for proofs
- Heyting algebra — the algebraic foundation this vault uses instead of set-theoretic foundations
- Type theory — an alternative foundation that replaces sets with types