Tarski-Grothendieck set theory
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. 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
.
s and definition
s defining Mizar's basic objects and processes are fully formal
, they are described informally below.
TG includes the following standard definitions:
Definitional axiom:
TG includes the following axioms, which are conventional because also part of ZFC:
Tarski's axiom (adapted from Tarski 1939). For every set
, there exists a set 
whose members include:
More formally: or
where "P(x)" denotes the power class of x and "≈" denotes equinumerosity
.
What Tarski's axiom states (in the vernacular) for each set
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 cardinal
s, thanks to which the ontology
of TG is much richer than that of conventional set theories such as ZFC.
Mizar system
The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...
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
Zermelo–Fraenkel set theory
In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
. Tarski–Grothendieck set theory is named after mathematicians Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
and Alexander Grothendieck
Alexander Grothendieck
Alexander Grothendieck is a mathematician and the central figure behind the creation of the modern theory of algebraic geometry. His research program vastly extended the scope of the field, incorporating major elements of commutative algebra, homological algebra, sheaf theory, and category theory...
.
Axioms
While the axiomAxiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s and definition
Definition
A definition is a passage that explains the meaning of a term , or a type of thing. The term to be defined is the definiendum. A term may have many different senses or meanings...
s defining Mizar's basic objects and processes are fully formal
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
, 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.
; - Ordered pairOrdered pairIn mathematics, an ordered pair is a pair of mathematical objects. In the ordered pair , the object a is called the first entry, and the object b the second entry of the pair...
: The set
; - SubsetSubsetIn mathematics, especially in set theory, a set A is a subset of a set B if A is "contained" inside B. A and B may coincide. The relationship of one set being a subset of another is called inclusion or sometimes containment...
: A set all of whose members are members of another given set; - The unionUnion (set theory)In set theory, the union of a collection of sets is the set of all distinct elements in the collection. The union of a collection of sets S_1, S_2, S_3, \dots , S_n\,\! gives a set S_1 \cup S_2 \cup S_3 \cup \dots \cup S_n.- Definition :...
of a family of sets
: The set of all members of every member of 
.
Definitional axiom:
- Given any set
, the singleton 
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 ontologyOntologyOntology is the philosophical study of the nature of being, existence or reality as such, as well as the basic categories of being and their relations...
as ZFC). - ExtensionalityExtensionalityIn logic, extensionality, or extensional equality refers to principles that judge objects to be equal if they have the same external properties...
axiom: Two sets are identical if they have the same members. - Axiom of regularityAxiom of regularityIn mathematics, the axiom of regularity is one of the axioms of Zermelo-Fraenkel set theory and was introduced by...
: No set is a member of itself, and circular chains of membership are impossible. - Axiom schema of replacementAxiom schema of replacementIn set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory that asserts that the image of any set under any definable mapping is also a set...
: Let the domainDomain (mathematics)In mathematics, the domain of definition or simply the domain of a function is the set of "input" or argument values for which the function is defined...
of the functionFunction (mathematics)In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
be the set 
. Then the rangeRange (mathematics)In mathematics, the range of a function refers to either the codomain or the image of the function, depending upon usage. This ambiguity is illustrated by the function f that maps real numbers to real numbers with f = x^2. Some books say that range of this function is its codomain, the set of all...
of
(the values of 
for all members 
of 
) is also a set.
Tarski's axiom (adapted from Tarski 1939). For every set
, there exists a set whose members include:
itself;- every subset of every member of
; - the power set of every member of
; - every subset of
of cardinality less than that of 
.
More formally: or
where "P(x)" denotes the power class of x and "≈" denotes equinumerosity
Equinumerosity
In mathematics, two sets are equinumerous if they have the same cardinality, i.e., if there exists a bijection f : A → B for sets A and B. This is usually denoted A \approx B \, or A \sim B....
.
What Tarski's axiom states (in the vernacular) for each set
there is a Grothendieck universeGrothendieck 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...
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
Axiom of infinity
In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of infinity is one of the axioms of Zermelo-Fraenkel set theory...
, choice, and power set
Axiom of power set
In mathematics, the axiom of power set is one of the Zermelo–Fraenkel axioms of axiomatic set theory.In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:...
. It also implies the existence of inaccessible cardinal
Inaccessible cardinal
In set theory, an uncountable regular cardinal number is called weakly inaccessible if it is a weak limit cardinal, and strongly inaccessible, or just inaccessible, if it is a strong limit cardinal. Some authors do not require weakly and strongly inaccessible cardinals to be uncountable...
s, thanks to which the ontology
Ontology
Ontology is the philosophical study of the nature of being, existence or reality as such, as well as the basic categories of being and their relations...
of TG is much richer than that of conventional set theories such as ZFC.
External links
- Trybulec, Andrzej, 1989, "Tarski–Grothendieck Set Theory", Journal of Formalized Mathematics.
- MetamathMetamathMetamath is a computer-assisted proof checker. It has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas...
: "Proof Explorer Home Page." Scroll down to "Grothendieck's Axiom." - PlanetMathPlanetMathPlanetMath is a free, collaborative, online mathematics encyclopedia. The emphasis is on rigour, openness, pedagogy, real-time content, interlinked content, and also community of about 24,000 people with various maths interests. Intended to be comprehensive, the project is hosted by the Digital...
: "Tarski's Axiom"