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.


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



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

Received January 1, 1989

Download a postscript version, MML identifier index, Mizar home page]