A brief introduction to algebraic set theory∗Steve AwodeyAbstractThis brief article is intended to introduce the reader to the field of algebraic set theory,in which models of set theory of a new and fascinating kin d are determined alge-braically. The method is quite robus t, applying to various classical, intuitionistic, andconstructive set theories. Under this scheme some familiar set theoretic properties arerelated to algebraic ones, while others result from logical constraints. Conventionalelementary set theories are complete with respect to algebraic models, which arisein a variety of ways, including topologically, type-theoretically, and thr ough variation.Many previous results from topos theory involving realizability, permutation, and sheafmodels of set theory are subsumed, and the prospects for further such u nification seembright.1 IntroductionAlgebraic set theory (AST) is a new approach to the construction of models of set theory,invented by Andr´e Joyal and Ieke Moerdijk and first presented in detail in [31]. It promisesto be a flexible and powerful tool for the investigation of classical and intuitionistic systemsof elementary set theory, bringing to bear a new insight into the models of such systems.Indeed, it has already proven to be a quite robust framework, applying to the study ofclassical, intuitionistic, bounded, and predicative systems, and subsuming some previouslyunrelated techniques. The new insight taken as a starting point in AST is that models of settheory are in fact algebras for a suitably presented algebraic theory, and that many familiarset theoretic conditions (such as well-foundedness) are thereby related to familiar algebraicones (such as freeness).AST is currently the focus of active research by several authors, and new methods arebeing developed for the construction and organization of models o f various different systems,as well as for relating this approach with other, more traditional ones. Some recent resultsare mentioned here; however, the aim is not to provide a survey of the current state ofresearch (fo r which the field is not yet ripe), but to introduce the reader to its most basicconcepts, methods, and results. The list of references includes some works not cited in thetext and should serve as a guide to the literature, which the reader will hopefully find moreaccessible in virtue of this brief introduction.∗Dedicated to Saunders Mac Lane, 1909–20051Like the original presentation by Joyal & Moerdijk, much of the research in AST involves afairly heavy use of category theory. Whether this is really essential to the algebraic approachto set theory could be debated; but just as in other “algebraic” fields like algebraic geometry,topology, a nd number theory, the convenience of functorial methods is irresistible and hasstrongly influenced the development of the subject.1.1 Free algebrasBy way o f introduction, we begin by considering some free algebras of different kinds.• The free group on one generator {1} is, of course, the additive group of integers Z,and the free monoid (semi-group with unit) on {1} is the natural numbers N. Thestructure (N, s : N → N), where s(n) = n + 1, can also be described as the free“successor algebra” on one generator {0}, where a successor algebra is defined to bean object X equipped with an (arbitrary) endomorphism e : X → X. Explicitly, thismeans that given any such structure (X, e) and element x0∈ X there is a unique“successor a lg ebra homomorphism” f : N → X, i.e. a function with f ◦ s = e ◦ f, suchthat f(0) = x0, as indicated in the following commutative diagram.10-Ns-NXf?.................e-x0-Xf?.................This is an “algebraic” way of expressing the familiar recursion property o f the nat ura lnumbers.• The free sup-lattice (join semi-lattice) on a set X is the set Pfin(X) of all finite subsetsof X, with unions as joins, and the free complete sup-lattice is the full powerset PX.In each case, the “insertion of generators” is the singleton mapping x 7→ {x}. Thismeans that given any complete sup-lattice L and any function f : X → L, there is aunique join-preserving function¯f : PX → L with¯f{x} = f (x), as in:X{−}-PXL¯f?.................f-Namely, one can set¯f(U ) =Wx∈Uf(x).2• Now let us combine the foregoing kinds of algebras, and define a ZF-algebra (cf. [31])to be a complete sup-lattice A equipped with a successor operation s : A → A, i.e.an arbitrary endomorphism. A simple example is a powerset PX equipped with theidentity function 1PX: PX → PX. Of course, t his example is not f ree.Fact 1 . There are no free ZF-algebras.For suppose that s : A → A were the free ZF-algebra on e.g. the empty set ∅, and considerthe diagram:(1)A{−}-PAA¯s?.................s-where ¯s is the unique extension of s to PA, determined by the fact that A is a completesup-lattice and PA is the free one on (the underlying set of) A. If A were now also a freeZF-algebra, then one could use that fact to construct an inverse to ¯s (which t he reader cando as an exercise; see [31, II.1.2] for the solution).On the o ther hand, if we allow also “large ZF-algebras” — ones with a proper class ofelements — then there is indeed a free one, a nd it is quite familiar:Fact 2. The class V of all sets is the free ZF-algebra (on ∅), when equipped with the singletonoperation a 7→ {a} as successor s : V → V , and taking unions as joins.Note that, as before, joins are required only for set-sized collections of elements, so thatsuch unions do indeed exist. This distinction of size plays an essential role in the theory.Given the free ZF-algebra V , one can recover the m embership relation among sets justfrom the ZF-algebra structure by setting,(2) a ǫ b iff s(a) ≤ b.The following then results solely from the fact that V is the free ZF- algebra:Fact 3 ([31]). Let (V, s) be the free ZF-algebra. With membership defined as in (2) above,(V, ǫ) then models Zermelo-Fraenkel set theory,(V, ǫ) |= ZF.As things have been presented here, this last fact is hardly surprising: we began with Vas the class of all sets, so of course it satisfies the axioms of set theory! The real point, firstproved by Joyal & Moerdijk, is that the characterization of a structure (V, s) as a “f ree ZF-algebra” a lready suffices to ensure that it is a model of set theory — just as the descriptionof N as a free successor algebra already implies the recursion property, and the usual