[FOM] The gold standard and FLT

[Franck Slama]

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/1e7ed840/attachment-0001.html>