Set theory

Content created by Egbert Rijke, Fredrik Bakke, Fernando Chu and Jonathan Prieto-Cubides.

Created on 2022-05-16.
Last modified on 2024-10-09.

Idea

In univalent type theory, what we refer to formally as a set is only in one sense what is clasically understood to be a “set”. Namely, we say a set is a type whose equality relation is a proposition. I.e., any two elements can be equal in at most one way.

However, both historically [FBHL73] and in contemporary mathematics [Kun11], what is usually meant by set theory is the study of a collection of related formal theories whose building blocks include a concept of sets and a propositionally valued elementhood relation, or membership relation, ∈ on them.

While this elementhood relation is not built into Martin–Löf type theory as a fundamental construct, there is one important instance of it present in Agda — namely, the smallness predicate:

  is-small l A := Σ (X : UU l), (A ≃ X).

We can say that a type A is an element of UU l if A is UU l-small in this sense. Indeed, that is-small l is a predicate is equivalent to the univalence axiom. This highlights a second connection between set theory and univalent type theory that is not directly compatible with the preconception that “set theory is a study of set-level mathematics”. Namely, the universe of sets need not itself be a set-level structure. In fact, with univalence it is a 1-type.

In this module, we consider ideas historically related to the study of set theories both as foundations of set-level mathematics, but also as a study of hierarchies in mathematics. This includes ideas such as cardinality and infinity, the cumulative hierarchy as a model of set theory, and Russell’s paradox.

Modules in the set theory namespace

module set-theory where

open import set-theory.baire-space public
open import set-theory.cantor-space public
open import set-theory.cantors-diagonal-argument public
open import set-theory.cardinalities public
open import set-theory.countable-sets public
open import set-theory.cumulative-hierarchy public
open import set-theory.infinite-sets public
open import set-theory.russells-paradox public
open import set-theory.uncountable-sets public

References

[FBHL73]
Abraham A. Fraenkel, Yehoshua Bar-Hillel, and Azriel Levy. Foundations of set theory. Volume 67 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam-London, revised edition, 1973. With the collaboration of Dirk van Dalen.
[Kun11]
Kenneth Kunen. Set theory. Volume 34 of Studies in Logic (London). College Publications, London, 2011. ISBN 978-1-84890-050-9.

Recent changes