A brilliant math ugrad at UMCP, Doug, is also a creative writer who

wants to work on large cardinals. His creative writing may help him there.

We had the following conversation:

DOUG: The proof of Fermat's last theorem depends on the existence

of certain large cardinals and hence is not in ZFC.

BILL: That is not true.

DOUG: Have you read the proof?

BILL: No, however, if that were true I would know it. See this blog entry.

DOUG: Why would you know it?

BILL: If FLT required LCs then

a) Number theorists would be nervous.

b) Logicians would be ecstatic

c) The math community would not have announced to the world that FLT was solved.

d) Wiles would not have collected his prize money for solving it.

e) Again, I would know it.

DOUG: All compelling arguments. Even so, FLT requires LCs.

BILL: I will bet you five dollars that the current proof of FLT does not depend on LCs.

DOUG: Uh. Your counter arguments are compelling.

BILL: So... no bet?

DOUG: Uh. No.

The next day I got an email from Doug with the subject heading

I cheated myself out of five dollars.

Doug found this article,

*What does it take to prove Fermat's Last Theorem? Grothendieck and the logic of number theory*by Colin McLarty, from 2009.The article says that YES the current proof of FLT DOES depend on LCs. Note that the proof is quite long and uses lots of other stuff that is sort of buried in it. So--- whats the catch?Why aren't number theorists nervous and logicians ecstatic? According to the article anyone who reads the proof of FLT and wanted to could unwind it and get it down to ZFC (and likely down to PA). But nobody has bothered yet.Hence nobody is nervous or ecstatic.

I will take their word for it, but it does make ME nervous. NOT about FLT which I am sure enough people have looked at (and looked at the background literature) that it really can be made to work in ZFC.I am more worried about papers that are not quite so looked at as having LC assumptions that are hidden from the reader that cannot be easily removed.

However KUDOS to Doug for telling me something in math that I did not know and should have. I will treat him to a more-than-five-dollar-lunch.

