Tarski–Grothendieck set theory

Tarski–Grothendieck set theory (TG) is an axiomatic set theory that was introduced as part of the Mizar system for formal verification of proofs. Its characteristic axiom is Tarski's axiom (see below). The theory is a non-conservative extension of Zermelo–Fraenkel set theory. Tarski–Grothendieck set theory is named after mathematicians Alfred Tarski and Alexander Grothendieck.

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;
• Unordered pair: A set with two distinct members. {a,b} = {b,a};
• Ordered pair: The set $\{\{a,b\},a\} = (a,b) \neq (b,a)$;
• Subset: A set all of whose members are members of another given set;
• The union of a family of sets Y: The set of all members of every member of Y.

Definitional axiom

• Given any set A, the singleton {A} exists.
• Given any two sets, their unordered and ordered pairs exist.
• Given any family of sets, its union exists.

TG includes the following axioms, which are conventional because also part of ZFC:

• 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.
• Axiom schema of replacement: 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.

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

• x itself;
• every subset of every member of y;
• the power set of every member of y;
• every subset of y of cardinality less than that of y.

More formally: ∃y [x ∈ y ∧ ∀z ∈ y [∀w (w ⊆ z → w ∈ y) ∧ ∃w ∈ y ∀v (v ⊆ z → v ∈ w)] ∧ ∀z [z ⊆ y → (z ≈ y ∨ z ∈ y)] ] or

∃y (x ∈ y ⋀ ∀z ∈ y (P(z) ⊆ y ⋀ ∃w ∈ y P(z) ⊆ w) ⋀ ∀z ∈ P(y)(z ≈ y ⋁ z ∈ y)), where "P(x)" denotes the power class of x and "≈" denotes equinumerosity.

What Tarski's axiom states (in the vernacular) for each set x there is a Grothendieck universe it belongs to.

It is Tarski's axiom that distinguishes TG from other axiomatic set theories. Tarski's axiom also implies the axioms of infinity, choice, and power set. It also implies the existence of inaccessible cardinals, thanks to which the ontology of TG is much richer than that of conventional set theories such as ZFC.

See also

• Grothendieck universe
• Axiom of limitation of size

References

• Blass, Andreas, Dimitriou, I. M., and Löwe, Benedikt (2007) "Inaccessible Cardinals without the Axiom of Choice," Fundamenta Mathematicae 194: 179-89.
• Bourbaki, Nicolas (1972). "Univers". In Michael Artin, Alexandre Grothendieck, Jean-Louis Verdier, eds. (in French). 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). Berlin; New York: Springer-Verlag. pp. 185–217. http://modular.fas.harvard.edu/sga/sga/4-1/4-1t_185.html. 
• Patrick Suppes (1960) Axiomatic Set Theory. Van Nostrand. Dover reprint, 1972.
• Tarski, Alfred (1938). "Über unerreichbare Kardinalzahlen". Fundamenta Mathematicae 30: 68–89. http://matwbn.icm.edu.pl/ksiazki/fm/fm30/fm30113.pdf. 
• Tarski, Alfred (1939). "On the well-ordered subsets of any set". Fundamenta Mathematicae 32: 176–183. http://matwbn.icm.edu.pl/ksiazki/fm/fm32/fm32115.pdf. 

External links

• Trybulec, Andrzej, 1989, "Tarski–Grothendieck Set Theory", Journal of Formalized Mathematics.
• Metamath: "Proof Explorer Home Page." Scroll down to "Grothendieck's Axiom."
• PlanetMath: "Tarski's Axiom"