Grothendieck Universes

The foundation of the Mizar Mathematical Library [2], is first-order Tarski-Grothendieck set theory. However, the foundation explicitly refers only to Tarski’s Axiom A, which states that for every set X there is a Tarski universe U such that X ∈ U. In this article, we prove, using the Mizar [3] formalism, that the Grothendieck name is justified. We show the relationship between Tarski and Grothendieck universe.

First we prove in Theorem (17) that every Grothendieck universe satisfies Tarski’s Axiom A. Then in Theorem (18) we prove that every Grothendieck universe that contains a given set X, even the least (with respect to inclusion) denoted by GrothendieckUniverseX, has as a subset the least (with respect to inclusion) Tarski universe that contains X, denoted by the Tarski-ClassX. Since Tarski universes, as opposed to Grothendieck universes [5], might not be transitive (called epsilon-transitive in the Mizar Mathematical Library [1]) we focused our attention to demonstrate that Tarski-Class X ⊊ GrothendieckUniverse X for some X.

Then we show in Theorem (19) that Tarski-ClassX where X is the singleton of any infinite set is a proper subset of GrothendieckUniverseX. Finally we show that Tarski-Class X = GrothendieckUniverse X holds under the assumption that X is a transitive set.

The formalisation is an extension of the formalisation used in [4].