Here's a precise question. Does Wiles' proof of FLT run just fine in the set theory that logicians would perhaps call "Zermelo + choice" -- i.e. drop the axiom schema of replacement but assume the axiom of choice to make analysis work sensibly? [Wiles' proof needs some cyclic base change, which involves a lot of functional analysis, and one would imagine that one needs enough AC to make this stuff go through, but my question is not about AC. I am also aware that there are theorems in logic of the form "if a statement has some properties and it is provable in ZFC then it's provable in certain other systems", but my question is not about the truth or provability of FLT in Z+AC, it's about whether Wiles' proof works].


My understanding of some justifications for including replacement: without it you can't construct the ordinal $\omega+\omega$, or the cardinal $\aleph\_\omega$. But I am not sure a number theorist would need such things. If you really need something with order-type $\omega+\omega$ you could just use $\{0,1\}\times\omega$ with some lexicographic ordering, and $\aleph\_\omega$ itself is not something I've ever seen in a number theory paper.


Of course Wiles' proof uses a lot of commutative algebra, directly or indirectly, and I do remember a proof in Matsumura's commutative algebra book that uses induction over ordinals, but if I remember correctly the induction was only needed in situations where some module was massively infinitely-generated over some ring.


Maybe Wiles' proof of FLT is asking too much -- what about something less technical, like Gross-Zagier or some other random thing? I'm sure people realise what I'm trying to ask -- take a "standard" result in "standard" number theory -- does one need Replacement? I'm not interested in statements about things that logicians might have constructed (for example [Goodstein sequences](https://en.wikipedia.org/wiki/Goodstein%27s_theorem)) that they may perhaps argue are "number theoretic" -- I know something about these things and they are interesting, but this question is not about them. I want to focus on standard well-known theorems in mainstream number theory from the last 50 years or whatever. Perhaps another reason to shy away from FLT is that on the face of it it uses some category theory and there was a certain amount of fuss in the 1990s about whether the proof actually was a ZFC proof [conclusion: it was, although it undoubtedly used references which talked about subtle constructions in very large categories so some rewriting would be necessary to stuff it in.]


The reason I ask is that I have it in my head (perhaps I read it in a paper by Adrian Mathias) that Bourbaki don't assume replacement in their treatise, and I remember at the time thinking "oh wow that's crazy, what an omission" but now having actually used Bourbaki as a reference for various facts in e.g. representation theory and analysis, and having begun to comprehend just how far they get and how much further they could have got, I am now wondering how important replacement is outside logic and neighboring areas.



Is the axiom schema of replacement used in algebraic number theory (or more generally outside logic)
At eric's request, I am expanding my comment into an answer.


If we set aside specific theorems in algebraic number theory for the moment, the question of whether Replacement is used in "ordinary mathematics" has come up on MO before, e.g.,
[here](https://mathoverflow.net/questions/121406/where-in-ordinary-math-do-we-need-unbounded-separation-and-replacement), [here](https://mathoverflow.net/questions/41118/axiom-of-replacement-in-category-theory), and [here](https://mathoverflow.net/questions/208711/who-needs-replacement-anyway), and it also surfaces on the Foundations of Mathematics mailing list from time to time. There is a relatively short list of known examples outside of set theory where Replacement is provably necessary. These include some [theorems about Borel sets](http://www.cs.nyu.edu/pipermail/fom/2006-February/010013.html) due to Martin, Friedman, and others as well as some more [algebraic examples](http://www.cs.nyu.edu/pipermail/fom/2010-January/014362.html) due to Adrian Mathias. Replacement is also needed to show that [various axioms of infinity are equivalent](http://www.cs.nyu.edu/pipermail/fom/2010-January/014354.html).


Now, if we lower the bar and declare that an argument "uses" Replacement if its most natural and direct interpretation invokes Replacement, then [it can be argued](http://www.cs.nyu.edu/pipermail/fom/2007-September/011909.html) that there are many such examples in ordinary mathematics. However, many of these arguments can in principle be reformulated using a combination of powerset and separation. So they do not "use" Replacement in the strongest sense that the theorems are unprovable without it.


Returning to number theory, the only way to be absolutely sure that Replacement is not needed in some argument is to check each step of the argument. However, given that provable uses of Replacement outside of set theory are so rare, it would be surprising if any "ordinary" theorem such as the ones you mentioned requires Replacement in a strong sense.


