Tarski–Grothendieck set theory

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 [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 [Tarski (1938)] [http://mmlquery.mizar.org/mml/current/wellord2.html#T26] 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.

ee also

*Grothendieck universe

Notes

References

* cite conference
first = Nicolas
last = Bourbaki
authorlink = Nicolas Bourbaki
year = 1972
title = Univers
booktitle = 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)
editor = Michael Artin, Alexandre Grothendieck, Jean-Louis Verdier, eds.
publisher = Springer-Verlag
location = Berlin; New York
language = French
pages = 185–217
url = http://modular.fas.harvard.edu/sga/sga/4-1/4-1t_185.html

* cite journal
last = Tarski
first = Alfred
authorlink = Alfred Tarski
year = 1938
title = Über unerreichbare Kardinalzahlen
journal = Fundamenta Mathematicae
volume = 30
pages = 68–89
url = http://matwbn.icm.edu.pl/ksiazki/fm/fm30/fm30113.pdf

* cite journal
last = Tarski
first = Alfred
authorlink = Alfred Tarski
year = 1939
title = On the well-ordered subsets of any set
journal = Fundamenta Mathematicae
volume = 32
pages = 176–183
url = http://matwbn.icm.edu.pl/ksiazki/fm/fm32/fm32115.pdf

External links

*Trybulec, Andrzej, 1989, " [http://mizar.uwb.edu.pl/JFM/Axiomatics/tarski.html Tarski–Grothendieck Set Theory] ", "Journal of Formalized Mathematics".
* PlanetMath: " [http://planetmath.org/encyclopedia/TarskisAxiom.html Tarski's Axiom] "