nLab algebraic set theory

Redirected from "Algebraic set theory".
Contents

Contents

Idea

The new insight taken as a starting point in algebraic set theory (AST) is that models of set theory are in fact algebras for a suitably presented algebraic theory, and that many familiar set-theoretic conditions (such as well-foundedness) are thereby related to familiar algebraic ones (such as freeness). (Awodey)

Description of the project

Also sometimes called categorical (meaning category-theoretic) set theory, algebraic set theory started to be developed in 1988 by André Joyal and Ieke Moerdijk and was first presented in detail as a book in 1995 by them. AST is a robust framework based on category theory to study and organize set theories and to construct models of set theories?. The aim of AST is to provide a uniform categorical semantics or description of set theories of different kinds (classical or constructive; bounded, predicative or impredicative; well founded? or ill founded, …), the various constructions of the cumulative hierarchy of pure sets, forcing models, sheaf models and realisability models.

Instead of focusing on categories of sets AST focuses on categories of classes. The basic tool of AST is the notion of a category with class structure (a category of classes equipped with a class of small maps (the intuition being that their fibres are small in some sense), powerclasses and a universal object) which provides an axiomatic framework in which models of set theory can be constructed. The notion of a class category permits both the definition of ZF-algebras? and related structures expressing the idea that the hierarchy of sets is an algebraic structure on the one hand and the interpretation of the first order logic of elementary set theory on the other. The subcategory of sets in a class category is an elementary topos and every elementary topos occurs as the topos of sets in some class category.

The class category itself always embeds into the ideal completion of a topos. The interpretation of the logic is that in every class category the universe is a model of basic intuitionistic set theory BIST\mathbf{BIST} that is logically complete? with respect to class category models. Therefore class categories generalize both topos theory and intuitionistic set theory. AST founds and formalizes set theory on the ZF-algebra with operations union and successor (singleton) instead of on the membership relation. The ZF axioms are nothing but a description of the free ZF-algebra just as the Peano axioms are a description of the free monoid on one generator. In this perspective the models of set theory are algebras for a suitably presented algebraic theory. Using an auxiliary notion of small map it is possible to extend the axioms of a topos and provide a general theory for uniformly constructing models of set theory out of toposes.

Naming

There are two reasons for referring to this research as “algebraic set theory”: The first reason is that the models of set theory that are produced by these methods are algebras for an abstractly presented “theory”, in a precise, technical sense known to category theorists as a monad. The notion of an algebra for a monad subsumes and generalizes that of a model for a conventional algebraic theory, such as groups, rings, modules, etc. Indeed, the first significant work in this style on the applications of category theory to the study of set theory was the monograph (Joyal-Moerdijk 1995) Algebraic set theory.

The second reason is that we believe the locution “algebraic logic” should properly refer to categorical logic rather than just the logic of Boole and his modern proponents, since categorical logic subsumes such lattice theoretic methods and not the other way around. Hence the term “algebraic set theory” rather than “categorical set theory”. This is in keeping with the use of “algebraic” to mean, essentially, “functorial” in modern algebraic topology, algebraic geometry, etc. (Awodey, Why “algebraic set theory”?)

Stack semantics

stack semantics provides a structural and somewhat more uniform way of treating “classes” in topos theory.

See also

References

Introductions and further pointers are at

Two introductions are:

A standard textbook is

A reference for BIST is

Last revised on July 16, 2022 at 01:53:02. See the history of this page for a list of all contributions to it.