[FOM] Shinichi Mochizuki on set-theoretical/foundational issues

[William Messing]

I think that Mochizuki is using the term set-theoretic universe in the 
precise sense of a Grothendieck universe, as defined in SGA 4, Expose I 
(appendix), that is in Bourbaki's set theory (as the appendix is written 
by Bourbaki) which is ZF without the axiom of foundations, but with the 
axiom of global choice, defined via Hilbert's epsilon symbol, called by 
Boubaki \tau.  Note explicitly that in expose I, ¶1, in addition to the 
standard axiom, (UA): every set is an element of an universe, a second 
axiom, (UB): if U is an universe, R{x} is  a formula and there exists an 
y\in U satisfying R{y}, then \tau_x(R{x}) is an element of U, is 
assumed.  This is used, among other things, to rigourously define the 
Yoneda embedding of an U-category, C, into the category C^ of U-valued 
presheaves on C.

William Messing