Tarski–Grothendieck set theory (TG, named after mathematicians Alfred Tarski and Alexander Grothendieck) is an axiomatic set theory.
Tarski's axiom implies the existence of inaccessible cardinals, providing a richer ontology than ZFC.
For example, adding this axiom supports category theory.
The Mizar system and Metamath use Tarski–Grothendieck set theory for formal verification of proofs.
Mizar's basic objects and processes are fully formal; they are described informally below.
First, let us assume that: TG includes the following axioms, which are conventional because they are also part of ZFC: It is Tarski's axiom that distinguishes TG from other axiomatic set theories.
[4][5] It also implies the existence of inaccessible cardinals, thanks to which the ontology of TG is much richer than that of conventional set theories such as ZFC.
It's an axiom that guarantees vastly more sets than ZFC does.
The system includes equality, the membership predicate and the following standard definitions: The Metamath system supports arbitrary higher-order logics, but it is typically used with the "set.mm" definitions of axioms.