@ARTICLE{CLASSES3.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  NOTE1 = {This work has been supported by
       the Polish National Science Centre granted by decision
       no. DEC-2015/19/D/ST6/01473.},
  TITLE = {Grothendieck Universes},
  SECTION1 = {Grothendieck Universes Axioms},
  SECTION2 = {Grothendieck Universe Operator},
  SECTION3 = {Set of All Sets Up To Given Rank},
  SECTION4 = {Tarski vs. Grothendieck Universe},
  DAY = {31},
  MONTH = {May},
  YEAR = {2020},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {The foundation of the Mizar Mathematical Library,
  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\in U$.
  In this article, we prove, using the Mizar\cite{Role_MML} formalism,
  that the Grothendieck name is justified. We show
  the relationship between Tarski and Grothendieck universe.\par
  First we prove in Theorem~\ref{Th17} that every Grothendieck universe satisfies Tarski's Axiom A.
  Then in Theorem~\ref{Th18} we prove that every
  Grothendieck universe that contains a given set $X$,
  even the least (with respect to inclusion) denoted by \texttt{GrothendieckUniverse}$\:X$,
  has as a subset the least (with respect to inclusion) Tarski universe that contains $X$,
  denoted by the \texttt{Tarski-Class}$\:X$. Since Tarski universes, as opposed to Grothendieck universes,
  might not be transitive (called \texttt{epsilon-transitive} in the MML)
  we focused our attention to demonstrate that \texttt{Tarski-Class}$\:X\: \varsubsetneq\:$\texttt{GrothendieckUniverse}$\:X$
  for some $X$.
  We show in Theorem~\ref{Th19} that
  \texttt{Tarski-Class}$\:X$ where $X$ is the singleton of any infinite set
  is a proper subset of \texttt{GrothendieckUniverse}$\:X$.
  Finally we show that
  \texttt{Tarski-Class}$\:X\:=\:$\texttt{GrothendieckUniverse}$\:X$ holds under
  the assumption that $X$ is a transitive set.
  \par The formalisation is an extension of
  the formalisation used in \cite{CBKP-CICM/MKM19}.}}

@inproceedings{CBKP-CICM/MKM19,
  author    = {Brown, Chad E. and P\k{a}k, Karol},
  editor    = {Kaliszyk, Cezary and
               Brady, Edwin and
               Kohlhase, Andrea and
               Sacerdoti Coen, Claudio},
  title     = {A Tale of Two Set Theories},
  booktitle = {Intelligent Computer Mathematics -- 12th International Conference,
               {CICM} 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings},
  series    = {Lecture Notes in Computer Science},
  pages     = {44--60},
  year      = {2019},
  volume    = {11617},
  publisher = {Springer},
  doi       = {10.1007/978-3-030-23250-4_4}}