Postscript: AH, the article was right: FLT was proven using ordinary set theory last year. (See here) by Colin McLarty (I assume its the same person). I will still take Doug to lunch- in a stupid, pedantic, technical sense I was right- the current (2014) proof of FLT did not use LC. But for the real issue of there being any problem at all, I was clearly wrong. Only a logician would say I was right. Hmm- Doug is a logician. Its up to him. (Hmm- my spell checker allows `Hmm' but not `Hmmm')

Is there any publications of this recent result by McLarty? I have not been able to find any paper.

ReplyDeleteIs there a new proof of FLT? Or does McLarty now show that the original proof of Wiles can be interpreted/modified (albeit, not in any significant way) to do away with the LC assumption?

ReplyDeleteIs this a meta-mathematical result? In many cases, the advanced set theory axioms don't change the arithmetical structure. Hence if an arithmetical statement (FLT is a $\Pi_1$ arithmetical sentence) is provable using arcane set-theory axioms it is provable without them.

ReplyDeleteGrothendieck himself speaks to these issues in

ReplyDeletea letter to Ronnie Brown:--------

"The question you raise, 'how can such a formulation [as post-ZFC "universes"] lead to computations?' doesn't bother me in the least! Throughout my whole life as a mathematician, the possibility of making explicit, elegant computations has always come out by itself, as a byproduct of a thorough conceptual understanding of what was going on. Thus I never bothered about whether what would come out would be suitable for this or that, but just tried to understand - and it always turned out that understanding was all that mattered."

--------

Why would/should practical engineers/simulationists care? For the eminently practical reason that Grothendieck's world-view is invariant under the duality

"formulation ⇆ computation."That is, the path between a "thorough conceptual understanding" of practical computations and a Grothendieck-style "childishly simple" formalization of that understanding comprises asinglemathematical path … that can be creatively traversed in either oftwodirections.Concretely, engineers are motivated to traverse this two-way path, in both directions, by the (seeming) obstructions to our geometric/dynamical understanding that are associated to the singularities of varietal state-spaces, and by the (seeming) obstructions to our algebraic/informatic understanding that are associated to the finite-field discretization of varietal state-spaces.

Both practical computations and Grothendieck-style abstract formulations show us that these obstructions are illusory, such tat the practical and abstract approaches

togetherprovide us with a "thorough conceptual understanding" (in Grothendieck's phrase) of why the past generation'sthousand-fold capability increases and thousand-fold cost decreases in simulation capabilitycan plausibly continue for another generation. Which would be GOOD, needless to say!ConclusionThe unbounded quest to understand mathematics “in width, in depth, and in context” requires our collective embrace ofboththe Grothendieck-style "childish simplicity" of post-ZFC universesandtheir un-simple PA foundations … even if as individuals we may strongly prefer one style of mathematics over the other.To Sidles: yes, exactly. I will write a fuller comment. But real the point is just as Sidles puts it.

ReplyDeleteGetting the universe axiom out and just using ZFC is routine but no one does it. It would have some some cost in terms of the conceptual order. It has no real profit from a logical point of view since ZFC is also vastly disproportionate to the arithmetic core of the proofs. When Grothendieck and Dieudonne came up with the methods using universes they knew it was a convenience and could be avoided. The best example would be Deligne's chapter of SGA 4.5 where he gently words most results to avoid universes, although he specifies in that work that he is not giving complete proofs, and he refers to complete proofs he wrote elsewhere that do use universes.

ReplyDeleteNothing I have written changes the real arithmetic of the existing proofs. My goal is to preserve that arithmetic while lightening the logical apparatus around it. I have shown that ZFC+U can be very far weakened to a logic at the strength of finite order arithmetic (dealing with numbers, sets of numbers, and so on to any finite level, but only to finite levels and with all sets defined by arithmetic conditions). Some of the most general lemmas have to be treated carefully here but the parts of the proofs that number theorists care about are unchanged. This is on the Math arXiv as "

A finite order arithmetic foundation for cohomology".

As a lot of logicians have said, large parts of the proof that are not overtly in Peano Arithmetic can be put there with no real change. But not all. There is no reason to doubt it can all get into PA somehow, but there is no articulate proof yet that it can, let alone a known proof in PA. I am a great optimist and believe that someday someone will find an overtly elementary argument for FLT, likely using the concrete arithmetic that goes into Wiles's and later known proofs, but that will depend on genius. At the same time we can analyze the conceptual tools currently used to show how far PA can handle them.

have long wondered if large cardinals relate somehow to high space-complexity functions in TCS or some other structure. it would seem there would have to be a connection somewhere. maybe a big bridge thm lurking here....

ReplyDeleteI remember seeing a talk by A. Macintyre outlining possible avenues to showing that FLT can be proved in Peano arithmetic (this is discussed in §2 of McLarty's paper). He seemed pretty convinced that it is possible, though I don't know what concrete progress has been made so far.

ReplyDeleteNote that it is trivial there are finite statements about numbers that can only be proven assuming the consistency of large cardinals. Proofs are finite objects, and as GĂ¶del first noted, can be encoded using Peano Arithmetic. Because ZFC is recursive, the existence of a proof that ZFC+"there exists a measurable cardinal" implies 0=1 is ultimately a statement about the existence of an integer with certain elementary properties. In other words, the assertion that no such integer exists is exactly the assertion that measurable cardinals are consistent.

DeleteBecause of Matiyasevich's theorem (and its fully constructive proof), this can actually be expressed in terms of an explicit Diaphontine equation whose solutions encode proofs of inconsistency. Simpler would be to evoke the Davis-Putnam-Robinson theorem regarding exponential equations (like Fermat!).

(william e emba)

Something similar was done by Solomon Feferman in the 1960s. See his "Set-theoretical foundations of category theory", in Reports of the Midwest Category Seminar, III, Lecture Notes in Mathematics, vol. 106, pp. 201-247, Springer-Verlag, Berlin, 1969.

ReplyDeleteIn brief, lots of freewheeling uses of proper classes of proper classes, etc, in the style of category theory fit inside ZFC using reflection. The main application was to localization of categories, something the Grothendieck school treated using universes. J. Frank Adams in his book on Stable Homotopy went so far as to describe the written proof of the main result was really a "research program". later officially solved by Bousfield, who essentially kept track of the reflection invocations to provide cardinality bounds.

(william e emba)

Number theorists and others have stopped caring about set theory long time ago. People insisting on turning these categorical perspectives to set theoretical perspectives are doing a translation for the older generation of mathematicians who have not got used to the categorical foundation. You cannot teach algebraic topology worrying all the time how to translate it back to set theory and with this attitude the students also learn not to care about set theory. However older mathematicians who are not brought up in this fashion and don't use category theory have hard time adopting to the new reality and feel insecure in using these tools. This is despite the fact that categorical perspective are often more concrete that their set theoretical counterpart. Expecting people to worry about how the set theoretical foundations of their proofs in this age is like expecting Python programmers to worry about how their code would like in assembly or even worth Turing machines!

ReplyDeletehttp://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory#Criticisms

ReplyDeleteYou might be interested to know that there is a set theoretic principle in set theory such that if you assume it you will end up with theorems that are counter-intuitive and if you assume their negation you end up with some other counter-intuitive theorem. There is a false sense of security in some mathematicians for being inside set theory like ZFC. The most one can say is that ZFC doesn't seem to be an inconsistent system but formal consistency is far from being sound and corresponding to the reality.