Definitions
Nearby Words

# Tarski–Grothendieck set theory

TarskiGrothendieck 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:

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.

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