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
, 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 be the set
. 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
(the values of
for all members
of
) 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
, there exists a set
(a "universe") such that
#
: it contains
#
: 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
#
: 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
#
: 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:
: