Otdfbt

I recently learned that some parts of SGA require axioms beyond ZFC. I am just a simple algebraic geometer so I am trying to understand how can this fact impact my life (you may have engaged in a similar game with the axiom of choice at some point of your mathematical career). I think this was only needed in the volume developing cohomology of topoi, correct me if I am wrong.

The question: is there some statement about schemes not involving the word "topoi" that you know how prove using the additional axioms, but do not know how to prove without them? I believe this question has nothing to do with the notion of completeness in mathematical logic (because I am not asking if something can be proved in principle, just if there is an obvious argument). If there is some logical argument showing that the answer is negative, I would like to learn about that too.

Bonus points if the proof of the statement in your answer relies on a Weil cohomology theory, rather than something random (I do not know if this is even possible). To be more precise, a Weil cohomology theory is only defined for smooth projective schemes over a field, for which all of this should probably be irrelevant, so I mean that the cohomology theory you use restricts to a Weil cohomology theory for smooth projective schemes over a field.

P.S. There was similar discussion in the context of Fermat's theorem, and if I understand correctly, the user BCnrd insists that universes are useless for etale cohomology without giving a reference. I believe there are few people on this planet who know etale cohomology better than BCnrd so that's some useful information. The question is not, however, limited to etale cohomology.

It's inherently difficult to give a negative answer to a question like this, but here's a technical fact that pushes in that direction:

Let ZFC$_n$ be the subtheory of ZFC gotten by restricting Separation and Replacement to $Sigma_n$ formulas. By the reflection principle,$^1$ for each $n$ the theory ZFC proves that there is an ordinal $alpha_n$ such that $V_alpha_nmodels$ ZFC$_n$. That is: $$mboxFor each $ninmathbbN$, ZFC proves Con(ZFC$_n$).$$

We can think of the $V_alpha_n$s as "approximate universes" which behave like universes for all "sufficiently simple" formulas, the point being that if you specify a complexity level ahead of time you can always assume you have an approximate universe appropriate to that complexity level.

Now the compactness theorem now naively suggests that - since we can only ever use finitely many sentences in a given proof - any argument with universes whatsoever can be replaced with one involving just approximate universes, and hence a proof in ZFC. This is of course false, but counterexamples have to be "global" as opposed to "local" - they need to at some point refer to the whole of the universe in question as a single completed object.

For exampe, the way ZFC + universes proves the consistency of ZFC is by showing that a universe $U$ is a model of ZFC. The statement "$Umodels$ ZFC" is expressed in the language of set theory by talking about Skolem functions over $U$ (or something morally equivalent), and this takes place in the context of the powerset of $U$. But this sort of thing isn't to my knowledge how universes are applied in algebraic geometry - they instead use a universe to argue that a "sufficiently closed" object exists in that universe, and this "local" argument is exactly the sort of thing that the reflection principle tells us can generally be reduced to ZFC alone.

Basically, a candidate example needs to not just take place inside a universe, but rather over a universe.

That said, there is an obvious place to look for such: arguments using two (or $n$) universes. The larger universe does see the smaller universe as a completed object, so the coarse heuristic above suggests that we can replace only the larger universe with an approximate universe - that is, that arguments which are quickly phrased in terms of two universes can be directly translated to arguments involving only one universe. Now we can't cheat anymore - we nee actual arguments about algebraic geometry. My understanding is that we're still in a situation where universes are an unnecessary convenience, but now I'm far outside of my area of competence. Still, the above should give an indication of why a real essential use of universes in a concrete result (which will certainly only involve reference to a small fragment of the cumulative hierarchy) would be very surprising.

$^1$OK fine, the reflection principle is usually phrased for finite subtheories of ZFC. But $(i)$ that's not really any different as far as the heuristic is concerned, just more annoying to work with; and $(ii)$ the stronger version of reflection I've stated is also true (the point being that for each $n$, the schemes of $Sigma_n$-Separation and -Replacement can be expressed in the language of set theory by a single sentence, which in turn can be proved from finitely many of the ZFC axioms which we can bash with the usual reflection hammer).

And on that note, it's worth pointing out two facts about reflection which help flesh out the picture:

• First, given that ZFC proves the compactness theorem, we seem to be in tension with Godel's incompleteness theorem. What saves us is that "$forall n$" and "ZFC proves" don't commute (unless ZFC is inconsistent of course): while ZFC does prove each specific instance of reflection, it can't prove the full version (unless, again, it's inconsistent).




• It's also worth noting that a similar result holds for (first-order) Peano arithmetic (as does the analogous version of the previous bulletpoint), although of course we need to talk about mere consistent Henkinized complete theories as opposed to canonical-ish models. As a cute consequence, Kripke used this fact to give a purely model-theoretic proof of Godel's incompleteness theorem (in the absence of reflection, his argument would require the soundness of PA, similarly to how Godel's original argument assumed $omega$-consistency rather than mere consistency).

Tim Chow drew my attention to this thread, and asked if I cared to comment. Actually I wrote up a detailed version of my thoughts several years ago, and to my surprise, Solomon Feferman thought enough of it for that to appear in "What is Category Theory". Their website has disappeared, so here is the version I found in my back-ups.

As a homotopy theorist, I have no idea of what is need for Wiles' proof of FLT, or what is used in EGA or SGA. For homotopy theory, the crux of the matter comes down to two things. First, we construct towers iteratively (potentially of transfinite length) and then take its limit or colimit. This assumes that the whole tower is small, while all we know is that the length is small. This is an implicit use of replacement. [Granted, if the iterative step is predicative, ZFC is enough. But see the next paragraph] The earliest use of this I know of is the proof of Brown Representability Theorem dating back 1960. I recall the same kind of argument somewhere in Neeman's book on triangulated categories. So may be it also needed for derived categories.

Another similar situation: I have a functor F and a small subcategory D of the domain of F. I want to know that F(D) is small so that I can talk about its limit/colimit. This already happens with the Milnor short exact sequence for arbitrary generalized cohomology theories [and can enter into play when studying generalized cohomology of infinite dimensional spaces such as classifying spaces of groups.] If F is itself constructed as the (co)limit of a tower constructed by transfinite induction, trying to stay within ZFC proper is not trivial.

People seem to get hung up on indexed categories (just use fibered categories all the time) and functor categories. But there is another use of universes that is more troublesome: Prove a theorem about small categories (or quasicategories or
Segal spaces or ...) and then apply to "the category of all spaces" (or ...). If the theorem about small categories was proved using only ZFC, then ZFC + global reflection does the trick. This was a suggestion of Feferman from the 60's, and my write-up was about getting around the second issue above. But published proofs ignore the subtleties: They implicitly assume Morse-Kelly. Then we need to invoke Grothendieck universes.

[If you don't understand the fuss in the third paragraph, think about this: $W$ is a set that satisfies all the ZFC axioms. For each natural number n, I construct an element $x_n$ of $W$. The details of the construction are hidden in a back box. Is the set $x_n$ an element of $W$? Or do you need to know the details of the construction?]