[FOM] Proving FLT in ZF or PA

[Harvey Friedman]

On 2/27/06 11:41 AM, "Ben Crowell" <fomcrowell06 at lightandmatter.com> wrote:

> Harvey Friedman wrote:
> 
>> Here are two possible explanations. [...]
> 
>> 1. These mathematicians are truly entirely comfortable with the present
>> situation ... they see nothing at all problematic about
>> Grothendieck universes, ...
> 
>> 2. They are trying to thumb their nose deliberately at the very idea that
>> mathematics need be formalized in any sense - or would even benefit from
>> being formalized in any sense.[...]
> 
> How about:
> 
> 3. They're convinced that the proof could be reworked so that it would
> only use ZFC, but they see it as a waste of time to carry out the
> routine steps that would be necessary. This would be like publishing
> a proof using infinitesimals, knowing that it could be rewritten
> using limits, and not feeling that anything would be gained by
> the rewrite.

I consider this as essentially the same as 2. I would accept your point IF
there was at least some footnote somewhere about how the proof can be
routinely adapted to lie within ZFC - say a simple sketch of a page or two.
Otherwise, I throw it in with 2. But I surmise from Colin that the issue
isn't even addressed in any footnote.

I didn't write 2 as idle speculation. I have certainly met some very well
known mathematicians expert in the categorical approach to mathematics who
believe strongly in 2. I wouldn't be surprised if 2 is taken for granted in
some circles, years ago, and at least as strongly today. My posting with the
full 2 is at http://www.cs.nyu.edu/pipermail/fom/2006-February/010070.html

But it looks rather promising that Colin McLarty will make the significant
contribution to f.o.m. by properly documenting the provability of FLT in a
fragment of ZFC. Fortunately he has the interdisciplinary skills, knowledge,
and interest to do this. I certainly don't.

> On 2/14/06 9:25 PM, "Robert M. Solovay" <solovay at math.berkeley.edu> wrote:
>
Earlier I asked:

>> For example, you might tell us something about

>> 1. Some of the results used that themselves may not be provable in PA, or
>> even properly statable in PA.

Solovay responded:

>     I mentioned the Langlands-Tunnel theorem. See Chapter VI in
>"Modular Forms and Fermats Last Theorem". I think this meets both your
>requirements.

>     As the cited book shows the Wiles-Taylor proof is a truly
>enormous beast. The work naturally seems to be carried out in third order
>number theory, and to compress it into PA seems a heroic if not impossible
>task.

Incidentally, here is a url for the book
http://www.amazon.com/gp/product/0387946098/103-1788394-4959032?v=glance&n=2
83155

You mention third order arithmetic here. How does this relate to the issue
that Colin McLarty is looking into? In particular, how confident do you feel
that FLT can at least be proved in third order arithmetic?

>     I'm extremly sceptical that the current proof can be reformulated
>in PA. Of course, there might be some wholly different elementary proof.
>I don't have strong opinions on that issue.

This is certainly among the most fascinating f.o.m. significant things I
have heard in years. What is, roughly speaking, the strongest system T for
which you would say now that

"I'm extremely skeptical that the current proof can be reformulated
in T. Of course, there might be some wholly different elementary proof.
I don't have strong opinions on that issue."

??

On 2/27/06 7:54 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> Harvey Friedman wrote:
>> Maybe it is relatively easy for some appropriate scholar to attest that
> [...]
>> Failing this, what about the prospects for some appropriate scholar to
>> attest that
> [...]
> 
> What exactly do you mean here by "getting a scholar to attest"?  This
> could range from a casual remark at tea by a famous mathematician who may
> be notorious for confidently proclaiming statements that sometimes later
> turn out to be false, to a published paper with some real work in it.
> Attestations on the former end of the spectrum are probably easy to come
> by, but do we really gain much from them?

I meant to say "appropriate scholar to appropriately attest ...".

>> It is somewhat surprising that algebraic geometers seem content to LEAVE
>> things in this state.
> 
> Based on anecdotal evidence (discussions with friends who are in algebraic
> geometry), "content" is the wrong word.
> 
> In other words, just because nobody is fixing the situation doesn't mean
> that everybody is "content" with it.  Was the mathematical community
> "content" with the status of the classification of finite simple groups
> prior to Aschbacher and Smith's recent work?  Some were, but a lot
> weren't; just because people weren't working on it doesn't mean they were
> "content."
> 
It should be much easier to document the provability in ZFC of this massive
amount of work than to substantially rework it. One should be able to
develop a strategy to document provability in ZFC perhaps with the help of
several of those mathematicians who are knowledgeable about various pieces.

I certainly have reached high levels of confidence about the formalizability
of proofs in restricted systems of various kinds, by such means, without
having any working knowledge of the relevant proofs. The best way to
document such "knowledge of formalizability" is perhaps not clear, but it is
doable. One lays out the principal definitions, perhaps in modified forms,
and one talks about the methods used for the various parts in logical terms.
I.e., one uses nested inductions here, and one uses explicit constructions
there, which are from thus and such comprehension axioms, etcetera. And then
one consults with the various people who have detailed working knowledge -
optimally, the authors. You may have to teach these consultants what to look
for that might upset the applecart.

All of this I am sure would have been suitably documented if they cared AND
they knew how to spot logical points. They could easily learn how to spot
logical points IF they cared about logical points.

I think that if one probes deeper, there is a very fundamental contempt for
foundational matters that lies at the heart of this situation. There is also
a lot of very strong Platonism going on.

In any case, it looks promising that McLarty and/or Solovay is going to
provide us some key insights.

Harvey Friedman