77

In a recent issue of New Scientist (16 Aug 2010), I was surprised to read that a part of Wiles' proof of Taniyama-Shimura conjecture relies on inaccessible cardinals.

Here's the article

Here's the relevant bit from the article:

"Large cardinals have been studied by logicians for a century, but their intangibility means they have seldom featured in mainstream mathematics. A notable exception is the most celebrated result of recent years, the proof of Fermat's last theorem by the British mathematician Andrew Wiles in 1994 [...] To complete his proof, Wiles assumed the existence of a type of large cardinal known as an inaccessible cardinal, technically overstepping the bounds of conventional arithmetic"

Is this true ? If so, could someone please outline how they are used ?

David Roberts
  • 33,851
Cosmonut
  • 1,041
  • 34
    No, completely false. Perhaps the author (whose mathematical training seems to be far from number theory) has misunderstood or misheard descriptions of parts of the argument. – BCnrd Aug 16 '10 at 11:12
  • 4
    Wiles's paper http://www.jstor.org/stable/2118559 makes no mention of inacessible cardinals. – Robin Chapman Aug 16 '10 at 11:13
  • 20
    Does any part of Wiles' proof or general results he may rely on make use of Grothendieck universes? The existence of these is equivalent to the existence of an inaccessible cardinal. – Joel David Hamkins Aug 16 '10 at 11:20
  • 11
    Dear Joel: Nope. – BCnrd Aug 16 '10 at 11:41
  • 50
    Actually, Cosmonut misquoted the article by leaving out the rest of the statement: "But there is a general consensus among mathematicians that this was just a convenient short cut rather than a logical necessity. With a little work, Wiles's proof should be translatable into Peano arithmetic or some slight extension of it." – JS Milne Aug 16 '10 at 13:41
  • 25
    The Stack Project develops a huge amount of Grothendieck style mathematics, including a lot of etale cohomology, using only ZFC (specifically, NOT using universes). If anyone has any doubt that this can be done, I suggest that they look at it. – JS Milne Aug 16 '10 at 18:48
  • 6
    I am a bit puzzled why this has now accumulated 2 votes to close (since I can't see the reasons selected by those who voted). – Yemon Choi Aug 16 '10 at 22:25
  • 5
    Why did Grothendieck introduce his Universes Axiom? – Pierre-Yves Gaillard Aug 17 '10 at 05:18
  • 20
    Dear Pierre: if one wants to write a treatise on a general theory of cohomology on all topoi, including operations like sheafification, enough injectives, derived categories, and Ext-sheaves, there needs to be a way to control the "size" of coverings which arise in these constructions (to replace the implicit role of "power set" for ordinary topology spaces). The universe stuff takes care of such matters in an elegant way, so one can focus attention on the more central aspects of the theory. – BCnrd Aug 17 '10 at 05:43
  • 2
    Dear BCnrd: Thanks a lot for your answer! Is proving FLT without universes a little bit like proving the PNT without complex analysis? – Pierre-Yves Gaillard Aug 17 '10 at 06:51
  • 14
    Dear Pierre: No. Universes have as much relevance to proof of FLT as general theory of derived categories does to finite-dim'l linear alg (i.e., no relevance). Just because certain theories (derived categories, topoi, etc.) are documented in one reference in hyper-general form using concept X doesn't imply that applications of those theories logically depend on X: there may be other ways to develop the theory (with a bit less generality), even documented in the literature, which suffice for applications of interest. Everything on this page is like a fog as far as proof of FLT is concerned. – BCnrd Aug 17 '10 at 12:14

5 Answers5

85

The basic contention here is that Wiles' work uses cohomology of sheaves on certain Grothendieck topologies, the general theory of which was first developed in Grothendieck's SGAIV and which requires the existence of an uncountable Grothendieck universe. It has since been clarified that the existence of such a thing is equivalent to the existence of an inaccessible cardinal, and that this existence -- or even the consistency of the existence of an inaccessible cardinal! -- cannot be proved from ZFC alone, assuming that ZFC is consistent.

Many working arithmetic and algebraic geometers however take it as an article of faith that in any use of Grothendieck cohomology theories to solve a "reasonable problem", the appeal to the universe axiom can be bypassed. Doubtless this faith is predicated on abetted by the fact that most arithmetic and algebraic geometers (present company included) are not really conversant or willing to wade into the intricacies of set theory. I have not really thought about such things myself so have no independent opinion, but I have heard from one or two mathematicians that I respect that removing this set-theoretic edifice is not as straightforward as one might think. (Added: here I meant removing it from general constructions, not just from applications to some particular number-theoretic result. And I wasn't thinking solely about the small etale site -- see e.g. the comments on crystalline stuff below.)

Here is an article which gives more details on the matter:

  • Colin McLarty, What does it take to prove Fermat’s last theorem? Grothendieck and the logic of number theory, Bull. Symb. Log. 16 No. 3 (2010) pp. 359–377, doi:10.2178/bsl/1286284558, archived author pdf.

Note that I do not necessarily endorse the claims in this article, although I think there is something to the idea that written work by number theorists and algebraic geometers usually does not discuss what set-theoretic assumptions are necessary for the results to hold, so that when a generic mathematician tries to trace this back through standard references, there may seem to be at least an apparent dependency on Grothendieck universes.

P.S.: If a mathematician of the caliber of Y.I. Manin made a point of asking in public whether the proof of the Weil conjectures depends in some essential way on inaccessible cardinals, is this not a sign that "Of course not; don't be stupid" may not be the most helpful reply?

David Roberts
  • 33,851
Pete L. Clark
  • 64,763
  • 43
    For etale cohomology all of that universe stuff is entirely irrelevant. I say this not as an "article of faith", but because I've read all of the proofs of the theorems of etale cohomology. Perhaps if one wants to make a super-general theory of cohomology for "all" topoi there are these problems, but if one only cares about more "real" examples such as etale cohomology then there are no issues. – BCnrd Aug 16 '10 at 11:38
  • 1
    @B: Obviously when I refer to workers in the field taking things on faith, I didn't mean you! On the other hand, I seem to recall you telling me a while ago (i.e., about ten years) that there were some issues as above with the crystalline site. Do you still feel that way? – Pete L. Clark Aug 16 '10 at 12:01
  • 9
    I completely agree with BCnrd opinions here but as far as I know there is no published complete proof of the relevant results that bypasses SGA IV so in that sense it is not an established fact. It is perhaps also interesting to note that (as far as I can remember) Manin poses the question on whether Deligne's proof of the Riemann hypotheses can be made independent of inaccessible cardinals in the problem list in Mathematical Developments Arising from Hilbert Problems: Proceedings (Proceedings of Symposia in Pure Mathematics, V. 28 parts 1 & 2). – Torsten Ekedahl Aug 16 '10 at 12:06
  • 3
    (cont'd) Having seen that I asked Deligne about what he thought and he agreed with me. (He also told me that he had spent some time trying to see if étale cohomology was recursively computable and had been able to conclude that with torsion coefficients it was but had been unable to get recursively computable bounds on the order of torsion in $\ell$-adic cohomology.) – Torsten Ekedahl Aug 16 '10 at 12:09
  • 13
    Section 1 of link shows the author "reasoning" about math he does not understand, and rests on the bogus argument that since there is one general reference on cohomology by Gr. written with universes, appeal to any cohomological results of Gr. has the same dependence. The result of Tate which concerns the author was inspired by Gr. duality but is just a piece of pure comm. algebra. Deligne-Rap. use Gr. duality, but Gr. duality requires no universes. (Improvements in the method removed Gr. duality, by the way.) Proofs exist to impart understanding; the author should have read some of them. – BCnrd Aug 16 '10 at 12:12
  • 1
    Just a clarification: My last comment was aimed at pointing out that there may be questions remaining about the (prooftheoretic?) complexity of étale cohomology but they lie in a completely different part of the complexity hierarchy than does dependence on inaccessible cardinals. – Torsten Ekedahl Aug 16 '10 at 12:25
  • 2
    Dear Torsten: I learned etale cohom. mainly from books of Milne and Freitag-Kiehl and later parts of SGA 4 (and some SGA 4.5 and Verdier's duality paper) which don't depend on the theory of cohomology on an arbitrary topos once one has the cohomology theory up and running from somewhere (such as the other sources). I never saw anything which required universes in that, and it gave all I needed to read Weil II. So I wonder: what specifically was Deligne agreeing with? Is there a specific example? (Etale cohom. may not be "recursively computable", but that seems to be a separate matter.) – BCnrd Aug 16 '10 at 12:26
  • 2
    Dear Pete: There remains a certain aspect of the "sheafification" process on the crystalline site that I haven't figured out how to carry out on general schemes (in a manner consistent with how the proofs of the theory work, especially a certain fiber-product construction with subrings) without the universe stuff. Some day I'll figure it out. (Torsten, do you know how to do it?) But this is exactly why I have always been careful to reject using universes in proofs of things I care about: so I'd never get dragged into concerns of the sort in the article you linked. – BCnrd Aug 16 '10 at 12:31
  • 1
    Link has W2/SGA4.5 in #7: While Deligne often uses Unis he stresses in conversation that they are a convenience technically eliminable in favor of ZFC. The theorems used in practice can always be given in terms of individual sheaves on small sites, without ever looking at whole categories of sheaves let alone categories of categories of them..This is a recipe for eliminating Unis from any use of Gr’s cohomology in NT..Though its obvious in practice that it could always be done, its not done in publications, and has never been made a precise metatheorem. Anyone interested should give it a try. – Junkie Aug 16 '10 at 12:49
  • 2
    @BCnrd: As I recall it Milne's book refers to SGA 4 at a few places. I have not read Freitag-Kiehl however. What Deligne agreed with was that the answer to Manin's problem was that inaccessible cardinals are not needed (the comment about recursivity was just to show that the concern about the use of inaccessible cardinals seems to focus on the wrong level). I am not sure which detail of the crystalline theory you are referring to (in practice it seems that at least the original crystalline theory is dealing even less with general sheaves than the étale one does). – Torsten Ekedahl Aug 16 '10 at 13:25
  • 3
    Dear Junkie: There are 2 issues. One is sheaf-theoretic and cohomological stuff on general topoi (sheafification, construction of enough injectives, making Hom between two sheaves into a set, etc.). For real examples like small etale site, Berkovich etale cohom, etc., no need for metathm or "elimination recipe" if one pays attention to it when reading all proofs. The 2nd issue is univ. mapping properties on "entire category" (your comment about "whole categories of sheaves"). That's an issue for category theory in general, not just SGA; handled as for flatness against "all" mods over a ring. – BCnrd Aug 16 '10 at 13:30
  • 1
    Dear Torsten: Thanks for clarification on Deligne's comment. Milne indeed refers to SGA4 in some places. When something I wanted to understand wasn't proved in Milne's book or F-K then either relevant parts from sga4 were covered nicely in sga 4.5 or could be understood directly from SGA4 without going back into the frightening volume 1....or in some cases (like aspects of torsion Kunneth in derived categories, which is really fearsome in sga4 and whose proof in F-K is too slick because the crucial relation with cup product is omitted) it was easier to work out the proofs by oneself. – BCnrd Aug 16 '10 at 13:46
  • 3
    Dear Torsten: For the crystalline theory, the issue is to control the "size" of the nil-thickenings one allows to consider in the sheaf theory. In the etale case, by restricting to small etale site on a fixed scheme (sheaves determined by affines etale over the base) we see that Hom between sheaves is a set (so Tohoku proof of enough inj's via transfinite induction on Hom sets can be applied). For crystalline case, seek analogous "small" site for same needs (e.g., want Ext's) while also retaining a form of the crucial ring fiber product trick early in the theory. Perhaps another 550 pts... – BCnrd Aug 16 '10 at 13:57
  • 4
    Dear BCnrd, I kinda figured it was something like that. I think I'll pass on that issue until I find myself needing it. In practice crystalline cohomology seem to me to be mostly a formalism for constructing appropriate complexes of sheaves in the Zariski topology. – Torsten Ekedahl Aug 16 '10 at 14:34
  • While the last two comments (by HG and PLC) hold some amusement/interest, might I respectfully suggest they don't really belong as MO comments? – Yemon Choi Aug 16 '10 at 23:01
  • 1
    Pete and I have both removed our comments. – Harry Gindi Aug 17 '10 at 01:27
  • 2
    Unfortunately the link to the article is no longer active, and it’s no longer clear what article was linked. – Peter LeFanu Lumsdaine May 13 '19 at 15:33
  • 1
    @PeterLeFanuLumsdaine I have put in a proper reference and link, though some kind soul had added a Wayback machine link in the meantime. – David Roberts Jun 18 '21 at 13:22
  • @PeteL.Clark for what it's worth Colin McLarty has results that show not even ZFC is needed for derived functor cohomology (and he claims "all of the relevant EGA/SGA"), see the edit to my answer to this question. It's not just arguments like in the paper you link, or historical citation tracing by involved parties and special case analysis. – David Roberts Jun 18 '21 at 13:38
  • 1
    @BCnrd for what it's worth check the edit at the end of my answer for more recent developments on proving universes and indeed full ZFC unnecessary for all the relevant "large structure" technology inside SGA. – David Roberts Jun 18 '21 at 13:40
57

I'm writing a new community wiki answer because it seems to me the consensus in the comments is that the accepted answer doesn't really tell the right story, and since this is something that pops up all the time it'd be good to have a single place to point people without making them read through all the comments. Please improve my answer.

In the most naive sense Wiles proof does depend on existence of Grothendieck universes (and thus on existence of inaccessible cardinals). By this I mean if you took every reference in Wiles proof and read the first published proof of that fact you'd certainly end up somewhere in SGA where, due to Grothendieck's love of generalization, you'd find universes popping up.

However, this certainly doesn't mean the proof really uses universes. It's widely believed (though for some people this belief may not come from much direct evidence) that in any practical situation you don't actually need universes. However, there are some concrete situations (BCnrd mentions some involving sheafification on the crystalline site) where it's not necessarily known how to eliminate the use of universes.

As a result, in order to figure out if Wiles's proof uses universes, or whether it's relatively easy to avoid them, you'd need to either read the proofs yourself or find someone who was both deeply familiar with the details of the proof, and someone who cares a lot about details. One person who comes quickly to mind is BCnrd. BCnrd was one of the mathematicians who proved the Modularity Theorem, which showed that all elliptic curves over $\mathbb{Q}$ are modular. This is a strengthening of Taylor and Wiles' result, which applied only to semi-stable elliptic curves, and the proof involved understanding and building on Taylor and Wiles' work. BCnrd is also famous for his attention to detail and for consulting underlying foundational sources; he is the author of a book dedicated to simplifying and correcting the presentation of Grothendieck duality in Hartshorne's book Residues and Duality.

As explained in the comments to Pete's answer, BCnrd says there's really no issue at all in Wiles's proof. All of the specific things that Wiles uses stay far away from any of the difficult issues where you might be worried about needing to invoke universes.

BCnrd
  • 6,978
Noah Snyder
  • 27,820
  • 3
    Edited to explain BCnrd's qualifications to those who don't already know them. – David E Speyer Aug 16 '10 at 16:05
  • 2
    Note to BCnrd: It occurs to me that my edits make it trivial for someone to deduce your identity. I assume you have no intention of being genuinely anonymous but, if this bothers you, let me know and I will remove them. – David E Speyer Aug 16 '10 at 16:06
  • 9
    Dear David: No problem. Dear Noah: Nice summary. Galois repns in pf of FLT are weight 2, built via Tate mods of Jacobians (no etale cohom). The part which gets some worked up about universes is Grothendieck duality (eliminated in the subsequent generalizations and improvements of the method, FWIW), but nothing in pfs of Gr. duality leads to universes either. Someone who reads the first proofs of original refs, as you suggest (bad idea: there's been progress!), won't run into universes. Too dramatic to focus on FLT. Would be better if those who speculate on certain proofs read them first. :) – BCnrd Aug 16 '10 at 16:44
  • 6
    I agree with all of this. I think McLarty's point of view makes some sense when FLT is read as a synecdoche for "modern arithmetic geometry using Grothendieck cohomologies". I am familiar with the foundations of etale cohomology and know that universes are absolutely not required there. However, for some other sites, things are less obviously benign. For an example -- which must be close to the simplest possible example -- of set-theoretic difficulties related to nilpotent thickenings, see Section 6 of http://math.uga.edu/~pete/apoints11.pdf. – Pete L. Clark Aug 16 '10 at 17:42
33

Can I draw attention to the continuation of that quotation? "But there is a general consensus among mathematicians that this was just a convenient short cut rather than a logical necessity. With a little work, Wiles's proof should be translatable into Peano arithmetic or some slight extension of it."

For the record, McLarty's paper in the Bulletin of Symbolic Logic was indeed the source for my claim that Wiles used an inaccessible cardinal (via Universes). If anyone fancies debating the exact definition of 'using' an axiom without 'needing' it, and whether or not that definition applies in the current case, we should probably do it somewhere else (Pedantry Overflow?). But I explicitly opposed the claim that the proof 'needed' large cardinal assumptions, so I don't propose to be too apologetic.

Anyway, it's an interesting question, and I'd be pleased if my article goes some way to bringing an answer into the public domain (even if I do get my head shot off in the process ;) ).

(Incidentally I would rather have left this as a comment than an answer, but don't have enough (any) reputation points. If anyone with superpowers wants to move it, please go ahead.)

Richard Elwes
  • 331
  • 4
    Incidentally, while I strongly agree that universes are not logically necessary, it not as clear to me exactly what axiom system is necessary for Wiles's proof. (I.e., how "slight [an] extension of" Peano arithmetic, if any, is actually needed.) The reason is that Wiles, like all modern number theorists, argues in a thoroughly second order way (i.e. works with the standard model of the natural numbers, argues with subsets of such, and so on), and I don't how strong an axiom scheme is needed to translate such arguments into first order arithmetic. – Emerton Aug 16 '10 at 22:16
  • 2
    I should add that while I have some expertise in Wiles's methods, I don't have any in logic, so you shouldn't take my concerns very seriously. I do remember one conversation in the Harvard tea room with Mark Kisin and Richard Taylor in which Richard raised this question (i.e. whether FLT was proved in PA), I think because someone had asked it of him, and my memory is that no-one really knew the answer; in part because of this, I've always been a bit agnostic as to exactly what axiom scheme is really required. (Clearly much less than large cardinals, though! See also ... – Emerton Aug 16 '10 at 22:19
  • 1
    Torsten Ekedahl's comments above about whether etale cohomology can be computed in a recursive fashion; this is one way of approaching the question as to what extent modern arithmetic geometry can be developed in PA or something similar.) – Emerton Aug 16 '10 at 22:22
  • So would it be correct to say that it is unknown whether FLT is a theorem of PA? Are people interested in that? Interested enough to work on it? – Carsten S Aug 16 '10 at 23:14
  • 4
    I now seem to have magically acquired enough reputation to comment...

    Very recently I have read that Angus Macintyre has announced a proof of FLT in PA. The only reference I can provide is this: http://cameroncounts.wordpress.com/2010/01/07/mathematics-and-logic-2/

     – Richard Elwes Aug 16 '10 at 23:30
  • 6
    Richard, it is more accurate to say Macintyre announced that the proof by Wiles can be developed in PA; the way you wrote it suggests there is some other approach in PA. The blog link says the proof by Wiles follows from his work "on the equivalence of modular forms and elliptic functions". Oops! – KConrad Aug 17 '10 at 03:32
  • 4
    Ok! Try again... Macintyre has reportedly announced a proof (which I would expect to be non-trivial) that Wiles' proof can be translated into PA.

    In the intro to his forthcoming book, Boolean Relation Theory and Incompleteneess, Harvey Friedman conjectures that it should be proveable in an elementary fragment $I \Sigma_0(exp)$. This is an instance of his conjecture that "Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in elementary arithmetic."

     – Richard Elwes Aug 17 '10 at 07:05
  • Is there any news about Macintyre's proof? – Hans-Peter Stricker Jan 20 '11 at 09:02
  • 3
    I heard Angus Macintyre talk about it fairly recently. The situation is a little unusual, as to write out a proof fully would entail multiplying the (already considerable) length of Wiles' proof by 5 (or 10 or something), to reduce every single step to PA. Macintyre does not intend to do this in full completeness, but he is continuing to prepare a manuscript to show that the key pieces of higher order machinery used in the Wiles' proof can be translated into PA. The focus is on the central modularity theorem, which he will show is effectively $\Pi^0_1$, and provable in PA. – Richard Elwes Mar 21 '11 at 12:03
  • 1
    Macintyre's account appears as the appendix to Chapter 1 ("The Impact of Gödel's Incompleteness Theorems on Mathematics") of Kurt Gödel and the Foundations of Mathematics: Horizons of Truth (Cambridge University Press, 2011). – Timothy Chow Nov 22 '21 at 15:27
29

There was some discussion about this on the FOM mailing list: see for example http://cs.nyu.edu/pipermail/fom/1999-April/002983.html, where someone claimed Wiles needed in accessible cardinals, and Harvey Friedman essentially told them to stop being stupid. (Friedman is the guy who created the subject of reverse mathematics, which studies what axioms are necessary for any given result.)

An analogy would be the claim that classifying groups of order 4 needs Grothendieck universes, because groups of order 4 form a proper class, so isomorphism classes of groups of order 4 form a 2-class of classes. This is obviously silly: it is trivial to restate the classification of groups of order 4 without using proper classes, but this makes the statement slightly more complicated: you have to talk about groups that are hereditarily finite sets or something like that, which is just an irrelevant complication. The use of Grothendieck universes is similar: for example, the collection of all etale spaces over a scheme is a proper class so in some sense uses universes to construct it, but is equivalent to a much smaller set so the use of universes is not necessary.

Richard Borcherds
  • 20,442
  • 6
    The final example above highlights the distinction between working with sheaves vs. presheaves. If one wants to consider presheaves on "all" schemes etale over a base, then the set theory issues emerge (e.g., Hom of presheaves isn't a set...). But we ultimately care about the sheaf theory (= the topos), for which much smaller sites compute the topos. That's why there is no problem with the concept of an etale sheaf even on "all" schemes etale over a fixed scheme. I think Milne's book notes an example of Waterhouse that illustrates the problems that arise if one is too cavalier with presheaves. – BCnrd Aug 16 '10 at 14:11
  • 28
    An interesting historical data point on the other side of this issue is that when Solovay proved the consistency with ZF+DC that every set of reals is Lebesgue measurable, he used an inaccessible cardinal in the proof, and many researchers at that time reportedly viewed this aspect as a removable defect in the proof. But it was later proved by Shelah that an inaccessible cardinal was necessary. – Joel David Hamkins Aug 16 '10 at 14:51
  • 3
    "According to the expert, the real reason that the obvious eliminability of Universes is not frequently pointed out in the literature is just that it is so obvious. But the expert says that if there was ever a problem, then a lot of attention would then be paid to it!" – Junkie Aug 16 '10 at 16:26
16

At the suggestion of François G. Dorais I am moving this answer from Recent claim that inaccessibles are inconsistent with ZF to here. The text below was written before I read the above, very well-informed answers/comments, so there is considerable overlap.

This is just a quick answer regarding FLT, mentioned by the OP.

Colin McLarty is working on showing a small part of Friedman's grand conjecture, namely that the Fermat-Wiles(-Taylor?) theorem is provable in a weak system of arithmetic. Since originally the semi-stable case of Taniyama-Shimura-Weil that Wiles proved (not to mention the work by others such as Frey, Serre, Ribet to get to that point) required large parts of algebraic and arithmetic geometry developed by the Grothendieck school, which among other things uses sheaves, cohomology and so on, and so a priori requires some foundational care. Universes (~inaccessible cardinals) were introduced to take care of the problem of e.g. forming categories of sheaves on categories of sheaves on a site.

However, one can use a version of set theory much weaker than ZFC+Universe(s), indeed a fair bit weaker than ZFC, as McLarty has shown, and still get pretty much all of EGA/SGA (this is based on general arguments, he hasn't sat down and worked through it all). However, the arithmetic geometry needed for FLT [edit: and indeed a lot of number theory] really only needs to consider countable sites, rather than generic small sites, and so one really only needs to assume much weaker assumptions about infinite objects.

A more recent talk (July 2011 - slides not publicly available as far as I know) by McLarty had the statement that derived functor cohomology is a finitely axiomatised first-order theory, and so not really the complicated logical beast it appears to be.

EDIT: More work has been published in the meantime:

  • Colin McLarty, The large structures of Grothendieck founded on finite-order arithmetic, Rev. Symb. Log. 13 No. 2 (2020) pp. 296–325, doi:10.1017/S1755020319000340, arXiv:1102.1773

To quote from the abstract:

Such large-structure tools of cohomology as toposes and derived categories stay close to arithmetic in practice, yet existing foundations for them go beyond the strong set theory ZFC. We formalize the practical insight by founding the theorems of EGA and SGA, plus derived categories, at the level of finite order arithmetic.

Some partial results to getting to a specific finite order are in

  • Colin McLarty, Zariski cohomology in second order arithmetic, arXiv:1207.0276

The cohomology of coherent sheaves and sheaves of Abelian groups on Noetherian schemes are interpreted in second order arithmetic by means of a finiteness theorem

though the tools in that paper are insufficient to apply to étale cohomology, this means we are a long, long way from needing universes.

David Roberts
  • 33,851