[FOM] What is the current state of the research about proving FLT?

[Tennant, Neil]

Tim Chow wrote on Sunday, January 07, 2018 3:00 PM

>Consider some "easy" proof such as the irrationality of sqrt(2).  If we
>were to formalize this proof in some axiomatic system S and then were to
>discover that S is inconsistent, then we would simply shrug and discard S.
>The inconsistency of S would not affect our belief in the correctness of
>the proof that sqrt(2) is irrational.  We would just come up with some
>other system S' in which we could formalize the proof.  And if S' turns
>out to be inconsistent, we would come up with S''.  Throughout, our
>certainty in the correctness of the proof of the irrationality of sqrt(2)
>would remain unmoved.

There is a big difference between the counterfactual conditional

"If we were to formalize this [informal] proof in some axiomatic system S..., then..."

and

"If we were to provide in some axiomatic system S a formal proof of the theorem in question, then ...".

The process of beginning with a particular informal proof and formalizing it involves supplying
missing details in a way that produces a formal proof that one can describe as a faithful "structural homologue"
of the informal one. That's what is alluded to in the antecedent of the first counterfactual conditional above.

For an example of the result of such "supplying of missing details", whose outcome was absolutely dictated (or
so it seemed, compellingly, to me) by the form of the famous informal proof of the irrationality of sqrt(2), the 
reader should take a look at my paper "Pythagoras meets Peano", at

https://u.osu.edu/tennant.9/files/2015/12/pythagoras_meets_peano-1bh66qg.pdf

The blow-up factor from informal to formal proof looks to be two or three orders of magnitude, even for such a
simple and informally compelling result as the irrationality of sqrt(2). One shudders to think what the blow-up factor 
(for faithful formalization) would be for the current informal proof of FLT!

So much for "structurally homologous" formalizations of informal proofs.

One can also, however, interpret the antecedent of the second counterfactual conditional above in a much less 
constrained way. One can contemplate giving a formal S-proof that bears no "structural homology" at all to the famous
informal proof in question. (And S might not even be Peano Arithmetic.) It's really only with this unconstrained construal 
that Tim's imagined outcome can be seriously entertained (that of the subsequently discovered inconsistency of the system 
S used).

So there is the interesting project of rendering each informal proof of a mathematical theorem as (say) a natural deduction 
in some Gentzenian form. The resulting formal proof allows one to tell, definitively, exactly what undischarged assumptions 
are being used in order to prove the theorem in question (at least, according to the informal proof being formalized).

This project of logically detailed re-presentation of the known corpus of mathematics can be combined with
a philosophically informed search for even deeper principles from which conventional mathematical axioms
can themselves be derived. An example would be any successful neologicist derivation of the Peano Axioms for
Arithmetic from more "conceptually compelling" principles---principles that might even enjoy the status of logical
principles, or deserve the label "analytic" (i.e. true by virtue of just the concepts involved).

This ongoing project-and-search, when the mathematical expressions are treated via rules for their introduction and
elimination in the fashion of Gentzen, I call "Natural Logicism". It involves taking each branch of mathematics "in its own
right" and on its own primitive conceptual terms. One refrains from trying to straitjacket the mathematical theory in question
 into the language and axiomatic system of, say, set theory. It allows one to state the underlying principles in ways that 
are "sui generis" for the arithmetic of whole numbers, or fractions, or real numbers; or for points, lines and planes in 
(say, projective) geometry. It allows one to try to illuminate how and why the mathematics in question is applicable 
in our wider thought and talk about the world.

Within the context of Natural Logicism, Tim's imagined situation (IMHO) recedes to the virtually unimaginable---at least, as far 
as the irrationality of sqrt(2) is concerned!

Neil Tennant