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 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 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 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 ...
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 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 1939Tarski (1939)). For every set x, there exists a set y whose members include: - x itself; - every element of every member of y; - every subset of every member of y; - the power set of every member of y; - every subset of y 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 y. More formally: :\forall x \exists y \in y \land \forall z \in y(z \subseteq y \land \mathcal P(z) \subseteq y \land \mathcal P(z) \in y) \land \forall z \in \mathcal P(y) (\neg( z \approx y) \to z \in y)/math> where “\mathcal P(x)” denotes the power class of ''x'' and “\approx” denotes
equinumerosity In mathematics, two sets or classes ''A'' and ''B'' are equinumerous if there exists a one-to-one correspondence (or bijection) between them, that is, if there exists a function from ''A'' to ''B'' such that for every element ''y'' of ''B'', ...
. What Tarski's axiom states (in the vernacular) is that for each set x 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. That y looks much like a “universal set” for x – it not only has as members the powerset of x, and all subsets of x, 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
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. And then any such y is itself a member of an even larger “almost universal set” and so on. It's one of the strong cardinality axioms guaranteeing vastly more sets than one normally assumes to exist.


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 In mathematics, the empty set is the unique set having no elements; its size or cardinality (count of elements in a set) is zero. Some axiomatic set theories ensure that the empty set exists by including an axiom of empty set, while in other ...
. 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 Singleton may refer to: Sciences, technology Mathematics * Singleton (mathematics), a set with exactly one element * Singleton field, used in conformal field theory Computing * Singleton pattern, a design pattern that allows only one instance ...
: A set with one member; *
Unordered pair In mathematics, an unordered pair or pair set is a set of the form , i.e. a set having two elements ''a'' and ''b'' with no particular relation between them, where = . In contrast, an ordered pair (''a'', ''b'') has ''a'' as its first e ...
: A set with two distinct members. \ = \; *
Ordered pair In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In co ...
: The set \ = (a,b) \neq (b,a); *
Subset In mathematics, set ''A'' is a subset of a set ''B'' if all 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 are unequal, then ''A'' is a proper subset o ...
: A set all of whose members are members of another given set; * The
union Union commonly refers to: * Trade union, an organization of workers * Union (set theory), in mathematics, a fundamental operation on sets Union may also refer to: Arts and entertainment Music * Union (band), an American rock group ** ''U ...
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: ⊢ ∃y(x ∈ y ∧ ∀z ∈ y (∀w(w ⊆ z → w ∈ y) ∧ ∃w ∈ y ∀v(v ⊆ z → v ∈ w)) ∧ ∀z(z ⊆ y → (z ≈ y ∨ z ∈ y)))


See also

*
Axiom of limitation of size In set theory, the axiom of limitation of size was proposed by John von Neumann in his 1925 axiom system for sets and classes.; English translation: . It formalizes the limitation of size principle, which avoids the paradoxes encountered in ea ...


Notes


References

*
Andreas Blass Andreas Raphael Blass (born October 27, 1947) is a mathematician, currently a professor at the University of Michigan. He works in mathematical logic, particularly set theory, and theoretical computer science. Blass graduated from the University ...
, I.M. Dimitriou, and
Benedikt Löwe Benedikt Löwe (born 1972) is a German mathematician and logician working at the universities of Amsterdam, Hamburg, and Cambridge. He is known for his work on mathematical logic and the foundations of mathematics, as well as for initiating the ...
(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, psychology ...
(1960) ''Axiomatic Set Theory''. Van Nostrand. Dover reprint, 1972. * *


External links

*Trybulec, Andrzej, 1989,
Tarski–Grothendieck Set Theory
, ''Journal of Formalized Mathematics''. *
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 ...
:
Proof Explorer Home Page.
Scroll down to "Grothendieck's Axiom." *
PlanetMath PlanetMath is a free, collaborative, mathematics online 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 c ...
:
Tarski's Axiom
{{DEFAULTSORT:Tarski-Grothendieck set theory Systems of set theory