HOME

TheInfoList



OR:

Tarski–Grothendieck set theory (TG, named after mathematicians
Alfred Tarski Alfred Tarski (; ; born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician ...
and
Alexander Grothendieck Alexander Grothendieck, later Alexandre Grothendieck in French (; ; ; 28 March 1928 – 13 November 2014), was a German-born French mathematician who became the leading figure in the creation of modern algebraic geometry. His research ext ...
) is an
axiomatic set theory Set theory is the branch of mathematical logic that studies Set (mathematics), sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory – as a branch of mathema ...
. It is a non-conservative extension of
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes suc ...
(ZFC) and is distinguished from other axiomatic set theories by the inclusion of Tarski's axiom, which states that for each set there is a "Tarski universe" it belongs to (see below). Tarski's axiom implies the existence of
inaccessible cardinal In set theory, a cardinal number is a strongly inaccessible cardinal if it is uncountable, regular, and a strong limit cardinal. A cardinal is a weakly inaccessible cardinal if it is uncountable, regular, and a weak limit cardinal. Since abou ...
s, providing a richer
ontology Ontology is the philosophical study of existence, being. It is traditionally understood as the subdiscipline of metaphysics focused on the most general features of reality. As one of the most fundamental concepts, being encompasses all of realit ...
than ZFC. For example, adding this axiom supports
category theory Category theory is a general theory of mathematical structures and their relations. It was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Category theory ...
. The Mizar system and Metamath use Tarski–Grothendieck set theory for formal verification of proofs.


Axioms

Tarski–Grothendieck set theory starts with conventional
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes suc ...
and then adds “Tarski's axiom”. We will use the
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
s,
definition A definition is a statement of the meaning of a term (a word, phrase, or other set of symbols). Definitions can be classified into two large categories: intensional definitions (which try to give the sense of a term), and extensional definitio ...
s, and notation of Mizar to describe it. Mizar's basic objects and processes are fully
formal Formal, formality, informal or informality imply the complying with, or not complying with, some set of requirements ( forms, in Ancient Greek). They may refer to: Dress code and events * Formal wear, attire for formal events * Semi-formal atti ...
; they are described informally below. First, let us assume that: * Given any set A, the singleton \ exists. * Given any two sets, their unordered and ordered pairs exist. * Given any set of sets, its union exists. TG includes the following axioms, which are conventional because they are also part of ZFC: * Set axiom: Quantified variables range over sets alone; everything is a set (the same
ontology Ontology is the philosophical study of existence, being. It is traditionally understood as the subdiscipline of metaphysics focused on the most general features of reality. As one of the most fundamental concepts, being encompasses all of realit ...
as ZFC). *
Axiom of extensionality The axiom of extensionality, also called the axiom of extent, is an axiom used in many forms of axiomatic set theory, such as Zermelo–Fraenkel set theory. The axiom defines what a Set (mathematics), set is. Informally, the axiom means that the ...
: Two sets are identical if they have the same members. *
Axiom of regularity In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every Empty set, non-empty Set (mathematics), set ''A'' contains an element that is Disjoint sets, disjoin ...
: No set is a member of itself, and circular chains of membership are impossible. *
Axiom schema of replacement In set theory, the axiom schema of replacement is a Axiom schema, schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image (mathematics), image of any Set (mathematics), set under any definable functional predicate, mappi ...
: Let the domain of the class function F be the set A. Then the
range Range may refer to: Geography * Range (geographic), a chain of hills or mountains; a somewhat linear, complex mountainous or hilly area (cordillera, sierra) ** Mountain range, a group of mountains bordered by lowlands * Range, a term used to i ...
of F (the values of F(x) for all members x of A) is also a set. It is Tarski's axiom that distinguishes TG from other axiomatic set theories. Tarski's axiom also implies the axioms of
infinity Infinity is something which is boundless, endless, or larger than any natural number. It is denoted by \infty, called the infinity symbol. From the time of the Ancient Greek mathematics, ancient Greeks, the Infinity (philosophy), philosophic ...
,
choice A choice is the range of different things from which a being can choose. The arrival at a choice may incorporate Motivation, motivators and Choice modelling, models. Freedom of choice is generally cherished, whereas a severely limited or arti ...
, and
power set In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
. It also implies the existence of
inaccessible cardinal In set theory, a cardinal number is a strongly inaccessible cardinal if it is uncountable, regular, and a strong limit cardinal. A cardinal is a weakly inaccessible cardinal if it is uncountable, regular, and a weak limit cardinal. Since abou ...
s, thanks to which the
ontology Ontology is the philosophical study of existence, being. It is traditionally understood as the subdiscipline of metaphysics focused on the most general features of reality. As one of the most fundamental concepts, being encompasses all of realit ...
of TG is much richer than that of conventional set theories such as ZFC. * Tarski's axiom (adapted from Tarski 1939). For every set s, there exists a set u (a "universe") such that # s \in u: it contains s # (\forall x \in u) (\forall y \subseteq x) (y \in u): it contains every
subset In mathematics, a Set (mathematics), set ''A'' is a subset of a set ''B'' if all Element (mathematics), elements of ''A'' are also elements of ''B''; ''B'' is then a superset of ''A''. It is possible for ''A'' and ''B'' to be equal; if they a ...
of every member # (\forall x \in u) (\mathcal(x) \in u): it contains the
powerset In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
of every member # (\forall x \subseteq u) (, x, < , u, \to x \in u): it contains every subset of itself that has smaller
cardinality The thumb is the first digit of the hand, next to the index finger. When a person is standing in the medical anatomical position (where the palm is facing to the front), the thumb is the outermost digit. The Medical Latin English noun for thum ...
More formally: :\forall s \exists u x, < , u, \to x \in u)/math> where , \cdot, denotes the
cardinality The thumb is the first digit of the hand, next to the index finger. When a person is standing in the medical anatomical position (where the palm is facing to the front), the thumb is the outermost digit. The Medical Latin English noun for thum ...
of a set. In short, Tarski's axiom states that every set belongs to a Tarski universe. If a Tarski universe is transitive, it is also a
Grothendieck universe In mathematics, a Grothendieck universe is a set ''U'' with the following properties: # If ''x'' is an element of ''U'' and if ''y'' is an element of ''x'', then ''y'' is also an element of ''U''. (''U'' is a transitive set.) # If ''x'' and ''y'' ...
. Conversely, assuming the
axiom of choice In mathematics, the axiom of choice, abbreviated AC or AoC, is an axiom of set theory. Informally put, the axiom of choice says that given any collection of non-empty sets, it is possible to construct a new set by choosing one element from e ...
, every Grothendieck universe is a Tarski universe (i.e. satisfies Tarski's axiom). That u looks much like a “universal set” for s – it not only has as members the powerset of s, and all subsets of s, it also has the powerset of that powerset and so on – its members are closed under the operations of taking powerset or taking a subset. It's like a “universal set” except that of course it is not a member of itself and is not a set of all sets. That's the guaranteed universe it belongs to. And then any such u is itself a member of an even larger “almost universal set” and so on. It's an axiom that guarantees vastly more sets than ZFC does.


Implementation in the Mizar system

The Mizar language, underlying the implementation of TG and providing its logical syntax, is typed and the types are assumed to be non-empty. Hence, the theory is implicitly taken to be non-empty. The existence axioms, e.g. the existence of the unordered pair, is also implemented indirectly by the definition of term constructors. The system includes equality, the membership predicate and the following standard definitions: * Singleton: A set with one member; * Unordered pair: A set with two distinct members. \ = \; *
Ordered pair In mathematics, an ordered pair, denoted (''a'', ''b''), is a pair of objects in which their order is significant. The ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a''), unless ''a'' = ''b''. In contrast, the '' unord ...
: The set \ = (a,b) \neq (b,a); *
Subset In mathematics, a Set (mathematics), set ''A'' is a subset of a set ''B'' if all Element (mathematics), elements of ''A'' are also elements of ''B''; ''B'' is then a superset of ''A''. It is possible for ''A'' and ''B'' to be equal; if they a ...
: A set all of whose members are members of another given set; * The union of a set of sets Y: The set of all members of any member of Y.


Implementation in Metamath

The Metamath system supports arbitrary higher-order logics, but it is typically used with the "set.mm" definitions of axioms. Th
ax-groth axiom
adds Tarski's axiom, which in Metamath is defined as follows: :


See also

* Axiom of limitation of size


Notes


References

* Andreas Blass, I.M. Dimitriou, and Benedikt Löwe (2007)
Inaccessible Cardinals without the Axiom of Choice
" ''Fundamenta Mathematicae'' 194: 179-89. * *
Patrick Suppes Patrick Colonel Suppes (; March 17, 1922 – November 17, 2014) was an American philosopher who made significant contributions to philosophy of science, the theory of measurement, the foundations of quantum mechanics, decision theory, psycholog ...
(1960) ''Axiomatic Set Theory''. Van Nostrand. Dover reprint, 1972. * *


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 PlanetMath is a free content, free, collaborative, mathematics online encyclopedia. Intended to be comprehensive, the project is currently hosted by the University of Waterloo. The site is owned by a US-based nonprofit corporation, "PlanetMath.org ...
:
Tarski's Axiom
{{DEFAULTSORT:Tarski-Grothendieck set theory Systems of set theory