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

[Harvey Friedman]

On Mon, Jan 8, 2018 at 12:18 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Foundations of Mathematics <fom at cs.nyu.edu>
> On Mon, 8 Jan 2018, Harvey Friedman wrote:
...
> I would phrase your objection as, "There is always the possibility that the
> mathematical reasoning used in the proof is incoherent."  This is not the
> same as saying that there is an inconsistency in some particular axiom
> system.  For a start, there is no such thing as "the" relevant axiom system
> that is necessary to formalize a particular argument such as the proof of
> the irrationality of sqrt(2).  More importantly, David Fernandez Breton's
> objection implicitly suggests that the *source* of our belief in the
> correctness of our mathematical reasoning is the consistency of some
> particular axiomatic system that we have concocted.  If we buy that, then we
> are quickly led down the garden path: We then start to worry about the
> consistency of the axiomatic system, and seek a *proof* of that consistency
> to allay our doubts, and then are dismayed that any such proof must be
> formalized in some other axiomatic system whose consistency is open to
> doubt, and so on in an infinite regress.
>
> This is all backwards.  It is only because we have prior confidence in the
> correctness of certain types of reasoning that we are able to define
> axiomatic systems and declare that they are even relevant to the project of
> investigating mathematical reasoning.
>
> In fact I would go further and say that if there is something incoherent
> about the proof of the irrationality of sqrt(2)---and remember that I chose
> this specifically because the proof is so easy and simple---it is not going
> to be exposed by concocting elaborate axiomatic systems and discovering
> inconsistencies in them.  It is going to come from reflecting on the proof
> itself.  That proof is at least as simple as any axiomatic systems that we
> devise.  If we have doubts about the irrationality of sqrt(2) then we are
> going to have doubts about strict reverse mathematics.
>

The whole point of SRM = strict reverse mathematics, is that
mathematical statements themselves form formal systems, so that the
present gap between formal systems logicians use and study and the
actual mathematics is closed. So inconsistencies in SRM systems are
the same as real inconsistencies in real mathematical thinking. So
what happens with inconsistencies in SRM rules what happens with real
inconsistencies in real mathematical thinking because they are one in
the same.

Essentially the entire point of SRM is to close this gap.

Harvey Friedman