Metamath Proof Explorer


Here we introduce Tarski-Grothendieck (TG) set theory, named after mathematicians Alfred Tarski and Alexander Grothendieck. TG theory extends ZFC with the TG Axiom ax-groth, which states that for every set there is an inaccessible cardinal such that is not in . The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics."

We first introduce the concept of inaccessibles, including weakly and strongly inaccessible cardinals (df-wina and df-ina respectively ), Tarski classes (df-tsk), and Grothendieck universes (df-gru). We then introduce the Tarski's axiom ax-groth and prove various properties from that.

  1. Inaccessibles
    1. Weakly and strongly inaccessible cardinals
    2. Weak universes
    3. Tarski classes
    4. Grothendieck universes
  2. ZFC Set Theory plus the Tarski-Grothendieck Axiom
    1. Introduce the Tarski-Grothendieck Axiom
    2. Tarski map function