<abstract xmlns="http://www.w3.org/1999/xhtml">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 <italic>X</italic> there is a Tarski universe <italic>U</italic> such that <italic>X</italic> ∈ <italic>U</italic>. 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 <italic>X</italic>, even the least (with respect to inclusion) denoted by GrothendieckUniverse<italic>X</italic>, has as a subset the least (with respect to inclusion) Tarski universe that contains <italic>X</italic>, denoted by the Tarski-Class<italic>X</italic>. 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 <italic>X</italic> ⊊ GrothendieckUniverse <italic>X</italic> for some <italic>X</italic>.Then we show in Theorem (19) that Tarski-Class<italic>X</italic> where <italic>X</italic> is the singleton of any infinite set is a proper subset of GrothendieckUniverse<italic>X</italic>. Finally we show that Tarski-Class <italic>X</italic> = GrothendieckUniverse <italic>X</italic> holds under the assumption that <italic>X</italic> is a transitive set.The formalisation is an extension of the formalisation used in [4].</abstract>

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].

Grothendieck Universes

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"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...

Grothendieck Universes

Online veröffentlicht: 09. Jan. 2021

Seitenbereich: 211 - 215

Akzeptiert: 31. Mai 2020

DOI: https://doi.org/10.2478/forma-2020-0018

Schlüsselwörter
Tarski-Grothendieck set theory, Tarski’s Axiom A, Grothendieck universe

© 2020 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Grothendieck Universes

Online veröffentlicht: 09. Jan. 2021

Seitenbereich: 211 - 215

Akzeptiert: 31. Mai 2020

DOI: https://doi.org/10.2478/forma-2020-0018

SchlüsselwörterTarski-Grothendieck set theory, Tarski’s Axiom A, Grothendieck universe

© 2020 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Schlüsselwörter
Tarski-Grothendieck set theory, Tarski’s Axiom A, Grothendieck universe