nLab
TarskiGrothendieck set theory
Contents
Context
Foundations
foundations
The basis of it all

mathematical logic

deduction system, natural deduction, sequent calculus, lambdacalculus, judgment

type theory, simple type theory, dependent type theory

collection, object, type, term, set, element

equality, judgmental equality, typal equality

universe, size issues

higherorder logic
Set theory
Foundational axioms
Removing axioms
Contents
Idea
TarskiGrothendieck set theory is an axiomatic set theory whose axioms are thos of ZFC plus the axiom that every set belongs to some Grothendieck universe.
This framework is standard in the works of Alexander Grothendieck and his school.
References
The notion first appeared in:
 Alfred Tarski, On wellordered subsets of any set, Fundamenta Mathematicae 32 (1939) 176–183,pdf
See also
Last revised on May 9, 2023 at 12:46:56.
See the history of this page for a list of all contributions to it.