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_n}\models$ ZFC$_n$. That is: $$\mbox{For each $n\in\mathbb{N}$, 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 "$U\models$ 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)*.

usesuniverses." I don't think he makes any claim that universes are actuallyneeded, merely that they served as a simplifying tool for introducing some large-scale concepts used in the proof. Personally, my read of that paper was as at least in part a defense of the use of unnecessarily powerful methods (with which I agree wholeheartedly). $\endgroup$28more comments