Journal of Formalized Mathematics
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Tarski Grothendieck Set Theory
Warsaw University Bialystok
Supported by RPBP.III-24.B1.
This is the first part of the axiomatics of the Mizar system. It includes
the axioms of the Tarski Grothendieck set theory. They are:
the axiom stating that everything is a set,
the extensionality axiom,
the definitional axiom of the singleton,
the definitional axiom of the pair,
the definitional axiom of the union of a family of sets,
the definitional axiom of the boolean (the power set) of a set,
the regularity axiom,
the definitional axiom of the ordered pair,
the Tarski's axiom~A introduced in  (see also ),
and the Fr\ae nkel scheme.
Also, the definition of equinumerosity is introduced.
\"Uber Unerreichbare Kardinalzahlen.
\em Fundamenta Mathematicae, 30:176--183, 1938.
On well-ordered subsets of any set.
\em Fundamenta Mathematicae, 32:176--183, 1939.
Received January 1, 1989
Download a postscript version,
MML identifier index,
Mizar home page]