# Is the axiom schema of replacement used in algebraic number theory (or more generally outside logic)

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) 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.

• I believe that many logicians expect that Wiles's proof might be undertaken in PA, which is considerably weaker than ZC in terms of arithmetic consequences. Angus MacIntyre was reportedly working on this, and some people had seen a manuscript, but I don't know the current status of this. See also Colin Mclarty's article, cwru.edu/artsci/phil/Proving_FLT.pdf. – Joel David Hamkins Sep 23 '15 at 14:51
• Definitely AC is not needed, since arithmetic truth is absolute between the full ZF universe $V$ and the constructible universe $L$, where one has ZFC. So if the proof can be undertaken in ZFC, then it can definitely be undertaken in ZF. – Joel David Hamkins Sep 23 '15 at 16:07
• The conventional wisdom is that replacement is not needed for ordinary mathematics. Often one can work around an apparent use of replacement by using powerset + separation, even if using replacement would be more "natural." Some examples of necessary uses of replacement can be found in the Foundations of Mathematics archives, e.g., cs.nyu.edu/pipermail/fom/2006-February/010013.html and cs.nyu.edu/pipermail/fom/2010-January/014362.html and cs.nyu.edu/pipermail/fom/2010-January/014354.html . As you can see, these examples are all somewhat arcane. – Timothy Chow Sep 23 '15 at 18:16
• @eric: While some choice is needed for functional analysis; for statements about integers like FLT you can avoid the axiom of choice. This had been discussed before on this site, and elsewhere. – Asaf Karagila Sep 23 '15 at 19:34
• Eric, as Asaf mentioned, my argument about AC applies to any specifically arithmetic assertion, and one can make the same conclusion about any statement of complexity up to $\Sigma^1_2$ and Boolean combinations of them. The point is that if one assumes only ZF, then the truth of the statement is absolute to the constructible universe, where ZFC holds. So if you can prove such a statement in ZFC, then it follows by this means that it is also a theorem of ZF. (I am not saying that one can easily find a direct proof in ZF, but this is a meta-theoretic proof that indeed such a proof does exist.) – Joel David Hamkins Sep 23 '15 at 19:40