[FOM] The gold standard and FLT

[Franck Slama]

Apologies for all the the typos, typing on a phone in a bus wasn't the best
idea.
Amongst them :
- (paragraph 1, line 3) "in its naive *forme*"
- (paragraph 3, line 1) "*it's* because instead of working with a precise
set of axiom"
- (paragraph 3, line 5) "they need to be careful with what *they*
manipulate"
- (paragraph3, line 11) "is *there* a risk to proceed like that ?"
- (paragraph 3, line 12) "Whether it is the fact that *there* exists an
appropriate system or the list of axioms of ZFC does not matter to me"
And without doubt certainly many others.

Best,

Franck

On Thu, Jan 11, 2018 at 9:48 AM, Franck Slama <franck.slama.pro at gmail.com>
wrote:

> Hi,
>
> Arnon, you might be biased because of your interest towards the
> foundations of maths, that we certainly all share
> here in this mailing list. However, mathematicians have been doing
> mathematics (and quite evolved mathematics!)
> long before set theory (even in its naive formed) started to be defined.
> Before the end of the 19th century, no one thought
> it was important to define a single system, with well defined axioms, and
> to prove the entirety of all mathematical
> theorems in this unique system. I (and I think all of us here) agree that
> this is what we effectively need if we want
> to have a single and consistent corpus of mathematics and not many
> separated areas (algebra, differential calculus,
> geometry, and so on) that would be incompatible together.
>
> However, this level of precision is inaccessible to most mathematicians,
> who often do not know (or care) much about
> the logical system in which they are building their proofs. For them, such
> a logical consistent system is taken for
> granted, and they do not wish to be involved in this at all. Although this
> is rather sad because formal logic is a fascinating
> area, I am forced to admit that if they would have to go down to this
> level, they would never have been able to make their
> contributions in their fields, which are no less beautiful. I strongly
> believe no one would have defined and showed important
> properties about elliptic curves and Galois cohomology by systematically
> going down to the axioms of ZFC.
>
> If mathematicians do not want to be involved in this activity of
> formalisation of mathematics, its because instead of working
> with a precise set of axiom, they work with one big axiom : that it's
> possible to define such a consistent system that allows
> them to work with sets, functions, derivatives, integrals, and everything
> else that they need every day. It's their big axiom.
> Are they crazy to believe in this? I don't think so. During the 19th
> century, mathematicians have found some paradoxes,
> and they've understood that they need to be careful with what manipulate,
> especially when they deal with "low level objects".
> So, some work on foundations has started to become important, and became
> an entire area in itself. This is our activity.
> We need to build such well defined logical systems in which mathematicians
> can do their work. And they (the vast majority
> of mathematicians), do not really care about what this exact system is.
> That's the low level, the assembly language of
> mathematics. What they want to do is high level, abstract mathematics. And
> our work is to provide them with a consistent
> system in which they can use their favourite every day objects. In CS
> terms, we're building the compiler of the mathematical
> language, down to set theory. Is their a risk to proceed like that (ie, to
> let them work outside of a precise formal system)? Yes.
> But we should accept this risk, as we must always believe in something.
> Whether it is the fact that their exists an appropriate
> system or the list of axioms of ZFC does not matter to me. It's the same :
> we are forced to believe in something. And by the way,
> I'm not at all confident with the list of axioms of ZFC, but that's just
> my taste.
>
> Let's be clear : if ZF or ZFC would turn out to be inconsistent, that
> wouldn't be the end of mathematics. I would be sure that
> it would be possible to defined another system in which everything that
> has been done could be "translated". It's even possible
> that the inconsistency would come from an unused axiom. After all, there
> is an infinity of axioms in ZF due to the presence of
> axioms schemas. And all mathematics are necessary expressed using only a
> finite amount of axioms. So it's even possible
> that an inconsistency in the logical framework could not affect at all the
> mathematics that have been built. Of course, until we
> build another system (this time a consistent one), all our proofs would
> become quite a bit lose, as they would not be chained
> to a clear set of axioms, which is the ground level of mathematics. Now,
> does the 10th floor is going to collapse into the 9th ?
> That's not sure, and very unlikely. Everything can be seen as "proven" in
> a broken system because of the conservative
> Principe of Explosion ("from falsehood follows anything"), which means
> that we can no longer distinguish between the "true" and
> the "false" because there is no such notion in a broken system. However,
> this principle does not tell us that everything is wrong.
> It does not tell us that all airplanes are going to suddenly crash because
> everything is false. It only tells us that we can't reason
> any more about what is proven and what is not, as everything is considered
> proven de facto. Airplanes have been flying for decades,
> and there is no reason that would crash suddenly. It's most certainly only
> a problem in the "assembly language" that must
> (and I believe, can) be fixed.
>
> I would like to be clear that, like you, I like when proofs can be written
> with great level of detail. I even love when they are so precise
> that computers programs can verify them, thus telling us if they are
> effectively valid proofs in the considered logical system. The reason
> why it's even better is that a human can get the verification wrong, when
> a computer can't. However, I am not sure that this style of
> mathematics is what mathematicians want to do. It might be because we do
> not have the right tools yet.
> If you give any current proof assistant (like Coq, based on type theory
> and not set theory) to the mathematicians, 95% would stop playing
> after a couple of hours and get back to "their real work". I'm also sadden
> by this situation because I would love to see all mathematics
> formalised into a logical system (and I would prefer it to be based on
> type or category theory rather than set theory, but that's my bias
> towards computer science), that could be checked by a computer program.
> Quite honesty, that's my dream. But stopping mathematicians
> of all fields to work (or claiming that what they do is not really proven
> because it does not meet *our* standards) until we manage to get such a
> system that would be usable by them is not a great idea. My point is that
> we need them to continue be creative in their fields, because we
> need what they produce. And anyway, they are manipulating quite high level
> objects, and they do not want to intensionally break the system.
> So there is very low risk that they will get a false proof because of an
> inconsistency at the set-theoretic level. In the meantime, let's work on
> building some great formal systems that they could perhaps use in a couple
> of decades, to build and check all the the mathematical knowledge
> with a great level of detail.
>
> Franck
>
>
> On Wed, Jan 10, 2018 at 11:12 PM, Arnon Avron <aa at tau.ac.il> wrote:
>
>>
>> In reply to my words "standard, eternal criteria of mathematics"
>> (that meant, if it was not clear, the standard, eternal criteria of
>> a rigorous, acceptable proof in mathematics), David Brenton wrote:
>>
>> > I think you're getting this backwards. Math has not always been
>> > this "paradise of rigor", which has just stopped being so in recent
>> times.
>> > On the contrary, for the longest time (with possibly the only
>> > exception of Euclid's elements), mathematics was an activity where
>> > the primary objective was to obtain results, rather than to be
>> > rigorous. Looking at most proofs from two or three centuries ago,
>> > they look much more like the kind of intuitive arguments that physicists
>> > do than like modern times proofs. The whole concern about foundational
>> > issues is relatively recent, its embryo probably first arose about
>> > halfway through the XIX century, and it only took full force in
>> > the early XX century. Considering that math has been around for
>> > millennia, I'd say that being careful about axiom systems, and
>> > what assumptions are being made, and about completely rigorous
>> > proofs, and the like, is more the exception, rather than the rule.
>>
>> And Timothy  Chow wrote:
>>
>> > Idealism is one thing, but historical inaccuracy is another.
>> > "Making explicit in a very precise way what are the assumptions that
>> > underlie the alleged proof" is almost never done in mathematics.
>> >
>> > For centuries, Euclid was the gold standard.  Today, we don't think
>> > that Euclid "made explicit in a very precise way" what all the
>> > assumptions were.
>> >
>> > If we look at mathematical practice across all fields and all of
>> > history, your "standard, eternal criteria" are far from being
>> > either.
>>
>> I was really amazed to read this kind of defense of the
>> current alleged proof, and especially of the attitude, of those who
>> claim to have proved FLT. I do wonder if those algebraic geometers
>> would be happy with the comparison made in these two messages of
>> their activity and proofs with those of  the mathematicians
>> in the 17th and 18th 0...
>>
>>  I also wonder, in view of what is described in these messages,
>> why we torture our students and ourselves by teaching
>> them what a rigorous proof should look like, and in
>> particular point out to them as severe mistakes  claims made
>> in their "proofs" that are not justified  by the collection of the
>> assumptions of the theorem they try to prove and
>> theorems that have already been proved before. What for? After all,
>> one needs not justify, or even make explicit, all the
>> assumptions one uses. Right?
>>
>>   Anyway, both Tim and David are confusing, in my opinion,
>> the norms of some area with the actual activity of the people
>> involved in that area. Thus many  religious people do sins.
>> Does this mean that they do not know what are the norms
>> in their religion and what is expected of them?
>>
>>   Despite what Tim and David note, mathematicians have had
>> a rather clear standard of what a rigorous proof is since
>> the time of Euclid. (And if they try to forget it,
>> people like Berkeley were there to remind them.)
>> Yes. There were periods in which the will to make rapid progress
>> in science caused mathematicians to neglect the old mathematical
>> norm of rigor. This does not mean that the mathematicians
>> at that time were not aware that they are not following
>> the standard eternal criteria. On the contrary: they felt
>> the need to justify this fact by claims like "for
>> rigor we have no time". (Sorry I do not remember now who
>> said this, and what were his exact words.) And of course,
>> At that glorious period really great mathematicians
>> were falling in traps like "proving" that 1-1+1-1+1...=1/2
>> Luckily, we have made some progress since those days. Are we
>> starting to go back? I am afraid that we are beginning to.
>>
>>   One more remark about Euclid. Tim emphasizes that
>> "Today, we don't think  that Euclid `made explicit in a
>> very precise way' what all the  assumptions were."
>> Absolutely true.  We have made indeed a great (temporary?) progress
>> since Euclid's time, and our  criteria
>> of rigor are (temporarily?) higher. But is there anybody who
>> infers from this, or thinks, that Euclid did not *try*
>> to make all his assumptions explicit? The crucial thing
>> is not whether Euclid succeeded in fully following
>> the general principles he forever set for mathematics,
>> but that he did set those principles, and was doing
>> his best to follow them. In contrast
>> (according to what I read here), the experts about the
>> alleged proof of FLT do not bother at all to make
>> their assumptions explicit!
>>
>>   Some years ago I predicted that all the great known
>> problems of mathematics will be solved in the next few
>> decades, because all is needed for this is to make "proofs"
>> very long and complicated on one hand (so that
>> nobody can really check them),  and not care
>> too much about rigor on the other... Isn't this wonderful?
>>
>> Arnon
>>
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> https://cs.nyu.edu/mailman/listinfo/fom
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180111/d2785795/attachment-0001.html>