Tarski–Grothendieck set theory

From Wikipedia, the free encyclopedia

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

Contents 1 Axioms 2 See also 3 Notes 4 References 5 External links

[edit] 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 A, the singleton {A} exists. Also, all possible subsets of A exist^{[clarification needed]}, and so does the power set of A;
• Two sets, their pair and ordered pairs exist;
• 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.

Any standard exposition of ZFC (e.g., Suppes 1960) reveals that given the four axioms above, all of the Definitional Axiom is redundant except for the existence of power sets and union sets, for which there are explicit ZFC axioms.

Tarski's axiom (adapted from Tarski 1939^[1]). 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)]].

It is Tarski's axiom that distinguishes TG from other axiomatic set theories. Tarski's axiom also implies the axioms of infinity, choice,^[2][3] and power set.^[4][5] 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.

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. Therefore TG does not directly support category theory or model theory. However, these theories can be modeled using suitable constructions on inaccessible cardinals.^{[citation needed]}

[edit] See also

• Grothendieck universe

[edit] Notes

1. ^ Tarski (1939)
2. ^ Tarski (1938)
3. ^ http://mmlquery.mizar.org/mml/current/wellord2.html#T26
4. ^ Robert Solovay, Re: AC and strongly inaccessible cardinals.
5. ^ Metamath grothpw.

[edit] 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". Michael Artin, Alexandre Grothendieck, Jean-Louis Verdier, eds. 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, Berlin; New York: Springer-Verlag. 
• 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. 

[edit] 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"