Tarski

Andrzej Trybulec Warsaw University Bialystok. Mizar project

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.

Andrzej Trybulec Warsaw University, Bialystok