Tarski–Grothendieck set theory (TG) is an axiomatic set theory derived by marrying Tarski's axiom (see below) to ZF. TG is part of the Mizar system for formal computer verification of mathematical proofs.

Axioms

While the axioms and definitions defining Mizar's basic objects and processes are fully formal, they are described informally below.

TG includes the following standard definitions:

• Singleton: A set with one member
• Pair: A set with two distinct members. {a,b} = {b,a}
• Ordered pair: The set {{a,b},a} = (a,b) ≠ (b,a)
• Subset: A set all of whose members are members of another given set
• The Power set of a set X: The set of all possible subsets of X
• The Union of a family of sets Y: The set of all members of every member of Y

Definitional axiom: Given any set, its singleton, power set, and all possible subsets exist. Given any two sets, their pair and ordered pairs exist.

TG includes the following conventional axioms:

• Set axiom: Quantified variables range over sets alone; everything is a set (the same ontology as ZFC).
• Extensionality axiom: Two sets are identical if they have the same members.
• Axiom of regularity: No set is a member of itself, and circular chains of membership are impossible.
• Fraenkel's scheme: Let the domain of the function F be the set A. Then the range of F (the values of F(x) for all members x of A) is also a set. This is the axiom schema of Replacement of ZFC.

Tarski's axiom distinguishes TG from other axiomatic set theories.

Tarski's axiom (adapted from Tarski 1939). For every set X, there exists a set U whose members include:

• X itself;
• Every subset of every member of U;
• The power set of every member of U;
• Every subset of U of cardinality less than that of U.

Tarski's axiom implies the Axiom of Choice and the existence of inaccessible cardinals. Thanks to these cardinals, the ontology of TG is much richer than that of conventional set theories such as ZFC.

Unlike Von Neumann–Bernays–Gödel set theory, TG does not provide for proper classes containing all sets of a particular type, such as the class of all cardinal numbers or the class of all sets. It therefore does not support category theory or model theory directly. However, such theories can be approximated using suitable constructions on inaccessible cardinals.

See also

• Grothendieck universe

Notes

References

• Bourbaki, Nicolas (1972). "Univers". Séminaire de Géométrie Algébrique du Bois Marie – 1963-64 – Théorie des topos et cohomologie étale des schémas – (SGA 4) – vol. 1 (Lecture notes in mathematics 269), 185–217. .
• Tarski, Alfred (1938). "Über unerreichbare Kardinalzahlen". Fundamenta Mathematicae 30 68–89.
• Tarski, Alfred (1939). "On the well-ordered subsets of any set". Fundamenta Mathematicae 32 176–183.

External links

• Trybulec, Andrzej, 1989, " Tarski–Grothendieck Set Theory", Journal of Formalized Mathematics.
• PlanetMath: " Tarski's Axiom"