I was reading that the universes which we now call "Grothendieck universes" were introduced by Grothendieck in order to avoid proper classes; from Grothendieck universe on Wikipedia:
The idea of universes is due to Alexander Grothendieck, who used them as a way of avoiding proper classes in algebraic geometry.
Now, the existence of such universes is axiomatized formally by Tarski's axiom in Tarski–Grothendieck set theory:
For every set $x$, there exists a set $y$ whose members include:
$x$ itself;
every subset of every member of $y$;
the power set of every member of $y$;
every subset of $y$ of cardinality less than that of $y$.
However, I was wondering, when Grothendieck initially introduced these universes:
- was he working in a formal theory, such as $\mathsf{ZFC}$, which he found insufficient and decided to augment with an axiom similar to Tarski's?
- or, was he working in naive set theory, which he nevertheless found to be insufficient for his purposes (perhaps thinking the existence of these sets was not guaranteed by intuition)?
I did some searching, but having not thoroughly combed the literature, I was not able to find the source(s) where he introduced universes; references are welcome.
