Re: [math-fun] Fermat's Last Theorem question
Yes, I can believe that FLT can be proved in ZF without AC. PA, on the other hand, is pretty rubbish (it can't even manage the well-ordering of epsilon_0). I would be highly surprised to see an elementary (provable in PA alone) proof of FLT. Sincerely, Adam P. Goucher
----- Original Message ----- From: Dan Asimov Sent: 02/20/13 07:02 PM To: math-fun Subject: Re: [math-fun] Fermat's Last Theorem question
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
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
Harvey Friedman's 'grand conjecture', partly in reply to McLarty, says that Fermat's Last Theorem (along with all theorems involving only finitary mathematical objects ever published in Annals of Mathematics) is provable in EFA, a weak fragment of PA. This demonstrates the conservation of surprise: either the grand conjecture is wrong or Adam would be surprised. Charles Greathouse Analyst/Programmer Case Western Reserve University On Wed, Feb 20, 2013 at 2:13 PM, Adam P. Goucher <apgoucher@gmx.com> wrote:
Yes, I can believe that FLT can be proved in ZF without AC. PA, on the other hand, is pretty rubbish (it can't even manage the well-ordering of epsilon_0). I would be highly surprised to see an elementary (provable in PA alone) proof of FLT.
Sincerely,
Adam P. Goucher
----- Original Message ----- From: Dan Asimov Sent: 02/20/13 07:02 PM To: math-fun Subject: Re: [math-fun] Fermat's Last Theorem question
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
_______________________________________________ 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
participants (2)
-
Adam P. Goucher -
Charles Greathouse