Say that "U" is the axiom that "For each set x, there exists a Grothendieck universe U such that x $\in$ U", where Grothendieck universes are defined in the usual way (or, if that's unclear, in this way). Also, say that "Ca" is the axiom that "For each cardinal κ, there is a strongly inaccessible cardinal $\lambda$ which is strictly larger than κ."
It's known that ZFC+U and ZFC+Ca are completely equivalent and prove the same sentences. A sentence is a theorem of ZFC+U iff it's a theorem of ZFC+Ca.
In addition to the above, there's also Tarski-Grothendieck set theory, which can be found here. The axioms of TG are
- The axiom stating everything is a set
- The axiom of extensionality from ZFC
- The axiom of regularity from ZFC
- The axiom of pairing from ZFC
- The axiom of union from ZFC
- The axiom schema of replacement from ZFC
- Tarski's axiom A
Tarski's axiom A states that for any set $x$, there exists a set $y$ containing, $x$ itself, every subset of every member of $y$, the power set of every member of $y$, and every subset of $y$ of cardinality less than $y$.
These three axioms from ZFC are then implied as theorems of TG:
- The axiom of infinity
- The axiom of power set
- The axiom schema of specification
- The axiom of choice
My question is as follows: is TG also completely equivalent to ZFC+U and ZFC+Ca, equivalent in the same sense that something is a theorem of TG iff it's a theorem of the other two? Is TG just an axiomatization of ZFC+U/ZFC+Ca which removes redundant axioms and allows them to just be theorems? Or is there some subtle difference between TG and ZFC+U/ZFC+Ca, in that there's some sentence which TG proves that's undecidable in ZFC+U/ZFC+Ca or vice versa?
In other words, instead of typing ZFC+Grothendieck, can I just type TG and be referencing a different axiomatization of the exact same thing?