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.

generaltheory of cohomology onalltopoi, 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. $\endgroup$6more comments