One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large categories are not even objects of the universe of discourse (though individual large categories can be considered by formulas defining their objects), and even working around that, we can't perform constructions like that of functor categories between them.

The most common way to deal with them is to wave your hands and say "universes!" which magically makes all your worries go away. (This is of course a joke, but it is generally understood that any such worrisome issues can be easily dealt with by passing to a higher universe.) I imagine in the context of proof assistants this is fairly convenient, as they generally are based on type theory which commonly have a hierarchy of universes as a built-in feature.

However many "purists" would not be content with this resolution as Grothendieck universes have strictly higher consistency strength than ZFC. There has been a fair bit of discussion in the past about whether the use of universes is ever of any real necessity, with the consensus strongly leaning towards "no" (see for instance this MO post or this one, also this one specifically about Wiles' work). Very few of these arguments however do any kind of "formal analysis" which would unambiguously remove the necessity of universes from such arguments.

I hereby ask: have there been any proposals to provide some formal tools which could transform a proof using universes into a proof in ZFC? This of course cannot be done in complete generality because ZFC+universes is not conservative over ZFC, but I could imagine some tool of this sort for uses of universes in the style of category theory.

  • 1
    $\begingroup$ A related question is: Are there any theorems which have been proven in a formal system that is not (known to be) conservative over ZFC, and where there is real doubt whether the proof works in ZFC? In other words, if someone produces such a formal tool, are there examples they can test it on? $\endgroup$
    – Will Sawin
    Commented Feb 9, 2022 at 2:06
  • 4
    $\begingroup$ I think that this is the wrong question. I think that we're seeing now that ZFC is becoming inconvenient to use when it comes to some aspects of modern mathematics; section 4 of Scholze's "etale cohomology of diamonds" is an example of exactly what mathematicians should not be being forced to waste their time on. I think Grothendieck was right and it's time to move on. Logicians may like to worry about this sort of thing, however if you are actually worried about assuming that ZFC is consistent then one might ask why you're working in ZFC in the first place. $\endgroup$ Commented Feb 11, 2022 at 6:39
  • 4
    $\begingroup$ @KevinBuzzard I don't think worrying about the consistency of ZFC is the point of the question. Rather it seems to be asking about applications of proof assistants to reverse mathematics. $\endgroup$
    – Couchy
    Commented Feb 12, 2022 at 19:12
  • 1
    $\begingroup$ @Wojowu Not really an answer, but I thought that it may be worth mentioning that I used ZFC in HOL to formalize some of the core theory about 1-categories. For example, see this link. I use the standard von Neumann hierarchy as a substitute for the Grothendieck universes. To get around the size-related difficulties, I modify the definition of a locally small category (I avoid the use of definability/reflection and other messy set-theoretic bits, but I never investigated the limits of my definitions). $\endgroup$ Commented Mar 3, 2022 at 1:22
  • 1
    $\begingroup$ @Rob Even if not for if its issues, how would Flow be relevant to the question? $\endgroup$
    – Wojowu
    Commented Mar 7, 2022 at 0:35


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.