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 a ...
and
Alexander Grothendieck) is an
axiomatic set theory
Set theory is the branch of mathematical logic that studies 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 mathematics, is mostly concer ...
. It is a
non-conservative extension In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory. Similarly, a non-conservative extension is a superthe ...
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 such a ...
(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
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'' a ...
it belongs to (see below). Tarski's axiom implies the existence of
inaccessible cardinal
In set theory, an uncountable cardinal is inaccessible if it cannot be obtained from smaller cardinals by the usual operations of cardinal arithmetic. More precisely, a cardinal is strongly inaccessible if it is uncountable, it is not a sum of ...
s, providing a richer
ontology
In metaphysics, ontology is the philosophical study of being, as well as related concepts such as existence, becoming, and reality.
Ontology addresses questions like how entities are grouped into categories and which of these entities ex ...
than ZFC. For example, adding this axiom supports
category theory
Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cate ...
.
The
Mizar system
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used i ...
and
Metamath
Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in ...
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 such a ...
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 f ...
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 definiti ...
s, and notation of Mizar to describe it. Mizar's basic objects and processes are fully
formal; 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
In metaphysics, ontology is the philosophical study of being, as well as related concepts such as existence, becoming, and reality.
Ontology addresses questions like how entities are grouped into categories and which of these entities ex ...
as
ZFC).
*
Axiom of extensionality
In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo–Fraenkel set theory. It says that sets having the same eleme ...
: 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 non-empty set ''A'' contains an element that is disjoint from ''A''. In first-order logic, the ax ...
: 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 schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite ...
: Let the
domain
Domain may refer to:
Mathematics
*Domain of a function, the set of input values for which the (total) function is defined
** Domain of definition of a partial function
** Natural domain of a partial function
** Domain of holomorphy of a function
* ...
of the
class function
In mathematics, especially in the fields of group theory and representation theory of groups, a class function is a function on a group ''G'' that is constant on the conjugacy classes of ''G''. In other words, it is invariant under the conjugat ...
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 that which is boundless, endless, or larger than any natural number. It is often denoted by the infinity symbol .
Since the time of the ancient Greeks, the philosophical nature of infinity was the subject of many discussions am ...
,
choice
A choice is the range of different things from which a being can choose. The arrival at a choice may incorporate motivators and models. For example, a traveler might choose a route for a journey based on the preference of arriving at a give ...
, 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 p ...
. It also implies the existence of
inaccessible cardinal
In set theory, an uncountable cardinal is inaccessible if it cannot be obtained from smaller cardinals by the usual operations of cardinal arithmetic. More precisely, a cardinal is strongly inaccessible if it is uncountable, it is not a sum of ...
s, thanks to which the
ontology
In metaphysics, ontology is the philosophical study of being, as well as related concepts such as existence, becoming, and reality.
Ontology addresses questions like how entities are grouped into categories and which of these entities ex ...
of TG is much richer than that of conventional set theories such as
ZFC.
* Tarski's axiom (adapted from Tarski 1939
[Tarski (1939)]). For every set
, there exists a set
whose members include:
-
itself;
- every element of every member of
;
- every subset of every member of
;
- the power set of every member of
;
- every subset of
of
cardinality
In mathematics, the cardinality of a set is a measure of the number of elements of the set. For example, the set A = \ contains 3 elements, and therefore A has a cardinality of 3. Beginning in the late 19th century, this concept was generalized ...
less than that of
.
More formally:
: