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.III24.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:176183, 1938.
 [2]
Alfred Tarski.
On wellordered subsets of any set.
\em Fundamenta Mathematicae, 32:176183, 1939.
Received January 1, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]