Journal of Formalized Mathematics
Axiomatics, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

## Tarski Grothendieck Set Theory

Andrzej Trybulec
Warsaw University Bialystok
Supported by RPBP.III-24.B1.

### Summary.

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 [1] (see also [2]), and the Fr\ae nkel scheme. Also, the definition of equinumerosity is introduced.

#### Bibliography

[1] Alfred Tarski. \"Uber Unerreichbare Kardinalzahlen. \em Fundamenta Mathematicae, 30:176--183, 1938.
[2] Alfred Tarski. On well-ordered subsets of any set. \em Fundamenta Mathematicae, 32:176--183, 1939.