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.

MML Identifier: TARSKI

Contents

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.