Toward Mac Lane Set Theory

Abstract

Steve Awodey Department of Philosophy Carnegie Mellon University Pittsburgh, PA 15213 USA

                      awodey@cmu.edu

June 2000

This work presents some tentative steps toward the theory of “Mac Lane sets”. Mac Lane [3, 4] has called for a categorical set theory with a global membership relation A ϵ B between sets. In contrast with elementary topos theory with its many useful interpretations, the intention is to axiomatize categories of sets specifically. Here the algebraic approach developed by Joyal and Moerdijk [2] is taken. Our axioms are close to those given by Alex Simpson [6], making use of some ideas of Dana Scott [5]. A related approach was taken in [1].

Mac Lane’s proposal for the category S of sets is based on a subcategory of distinguished monomorphisms A ↪ B, called inclusions, which are to order the objects. There are to be unique epi-inclusion factorizations, in addition to finite limits. Some further details are suggested, but many are left unspecified, the intention presumably being that further conditions will be determined. In that spirit, here we take the familiar approach of formulating a category of classes C, and determining the sets as those classes that are small. Unlike previous treatments, however, our notion of smallness is not primitive, but is defined simply as exponentiability:

Definition. A class A is small if C^{A} exists for every class C.

The notions of small map and small relation are derivative of this one: a map f : A → B is small if it is a small object in the slice category C/B, and a relation R ↣ A × B is small if its second projection R ↣ A × B → B is a small map.

Axioms for Sets and Classes

1. Classes. The category C of classes is regular; it has all finite limits and stable coequalizers of kernel pairs. Moreover, there is a universal class U, such that every class C has a selected monomorphism i_{C} : C ↪ U.

This determines the inclusions as those maps C → D that commute with the i’s.

C ^{⊂  >} D
[figure: i_{C}; i_{D}]
U

2. Powerclass. Every class C has a powerclass P (C), the class of all “subsets” of C. It has the defining property that maps D → P (C) correspond to small relations on C ×D, via pullback of the generic small relation ∈_{C}↣ C × P (C).

It follows that the class of all sets P (U) has a universal small map π : E → P (U), namely the second projection of ∈_{U}↣ U × P (U). Every small map f : A → B can be obtained as a pullback of π.

3. Small powers. The powerclass P (π : E → P (U)) of the universal small map is also small.

It can be shown that any small map f : A → B has a power object P (f) in C/B, so P (π) necessarily exists. The axiom implies that P^{n}(A) is small whenever A is.

4. Initial algebra. The canonical inclusion P (U) ↪ U is an initial algebra for the covariant functor P : C → C.

It follows that P (U) ≅ U, so that every element of a set is a set. A principle of ∈-induction also follows, as does the usual foundation axiom.

Sets in C

The sets are the small objects in C, which are also the small subobjects A ↪ U. Since P (U) ≅ U, the universe U “internalizes” the subcategory S → C of sets. More precisely, U is the class of objects of an internal category U in C, for which there is an equivalence,

Hom_{C}(1, U) ≃ S.

The universal generic small relation ∈_{U}↣ U × P (U) results in a relation on U by composing with i : P (U) ≅ U,

ϵ : ∈_{U}⟶ U × P (U) ≅ U × U.

This ϵ-relation on U therefore induces one on S, namely by defining:

A ϵ B iff iA ∈_{U} B.

This is the desired global membership relation on the category S of sets.

A Model

A model of our axioms for the category of sets and classes is provided by the hereditarily finite sets V_{ω} as follows.

C: V_{ω+1} as a full subcategory of Sets, i.e. the category of all C ⊆ V_{ω}

U: V_{ω}

S: A ⊆ V_{ω} is small iff it is finite

f : A → C is small iff all of its fibers f^{−1}{c} are finite

R ↣ A × B is small iff each Rb = {x ∈ A | xRb} is finite

P (C): the set P_{f}(C) of all finite subsets of C

The canonical inclusion i : P_{f}(V_{ω}) ↪ V_{ω} takes a finite subset A ⊆ V_{ω} to itself, regarded as an element iA ∈ V_{ω}. This is indeed an isomorphism, since every u ∈ V_{ω} is a finite subset of V_{ω}. Given any C ⊆ V_{ω} equipped with a map α : P_{f}(C) → C, define h : V_{ω} → C by:

h(∅) = α(∅),
h(A) = α({ha | a ∈ A}).

This is clearly the unique map that makes the following square commute.

\begin{matrix}P_{f}(V_{ω}) & \overline{P_{f}(h) _{>}} & P_{f}(C) \\ V_{ω} & i_{∨} & \overline{h _{>}} & A & α_{∨} \end{matrix}

References

[1] C. Butz, “Gödel-Bernays type theory,” CT ‘99, Coimbra, Portugal.

[2] A. Joyal and I. Moerdijk, Algebraic Set Theory, LMS Lecture Notes 220, Cambridge University Press, 1995.

[3] S. Mac Lane, Unpublished notes on set theory with elements, circulated privately, 1999.

[4] S. Mac Lane, “Foundations by using categories with elements,” Annual Meeting of the Association for Symbolic Logic, Urbana, June 2000.

[5] D. S. Scott, “Outline of a theory of classes,” unpublished manuscript dated April 22,1999.

[6] A. Simpson, “Elementary axioms for categories of classes,” 14th IEEE Symposium on Logic in Computer Science, pp. 77–85, 1999.