Tarski–Grothendieck Set Theory (TG)

Origin. Alfred Tarski, "Über unerreichbare Kardinalzahlen" (Fundamenta Mathematicae 30, 1938) and "On well-ordered subsets of any set" (Fund. Math. 32, 1939), where the axiom now called Tarski's axiom A appears — a closure condition on sets, formulated for the theory of inaccessible cardinals rather than for foundations. Grothendieck introduced universes in the 1960s (SGA 4) to make category theory usable in algebraic geometry without proper-class evasions. The two are the same axiom, and the name records that they were arrived at independently. Trybulec ("Tarski–Grothendieck Set Theory", Journal of Formalized Mathematics, 1989) made it the base of Mizar; Metamath uses it too.

Models. ZFC in which every set sits inside a model of ZFC. A Grothendieck universe is a transitive set closed under pairing, union, and power set and containing ω; Tarski's axiom says every set belongs to one. What this buys is size: the category of all groups is not a proper class but a set relative to a universe, and one can quantify over it, take functor categories, and move to a larger universe when the construction outgrows the current one. It is the theory that makes "the category of all X" a legitimate object without leaving set theory.

Formalism.

Language: ∈. Same as ZFC's.

Axioms: all of ZFC, plus

Tarski's axiom A. For every set X there is a set U with: (i) X ∈ U (ii) ∀Y ∀Z (Y ∈ U ∧ Z ⊆ Y → Z ∈ U) (members' subsets are members) (iii) ∀Y (Y ∈ U → 𝒫(Y) ∈ U) (members' power sets are members) (iv) ∀Y (Y ⊆ U → Y ≈ U ∨ Y ∈ U) (subsets of U are members or equinumerous with U)

where ≈ is equinumerosity. Clause (iv) is the inaccessibility condition: a subset of U is either a member or as big as U, so U is not the union of fewer, smaller pieces.

Grothendieck universes: a set U that is transitive, contains ω, and is closed under 𝒫, pairing, and indexed unions (⋃_{i∈I} xᵢ ∈ U whenever I ∈ U and each xᵢ ∈ U). A transitive Tarski universe is a Grothendieck universe; assuming AC, every Grothendieck universe satisfies Tarski's axiom for its members. The two notions coincide in practice.

Strength, stated exactly: Tarski's axiom implies the axioms of choice, infinity, and power set — so TG can be presented over ZF, or over less. Over ZFC, Tarski's axiom is equivalent to "there is a proper class of strongly inaccessible cardinals". Not equiconsistent — equivalent. The universes are precisely the V_κ for κ inaccessible (plus V_ω). TG is therefore a non-conservative extension of ZFC: it proves Con(ZFC), and by Gödel's second theorem ZFC does not.

What it does: For any set X, the universe U ∋ X is a model of ZFC containing X. So "the category of all groups in U" is a set; a functor category between U-small categories is a set in the next universe; the hierarchy of universes never runs out. Grothendieck's own use in SGA 4: sheaf cohomology on sites requires the category of presheaves, which requires the source category to be small relative to something.

Alternatives: NBG or MK — make classes objects; adequate for one level of largeness, awkward for functor categories on class-sized categories. See Class Theories. Feferman's system, and the reflection-based approaches, which get most of the effect conservatively over ZFC — the standard rejoinder that universes are more than the mathematics needs. ETCS or a topos-theoretic base, which relocate the question. See ETCS.

Symbols.

Metatheory. The equivalence over ZFC with a proper class of inaccessibles is the whole of TG's metatheory and the whole of the argument about it. Because the relation is equivalence rather than equiconsistency, TG is not a bookkeeping device: it proves Con(ZFC), and adopting it is adopting a large cardinal axiom, whatever the motive. Whether category theory needs this is the standing dispute — Feferman's reflection-based systems recover most working practice conservatively over ZFC, and the observation that Grothendieck reached for universes because they were convenient rather than because a theorem required them is the strongest form of the objection. The counter-observation is that TG's inaccessibles are at the very bottom of the large cardinal hierarchy and that no one has produced a mathematical statement whose proof in TG resists elimination and whose interest survives the elimination. Neither side is settled by a theorem.

Applies to. Category theory and homological algebra, where "the category of all X" is the construction that requires it — SGA 4, and the standard treatments of derived categories and stacks. Formal verification: Mizar's entire library is developed in TG, and Metamath offers it. Algebraic geometry, through Grothendieck's own use. The size problem generally, as the maximal-ontology option alongside NBG's classes and Feferman's reflection. Large cardinals at the inaccessible level, where TG is the working presentation.

Limitations. Not conservative over ZFC — TG proves Con(ZFC), so its consistency is not available from ZFC and the extra strength is real, not notational. For most of what category theorists actually do, universes are eliminable, and that they are convenient is not an argument that they are necessary; the reflection-based alternatives make this concrete. Tarski's axiom as stated is opaque — clause (iv) is inaccessibility in disguise, and nobody reads it that way without being told. The Mizar formulation carries its own commitments (a typed language with non-empty types), so "Mizar uses TG" describes an implementation, not a neutral endorsement of the theory.

© 2026 Lingenic LLC