Why this question on AC in proof of FLT was marked as duplicate? [closed]

Why this question was marked as duplicate of this one? The former asks if AC can be removed from Wiles's proof of FLT. The latter asks [What are some examples of theorems in number theory that require the axiom of choice or its equivalents (ie Zorn's lemma) for its proof?] I think they are totally different questions. He is asking examples of theorems in number theory which require AC. So whether FLT requires AC or not is not his main concern. This can cause a big difference between the answers for both questions. Closing the question shut out potentially good answers for it.

• (I haven't voted to close but) you're conveniently end your citation of the latter question before «Someone mentioned to me that Fermat's Last Theorem requires AC. Can someone verify this?» part. – Grigory M Dec 25 '13 at 21:06
• @GrigoryM [you're conveniently end your citation of the latter question] Hey, anybody can read the whole text of his question. – Makoto Kato Dec 25 '13 at 21:26
• It is a duplicate because Andre's answer answers your question. Because of Shoenfield's absoluteness theorem, if the statement is provable with the axiom of choice, it is provable without it. Since it is provable with the axiom of choice, essentially the use of choice can be eliminated. Do note that Wiles did not prove FLT. He proved a much stronger theorem, where I suspect the axiom of choice might not be possible to remove. If and when a proof from $\sf PA$ is found, it will be possible to conclude how will a choiceless proof should look like. But choice is not needed, as Andre indicates. – Asaf Karagila Dec 25 '13 at 22:29
• I am saying that this is quite likely. Colin McLarty, to my knowledge, worked on that sort of proof. It might be possible to prove a weaker theorem, where the only objects we care to deal with are those actually needed to prove FLT itself (after all, FLT is but a corollary). But it is most certainly that if $\sf ZFC$ (or even $\sf ZFC$ along with some large cardinal axiom) proves a first-order statement about number theory then $\sf ZF$ (with the possible large cardinal axioms) prove that statement as well. Therefore a proof that FLT is true exists from $\sf ZF$ (maybe with large cardinals). – Asaf Karagila Dec 25 '13 at 23:04
• So... once again you ask people to go through 400 pages of mathematical text, and reprove everything without using the axiom of choice? Yeah, let me notify you that your question is no longer a duplicate. It's now "Too broad". I don't mind voting to reopen in order to close it again, if you prefer. You can instead ask one of the moderators to do that directly without exhausting people with reopening and re-closing. – Asaf Karagila Dec 25 '13 at 23:38
• @MakotoKato The argument I mentioned is perfectly standard, and explains how to remove choice from any proof of FLT whatsoever, including Wiles's. – Andrés E. Caicedo Dec 25 '13 at 23:42
• Funny how this can be discussed with no problem on MathOverflow, along the lines OP is interested in, but here it is closed and gets an insulting talk about "asking people to go through 400 pages and reprove everything". @AndresCaicedo 's observation about absoluteness is relevant, but does not dispose of the question as usually understood (e.g., in McLarty's papers, or Asaf's first comment about the "much stronger theorem"), which is whether the body of more general theory Wiles relied on can be written without AC, with minimal disturbance (or close to none for the FLT argument). – zyx Dec 26 '13 at 0:33
• @zyx It is not just an issue of relevance. It is the answer to the question, as usually understood. – Andrés E. Caicedo Dec 26 '13 at 0:54
• @AndresCaicedo, it is only one answer, and not particularly the "usually understood" or most relevant one from several perspectives (some of which are illustrated by the discussion at MathOverflow, and others include the matter of provability in constructive formal systems, which are arguably a better rendition of the intention of such a question). Some of these other answers are more specific to FLT than to the general "number theory without AC" thread, and it is not presently possible to add them unless the question is re-opened. – zyx Dec 26 '13 at 1:38
• @zyx Whatever you say. – Andrés E. Caicedo Dec 26 '13 at 1:48
• (I did not mention $\mathsf{ZF}$, because the surrounding set theory is not the issue. But this is not the forum for that discussion. If the question is reopened, such technical matters should be detailed in answers.) – Andrés E. Caicedo Dec 26 '13 at 2:23
• > Colin McLarty, to my knowledge, worked on that sort of proof [one that does not prove the Taniyama-Shimura-Weil conjecture first and derive FLT as corollary.] < ---- I don't think McLarty was ever addressing this issue. It is the opposite of what he was interested in (having started from topos theory), which was whether the machinery of Grothendieck algebraic geometry requires notable amounts of set theory (such as beyond ZF, or more than PA) to set up in a generality sufficient for its storied applications like the Fermat, Weil and Mordell conjectures. – zyx Dec 26 '13 at 6:27
• I don't see how any proof using inaccessible cardinals can be acceptable to those who don't accept their existence. – dfeuer Dec 31 '13 at 5:38
• Right. It is very weird to try to wall off the matters like inaccessibles and constructive proofs (the latter would probably kill off the AC issue in multiple ways) from a question that asks about the need for an abstract existence principle like AC in a concrete problem. As often as not, people asking these questions mean to ask about the more general question but AC is the only way that they know of for such issues to present themselves. @dfeuer – zyx Dec 31 '13 at 7:35
• (This is my last comment on this thread, barring fixing minor typos. I leave it to others to flesh out the sketch or to discuss its shortcomings.) – Andrés E. Caicedo Jan 4 '14 at 6:55

I would just like to record that I'm disappointed in the way this question was handled. As zyx notes in a comment under Alex Becker's answer, there are numerous comments in this meta-thread that could have appeared as (at least partial) answers to the question proper.

Even if (in some people's view) the question admits a trivial answer, it wouldn't be the only such question on the site. Personally, though, I find the question interesting; as someone who works in the area related to Wiles's proof, it's something I think about myself from time to time.

Added: To give one concrete example of an answer to the original question:

In the paper of Taylor--Wiles, a certain "non-canonical" projective limit is taken, and it is important to show that it is non-empty (indeed, the whole proof rests on this). I remember being in the lectures at Harvard when Taylor first explained this (in the Fall of 1994), and audience members (Mazur, Serre, ... ) being shocked --- the whole thing seemed quite unnatural, and the non-emptiness was proved basically by a compactness argument (Tychonoff's theorem, if you like), which (at least naively) uses some form of choice.

This was disturbing enough to people in the field that some serious thought was given to how to eliminate this; in the standard text on the subject (Modular forms and Fermat's Last Theorem, ed. by Cornell, Silverman, and Stevens) the chapter dealing with this argument explains how to replace the projective limit and compactness argument by a concrete constructive argument that works at some (construcively determined) finite level of the projective system in play.

This reminds of various discussion Terry Tao has placed on his blog, where he explains how to go from "hard" finitistic analysis (with a lot of $\epsilon$-management) to more soft, infinitary arguments (say by applying non-standard analysis ideas), except here number theorists were going in the reverse direction, in order to convince themselves that the infinitary methods weren't really necessary.

If this kind of fuss seems strange to non-number-theorists, I should explain that for those schooled in number theory/Grothendieckian alg. geom./commutative algebra in the modern style, non-canonical infinitary constructions (that I imagine some analysts, or Ramsey-theorists, and so on, might regard as their bread-and-butter) run very much against the established cultural view as to why statements are (or should be) true. Similarly, elimination of choice simply by "reduction to $L$" doesn't fit very well with number-theoretic culture; people expect more directly structural/conceptual explanations (where the structures and concepts involved should have to do with particular arithmetic objects in play, not general foundational ideas).

[By the way, I think this is an example of material that would have been better posted as an answer to the original question then on this meta-thread.]

• Matt, do you think about whether or not this particular proof has used the axiom of choice; or do you wonder if the statement is provable without the axiom of choice? And when you do think about this, do you expect someone else to go through Wiles proof in its entirety and underline every use of the axiom of choice, and footnote how it can be circumvented? – Asaf Karagila Jan 4 '14 at 10:15
• @AsafKaragila: Dear Asaf, I mainly try to imagine putting all arguments in the framework of Kronecker's dictum about the natural numbers; I like to imagine that number theory (or the number theory I'm interested in) can be "quarantined" from foundational issues. I do know a large amount of the details of Wiles's argument, so I don't really expect someone else to think about it; rather, I do so myself. (And not just with Wiles's arguments, but with my own arguments, and other related arguments in the field.) Best wishes, – Matt E Jan 4 '14 at 13:53
• @AsafKaragila: P.S. I have edited my answer to note one concrete example of eliminating a choice-like construction from the argument. – Matt E Jan 4 '14 at 13:54
• Matt, it did occur to me that for a number theorist not experienced in set theory, the appeal to an application of Shoenfield Absoluteness would undoubtedly look like a black box. Ultimately I think the set theorists are making a very powerful point, but not one that makes the proof-theoretic details of eliminating choice from the proof transparent. I'm not sure what can be done at this point, but perhaps another question could be asked to get more details. Best regards, Todd. – user43208 Jan 4 '14 at 14:31
• Matt, alright then, a poor example with Wiles' proof. But I suspect that you understood my point nonetheless. I don't think that number theorists are not asking these sort of questions, I'm sure that a lot of people do. Much like set theorists would ask for how we can eliminate model theoretic proofs (which rarely do occur) in set theory. But still, as a number theorist, if I were to approach you with a choice-free proof of FLT, your response wouldn't be "No. I want a choice-free version of the Wiles proof."; [...] – Asaf Karagila Jan 4 '14 at 14:46
• and certainly if the proof itself uses heavy machinery which lies beyond the basic domain of the standard natural numbers, it seems to me that perhaps one should be willing to accept this sort of fact, that employing set theoretic and proof theoretic magic might not be sufficiently satisfying. Moreover, even if you did want to see a certain thing, you'd pick yourself up and go through with it. My point against the undeletion and reopening of this thread is that there was a lot of fussing about it before it even reached an accepted form that generated two answers on meta. [...] – Asaf Karagila Jan 4 '14 at 14:50
• And I'm not even going to start and point out the utter dishonesty of posting this on MO, before the MSE thread was deleted, without even mentioning the cross-posting (something which is looked upon badly regardless to the OP, or the quality of the question.), and everything else related to that matter that happened there. There is another problem lying in the fact that this is not the first time that the OP starts a thread, which is then leaking to two meta-threads and countless arguments before a reasonable answer is given anywhere. That is not the way things should be. [...] – Asaf Karagila Jan 4 '14 at 14:51
• Finally, I do accept the fact that there are cultural and personal issues to be dealt with here. And that perhaps there is a fault in part of the community which to some degree antagonizes the OP. But there is a lot to be said about the OP himself, and the consistent insistence that nothing he does is wrong, and the refusal to accept the opinion of anyone else. This causes some people to stop giving any leeway to the OP, and hit the "eject" button on the slightest issue. The OP is fully aware of that by now, but does nothing to correct this. [...] – Asaf Karagila Jan 4 '14 at 14:54
• So perhaps if the question was posted by someone else, and in a proper and well-presented form to begin with, and was not met by so much meta issues... perhaps then it would be a good answer to it. Perhaps Andres' answer on the comments to this meta thread would have been an acceptable answer (although you indicate that it isn't really an acceptable answer from a mathematical point of view, but rather a metamathematical point of view). But things happened the way they happened, and that only made the chasm between the OP and a part of this community wider apart. Regards, – Asaf Karagila Jan 4 '14 at 14:56
• (I am sorry for this extremely long comment, I tried to keep it short and not elaborate on some of the things that I wanted to add. I have no intentions to reply any replies to this long post, because I don't want to be dragged into an infinite discussion on meta, like some people enjoy see me go through. Hopefully those comments shed light on my side, and perhaps on other people's opinion on this not-first-incident on the matter of this particular user. And I'm sorry that my memory works, and I cannot separate a question from its asker.) – Asaf Karagila Jan 4 '14 at 14:59
• @Asaf: Dear Asaf, Don't feel any obligation to reply. I just wanted to let you know that I read your comments, and I do think I understand your point of view (and I realize that it isn't isolated; my view is probably much more in the minority than yours). I appreciate you going to the effort of explaining it, and I also am learning more about other mathematical cultures by reading your remarks (here and elsewhere). Best wishes, – Matt E Jan 4 '14 at 15:12
• Dear Matt, it is very easy to explain (even if it is a lengthy explanation) if the other side is willing to listen. I always admired your patience and kindness in this aspect. I should probably say that I never saw myself a cultural ambassador of anything but myself, and even then there are exceptions. :-) – Asaf Karagila Jan 4 '14 at 15:35
• @user43208: Dear Todd, I don't think it's just the black-box aspect that people might find unappealing. The point is that an appeal to choice (say in the Taylor--Wiles patching method) is one concrete manifestation of a more general non-canonicality inherent in the construction. This is what people don't like. In algebraic number theory, arguments and constructions are typically canonical, and if they're not, people work to make them so. (Consider pre-Artin class field theory, in which had a non-canonical isomorphism between abelian Galois groups and ray class groups, and how much more ... – Matt E Jan 4 '14 at 20:24
• ... satisfying the canonical isomorphism given by the Artin map is.) Reducing to $L$ and using choice there doesn't really deal with this non-canonicality, since the well-orderings so obtained don't reflect any of the actual number-theoretic structure of the objects under investigation. Best wishes, Matt – Matt E Jan 4 '14 at 20:27
• @ColinMcLarty: Dear Colin, No, I don't think so. (I think that article explains a proof, or a modification of a proof, of Faltings that gives a more concrete alternative to Mazur's original construction of universal def. rings of Galois reps. via appealing to Schlessinger's criteria.) I don't have my copy of the book with me, but it's in one of the chapters explaining the Taylor--Wiles patching argument, I think the one called Criteria for complete intersections''. Regards, – Matt E Feb 5 '14 at 0:04

As the comments to the question state, the trivial answer to the question is "no, the use of the axiom of choice is not essential" because of some metatheorems in set theory.

I voted to close the question after it was clear that the desired response was to reject the trivial answer. Instead, the question was for someone to go through Wiles' literal proof line by line and (somehow) opine on the use of choice. I see at least two problems with that:

• It is too broad. As the FAQ says, if one can imagine an entire book being written to answer a question, it is too broad. To give the desired answer, one would need to look not only at Wiles' proof but at all the theorems it uses, including (famously) results from the SGA. That would take something like a book to answer, so in my opinion it is too broad.

• It is primarily opinion based. There is no objective standard for "can be removed" after the trivial answer has been excluded, because now one is forced to decide how much one can deviate from Wiles' original proof without making any "essential" changes.

• If somebody asked whether Wiles (or Perelman, or Mochizuki, or whatever other) proof is correct and complete, an approximate expert answer that talks about known aspects of the proof would have been the expected and sufficient answer. On what basis do you interpret this question any differently, e.g., as asking to go line by line through the proof? One can cite what has been published (McLarty), what has been announced (MacIntyre), relevant metatheorems (going beyond the one you stated), or say any number of other high-level observations similar to the ones about correctness of the proof. – zyx Dec 31 '13 at 2:56
• The question does not seem to accept an approximate expert answer (which is, of course, "yes, AC can be eliminated"). I am somewhat familiar with McLarty's work, but I do not see it as particularly relevant to the question whether AC can be eliminated from Wiles' proof, because McClarty seeks any proof and seeks to eliminate more than just AC. Separately, I have qualms about whether the questions you allude to in your first sentence would be on topic. – Carl Mummert Dec 31 '13 at 3:03
• McLarty and others are relevant to other lines of argument about AC. It's amazing this has to be pointed out, because for no other question on MSE is an abstract existence theorem that answers one (possibly unintended) interpretation of the question taken as a reason to make it impossible to add other types of answer. I would think that the existence of one answer demonstrates that the question is answerable, which is a good thing. – zyx Dec 31 '13 at 3:19
• @zyx: as far as I can tell, it is the asker who made the decision that only a very specific type of answer is acceptable - and it is that limitation in the question that led me to vote to close. If the question were modified to ask about the general foundations in which FLT might be provable - without reference to Wiles' literal proof and without a specific focus on AC - then the question would be much improved, and the sort of answer you describe might fit. But as the question is currently stated, I am not convinced that it would fit. – Carl Mummert Dec 31 '13 at 3:24
• If you did not notice, I voted to close after the question had been reopened and edited to narrow its focus. – Carl Mummert Dec 31 '13 at 3:27
• I did see that. What I did not see is where or how the asker "made the decision that only a very specific type of answer is acceptable". The focus of the question was narrow enough before and after the edit (I think the edit was a pointless MSE thing forced by the first set of close votes), but setting that aside, in the post-edit version it is hard to see how stating that the question is about Wiles' original proof requires a line-by-line analysis in order to produce the kind of answer that would have been expected, sufficient, and generally appreciated. – zyx Dec 31 '13 at 3:36
• Perhaps we simply read the question differently. @zyx. – Carl Mummert Dec 31 '13 at 3:38
• Clearly that is so, but I'm genuinely puzzled as to what (or where, in the OP's writing) is the part you read as requiring a line by line analysis, or fundamentally different in character from any number of general questions one can ask about a big proof, such as whether it is complete. – zyx Dec 31 '13 at 3:40

In the comments to this question, you have suggested that you are not interested so much in whether a proof of FLT requires AC, but whether Wiles's specific approach requires it. If you edit the question to reflect this and then flag it stating that you have edited it and would like it reopened, I will gladly do so.

• Will you also close math.stackexchange.com/questions/618311/… as a duplicate of MK's question while you're at it? (Since it's "clear" that it's not about FLT without choice, but Wiles' proof without choice; which I still think is way too broad, or can be answered in a comment.) – Asaf Karagila Dec 26 '13 at 1:09
• @AsafKaragila Sure. – Alex Becker Dec 26 '13 at 1:10
• @AsafKaragila On the topic of whether the question is "too broad": it may be, but it's not obvious enough for me to take action as a moderator. I can certainly conceive of answers that could reasonably be given by an expert without too much work, e.g. that one of his intermediate results implies some form of choice (I have no idea whether this is true). However, if the community closes it as "too broad" I will respect that. – Alex Becker Dec 26 '13 at 1:13
• No, certainly answers can be given by an expert. "No. No one sat down to check that." and "It seems reasonable that for the case of FLT no choice is needed, but no one verified that". Maybe even something along the lines of "No, nobody checked that because no one had asked that question seriously until now. Here is Wiles' proof, feel free to work on that issue. Good luck". I would be extremely surprised if anyone had actually worked on that before, and any answer longer than those one-liner comments is to be given. – Asaf Karagila Dec 26 '13 at 1:18
• @AsafKaragila Perhaps. I just don't know enough about the body of research to make that claim. – Alex Becker Dec 26 '13 at 1:25
• @AsafKaragila, that is incorrect: there is a lot that has been said on this subject by experts, and more that can be said. Keeping the question open is one way to allow that to happen. – zyx Dec 26 '13 at 1:46
• It is not even the most relevant example, but Colin McLarty's papers on homological algebra and algebraic geometry foundations are specifically aiming at understanding what (from the logic and set theory side, which is his background) is needed in Wiles proof. That is an example of someone who "actually worked on that". – zyx Dec 26 '13 at 1:55
• @AlexBecker [If you edit the question to reflect this and then flag it stating that you have edited it and would like it reopened, I will gladly do so.] I edited the question as you suggested and flagged it. – Makoto Kato Dec 27 '13 at 0:46
• @AlexBecker Are you there? – Makoto Kato Dec 27 '13 at 6:23
• Alex, if you want to cast the fifth vote, it's not a moderator power use anymore. But from what I gather from the comments here and to the questions it seems that "Experts are working on this topic" implies that the "necessity of large cardinals" and "the necessity of the axiom of choice" are the same thing. I can't wait for the rest of the set theory community to hear about that! And that Colin McLarty and other experts working on simplification of the FLT proof will only work on it if the MSE question is open, and will not choose to publish their result in an actual journal instead. – Asaf Karagila Dec 27 '13 at 11:17
• @AlexBecker Thanks. – Makoto Kato Dec 28 '13 at 5:49
• Is "experts are working on this topic" something posted here, or the meta distortion field at work? Experts said and wrote things about FLT in relation to set theory, and there is "more that can be said" that is not (yet) noted in that literature, but can be remarked on MSE if the question stays open. For example the internal logic of $(\infty,1)$-categories, the structured setting for higher homotopy theory, is believed to be an intuitionistic type theory, in which case the classical set theory foundation was irrelevant. But @AsafK sarcasm is clearly more interesting. – zyx Dec 29 '13 at 4:22
• > the comments [implied] experts working on simplification of the FLT proof will only work on it if the MSE question is open < ---- returning to the world of nonfiction, what the posted comments actually said is that it is not possible to share in MSE the results published by those experts (or to add other relevant observations) as long as the question is closed. Some of it can, and possibly will, be posted under the "duplicate" query, but some things are specific to the FLT proof and as long as that can not be open for discussion in MSE, the material just named apparently can't be posted. – zyx Dec 29 '13 at 4:59
• @zyx: I think you are looking at a different question, such as "is FLT provable in PA"? The question as stated is just about the axiom of choice, not even about eliminating inaccessibles. – Carl Mummert Dec 31 '13 at 2:18
• I am looking at the posted question, which (even if taken with the absurd restriction that inaccessibles, PA and other matters are to be excluded from the responses) has answers about the AC issue that do not proceed from from an analysis of absoluteness, and are tied to some particular features of FLT that are not common to other big theorems like the Mordell and Weil conjectures, and therefore not expected to appear under the "duplicate". The place to post those things is under the original question, not a meta comment thread. @CarlMummert – zyx Dec 31 '13 at 3:07