Open AccessGrothendieck Universes
Author(s) -
Karol Pąk
Publication year - 2020
Publication title -
formalized mathematics
Language(s) - English
Resource type - Journals
eISSN - 1898-9934
pISSN - 1426-2630
DOI - 10.2478/forma-2020-0018
Subject(s) - mathematics , universe , transitive relation , class (philosophy) , axiom , set theory , extension (predicate logic) , discrete mathematics , set (abstract data type) , algebra over a field , pure mathematics , combinatorics , computer science , artificial intelligence , physics , geometry , astrophysics , programming language
Summary 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 GrothendieckUniverse X , has as a subset the least (with respect to inclusion) Tarski universe that contains X , denoted by the Tarski-Class X . 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-Class X where X is the singleton of any infinite set is a proper subset of GrothendieckUniverse X . 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].