[math-fun] Fermat's Last Theorem question
Q about the proof of FLT: I realize that Fermat himself wouldn't recognize Wiles's proof, but would Fermat recognize the assumptions? I.e., does the Wiles proof require any "exotic" assumptions -- e.g., axiom of choice, generalized Riemann hypothesis, etc. ?
On 2/19/2013 10:54 AM, Henry Baker wrote:
Q about the proof of FLT:
I realize that Fermat himself wouldn't recognize Wiles's proof, but would Fermat recognize the assumptions?
I.e., does the Wiles proof require any "exotic" assumptions -- e.g., axiom of choice, generalized Riemann hypothesis, etc. ?
It may surprise you to find out that the question of what assumptions Wiles' proof requires is still a subject of debate. To take care of the uncontested parts first, Wiles definitely does not rely upon RH, ERH, GRH or any other unproved hypothesis of number theory. His result is "unconditional". He does (implicitly) use AC, if only because it is embedded deep into the tissue of modern algebra (e.g., starting on page 3 of Atiyah and Macdonald's "Introduction to Commutative Algebra"). The controversy arises from Wiles' use of Grothendieck's development of algebraic geometry, and in particular of so-called "cohomological number theory". As a matter of technical convenience, Grothendieck assumes the existence of a "universe", which is, essentially, a set that can model ZFC. The existence of such a set implies the consistency of ZFC, so (by Godel Incompleteness) it is an assumption strictly stronger than ZFC. The question is whether this technical device (equivalent to assuming the existence of an uncountable strongly inaccessible cardinal) can be removed. One common opinion is that it can in all proofs of interest, including Wiles', but that it may be quite some time before anyone actually succeeds in doing so. I learned most of what I know about this issue from a paper by Colin McLarty published in 2010 in the Bulletin of Symbolic Logic (online here: http://www.cwru.edu/artsci/phil/Proving_FLT.pdf). It is surprisingly readable, but of course it only presents his point of view. In particular, he believes that the usage of universes is removable, but doubts that Wiles' proof can be reduced all the way to Peano arithmetic. -- Fred W. Helenius fredh@ix.netcom.com
On 2/19/2013 10:54 AM, Henry Baker wrote:
Q about the proof of FLT:
I realize that Fermat himself wouldn't recognize Wiles's proof, but would Fermat recognize the assumptions?
I.e., does the Wiles proof require any "exotic" assumptions -- e.g., axiom of choice, generalized Riemann hypothesis, etc. ?
When I answered this yesterday, I cited a 2010 article by Colin McLarty. He's been busy since, and my newsfeed this morning contained a headline from Science News about his work: "A mathematician puts Fermat's Last Theorem on an axiomatic diet" (http://www.sciencenews.org/view/generic/id/348403/description/A_mathematicia...). It's a fluffy article based on work McLarty announced at the recent Joint Meetings; here's the abstract for that talk, "Grothendieck's cohomology founded on finite order arithmetic": Despite rumors to the contrary, Grothendieck and others published proofs using Grothendieck universes, which are sets so large that ZF does not prove they exist. Number theorists to this day cite those published proofs. More conservative references avoid universes but still use far stronger set theory than the number theory requires, such as large amounts of replacement. We describe the issues and show how to formalize the entire Grothendieck apparatus at the strength of finite order arithmetic (simple type theory with infinity) and describes progress towards yet weaker foundations. (Received September 18, 2012) So he claims to have shown that Grothendieck's universes are not needed, but he's still a long way from Peano arithmetic. -- Fred W. Helenius fredh@ix.netcom.com
Let me add another sentence from that Science News article, since not quite knowing what either "finite order arithmetic" or "simple type theory" means, this clarified things for me: ----- McLarty recently showed that Fermat’s Last Theorem can be proven using the ordinary axioms of mathematics, and even a bit less. ----- The article's author seems to say that the ordinary axioms of mathematics means "set theory", which I take to mean the ZF axioms, apparently without AC. --Dan On 2013-02-20, at 10:04 AM, Fred W. Helenius wrote:
On 2/19/2013 10:54 AM, Henry Baker wrote:
Q about the proof of FLT:
I realize that Fermat himself wouldn't recognize Wiles's proof, but would Fermat recognize the assumptions?
I.e., does the Wiles proof require any "exotic" assumptions -- e.g., axiom of choice, generalized Riemann hypothesis, etc. ?
When I answered this yesterday, I cited a 2010 article by Colin McLarty. He's been busy since, and my newsfeed this morning contained a headline from Science News about his work: "A mathematician puts Fermat's Last Theorem on an axiomatic diet" (http://www.sciencenews.org/view/generic/id/348403/description/A_mathematicia...). It's a fluffy article based on work McLarty announced at the recent Joint Meetings; here's the abstract for that talk, "Grothendieck's cohomology founded on finite order arithmetic":
Despite rumors to the contrary, Grothendieck and others published proofs using Grothendieck universes, which are sets so large that ZF does not prove they exist. Number theorists to this day cite those published proofs. More conservative references avoid universes but still use far stronger set theory than the number theory requires, such as large amounts of replacement. We describe the issues and show how to formalize the entire Grothendieck apparatus at the strength of finite order arithmetic (simple type theory with infinity) and describes progress towards yet weaker foundations. (Received September 18, 2012)
So he claims to have shown that Grothendieck's universes are not needed, but he's still a long way from Peano arithmetic.
-- Fred W. Helenius fredh@ix.netcom.com
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
On Wed, Feb 20, 2013 at 2:02 PM, Dan Asimov <dasimov@earthlink.net> wrote:
Let me add another sentence from that Science News article, since not quite knowing what either "finite order arithmetic" or "simple type theory" means, this clarified things for me:
----- McLarty recently showed that Fermat’s Last Theorem can be proven using the ordinary axioms of mathematics, and even a bit less. -----
The article's author seems to say that the ordinary axioms of mathematics means "set theory", which I take to mean the ZF axioms, apparently without AC.
I would very much doubt that it means ZF, rather than ZFC. Do you think that "the union of countably many countable sets is countable" is a theorem of ordinary mathematics? It's not a theorem of ZF (by "countable", I mean not a set in 1-1 correspondence with aleph-null, but a set that is not larger than aleph-null; it might be incomparable). Responses of the form "here's an informal proof that the countable union of countable sets is countable" don't show this is incorrect; they just show that informal mathematical reasoning of the sort you normally use makes unconscious use of at least a weak form of choice, such as countable choice. Unless you're an expert in the field, or actually formalize your proof, I don't trust intuitions that a proof can be formalized in ZF. Andy
--Dan
On 2013-02-20, at 10:04 AM, Fred W. Helenius wrote:
On 2/19/2013 10:54 AM, Henry Baker wrote:
Q about the proof of FLT:
I realize that Fermat himself wouldn't recognize Wiles's proof, but would Fermat recognize the assumptions?
I.e., does the Wiles proof require any "exotic" assumptions -- e.g., axiom of choice, generalized Riemann hypothesis, etc. ?
When I answered this yesterday, I cited a 2010 article by Colin McLarty. He's been busy since, and my newsfeed this morning contained a headline from Science News about his work: "A mathematician puts Fermat's Last Theorem on an axiomatic diet" (http://www.sciencenews.org/view/generic/id/348403/description/A_mathematicia...). It's a fluffy article based on work McLarty announced at the recent Joint Meetings; here's the abstract for that talk, "Grothendieck's cohomology founded on finite order arithmetic":
Despite rumors to the contrary, Grothendieck and others published proofs using Grothendieck universes, which are sets so large that ZF does not prove they exist. Number theorists to this day cite those published proofs. More conservative references avoid universes but still use far stronger set theory than the number theory requires, such as large amounts of replacement. We describe the issues and show how to formalize the entire Grothendieck apparatus at the strength of finite order arithmetic (simple type theory with infinity) and describes progress towards yet weaker foundations. (Received September 18, 2012)
So he claims to have shown that Grothendieck's universes are not needed, but he's still a long way from Peano arithmetic.
-- Fred W. Helenius fredh@ix.netcom.com
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
-- Andy.Latto@pobox.com
participants (4)
-
Andy Latto -
Dan Asimov -
Fred W. Helenius -
Henry Baker