Grothendieck Universes

[jodmos.horon]

> Jodmos Horon wrote
>
> "I'm not really convinced that any formalisation of category
> theory or of a specialisation thereof has managed to adequately interpret ZFC."

Harvey Friedman wrote:
> Any formalization of a Grothendieck Universe should interpret ZFC. Certainly Topoi interpret WZ (weak Zermelo).
>
> References anyone?

Well, it certainly seems people do make this claim.

"Structural set [theories] — these are sets where everything is invariant under isomorphism, and where elements do not have independent existence. Sometimes set theories of this sort have been referred to as categorical set theories, but this is not strictly necessary. Examples include Lawvere's ETCS (elementary theory of the category of sets) and Shulman's SEAR (sets, elements and relations). The latter is not axiomatised as a category with certain properties, but as a three-sorted theory using the eponymous sorts. Structural set theories can be augmented with axiom schemas that make them equiconsistent with ZFC, if desired." -- David Michael Roberts on page 2 in notes on "Class forcing and topos theory", 2015-2018.

https://doi.org/10.4225/55/5b2252e3092af

I however fail to see how an elementary topos may be first-order axiomatised in the language of categories to enforce the claim that it lives in a Grothendieck universe. For a topos, one may axiomatise the claim that the powerset functor may be internalised by postulating a subobject classifier living in the topos. That's first-order in the language of categories. For Grothendieck universes, I fail to see where a similar "trick" may come into play.

This seems to be a claim that ZFC may be interpreted by structural set theories such as ECTS or SEARL augmented by axiom schemas. I just do not know of a reference where such a claim is written down and proven black on white.

Seems like the claim that the notion of Grothendieck universes may be internalised in topoi has been made or discussed here:

Christian Maurer, Universes in Topoi, 1975, in Model Theory and Topoi, LNM 445, Springer, pp.285-296.

Need to get a hold of it, though.

Jodmos Horon.