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.

  • 4
    $\begingroup$ 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. $\endgroup$ Sep 23, 2015 at 14:51
  • 4
    $\begingroup$ 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. $\endgroup$ Sep 23, 2015 at 16:07
  • 2
    $\begingroup$ 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. $\endgroup$ Sep 23, 2015 at 18:16
  • 4
    $\begingroup$ @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. $\endgroup$
    – Asaf Karagila
    Sep 23, 2015 at 19:34
  • 2
    $\begingroup$ 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.) $\endgroup$ Sep 23, 2015 at 19:40

1 Answer 1


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, here, and here, 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 due to Martin, Friedman, and others as well as some more algebraic examples due to Adrian Mathias. Replacement is also needed to show that various axioms of infinity are equivalent.

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

  • 1
    $\begingroup$ "The only way to be absolutely sure that Replacement is not needed in some argument is to check each step of the argument." - Why should we believe this? In other comments, users have pointed out theorems to the effect of if some arithmetic statement can be proved with the Axiom of Choice then it can be proved without the Axiom of Choice. Presumably something similar could hold for Replacement as well... $\endgroup$ Sep 23, 2015 at 20:59
  • 8
    $\begingroup$ @SamHopkins: Replacement is fundamentally different from Choice in this respect; Replacement increases the consistency strength of set theory but Choice does not. In particular, assuming Z is consistent, then there are arithmetic consequences of ZF that are not consequences of Z (such as the consistency of Z). In fact, it is consistent that ZF is inconsistent but Z is consistent, so you can (consistently) take the arithmetic consequence to be any arithmetic statement not provable in Z. $\endgroup$ Sep 23, 2015 at 21:31
  • 1
    $\begingroup$ Can you give any example of a theorem in ordinary mathematics outside set theory and higher logic whose natural proof uses something beyond ZFC plus bounded replacement ("∀x∈S ∃!y ( Q(x,y) ) ⇒ ∃T ∀x∈S ∃!y∈T ( Q(x,y) )" for each predicate Q whose quantifiers are all bounded)? $\endgroup$
    – user21820
    Jul 20, 2020 at 14:52
  • $\begingroup$ I guess I'll assume the answer to my question is "no", since no example has been found for more than a year? =) $\endgroup$
    – user21820
    Jan 22, 2022 at 16:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.