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