[FOM] Michael Detlefsen

[Harvey Friedman]

So sad to hear of the passing of Mic Detlefsen.

On Sat, Jan 11, 2020 at 1:09 AM Timothy Y. Chow
<tchow at math.princeton.edu> wrote:
>
> Martin Davis wrote:
> > The following is quoted from the Notices of the AMS. It was called to my
> > attention by Dana Scott.
> >
> > Martin
> > ***************************************************************
> > Michael Detlefsen, whose research in mathematics and philosophy focused
> > on the work of David Hilbert, died October 21 a week before his 71st
> > birthday.
>
> I am sorry to hear the news.  Last April, I had an interesting email
> exchange with Professor Detlefsen, regarding whether Goedel's second
> incompleteness theorem (G2 for short) kills Hilbert's program of
> consistency proofs.  Detlefsen thought that it didn't.  I partially agree,
> in that I maintain that in addition to G2, one needs to assume what one
> might call a "formalization thesis":
>
>    (*) Any finitistic proof of the consistency of PA can be mimicked by a
>        formal proof of Con(PA) from the axioms of PA.
>
Chow goes on to compare this situation with the usual Church's Thesis
- say in connection with Hilbert's 10th. Here is my view.

1. One can raise this issue in both contexts. However, there is a
completely fundamentally important sense in which both results are
decisive, because they address the situation armed with the very best
definitional framework that we have, with absolutely no rivals. The
situation is extremely decisive COMPARED to what we have all through
science and engineering

2. It is only the special preoccupation of pure mathematicians and
philosophers who are obsessed (me included) with the search for
*PERFECT KNOWLEDGE*.

3. In other words, we look to strengthen anything that we reasonably
know, and we are interested in doing this REGARDLESS OF ANY REAL NEED
OR ANY PROMISE OF GETTING ANY WHERE because we are not afraid to
completely waste our time in the search for PERFECT KNOWLEDGE.

4, So we try to do things like this. Analyze what we mean or could
mean by "finitary proof" with the aim of showing that it must at least
be formalizable in PA. Or analyze what we mean by algorithmically
decidable and prove that it falls within recursive.

5. Well, efforts along these lines are still far from the PERFECTION
that we all seek, and most of us think that to gain that level of
perfection in these two context and other related contexts, is going
to require some great breakthrough.

5. However, failing to see this breakthrough, I do not have any doubts
that the right way of looking at both of these is that exactly the
right fundamentally important theorems were proved by Goedel, Davis,
Putnam, J. Robinson, Matiyzsevic. No kind of unforeseen expansion of
finitary and algorithmic is going to change that in the slightest.

Harvey Friedman





> The mimicry here is the kind of activity that people do when they read a
> theorem and proof in a mathematical text and try to convince a
> computerized proof assistant that what they've just read is correct.  In
> many ways this is similar to what computer programmers do when they read
> and understand an algorithm and then program a computer to execute the
> algorithm.
>
> Below, for those who are interested, is (part of) the final email that I
> sent to Professor Detlefsen.  It is too bad that he will never be able to
> continue the conversation.
>
> > Date: Wed, 24 Apr 2019 22:07:49 -0400
> > From: Timothy Y. Chow
> > To: Michael Detlefsen
> > Subject: Re: A comment of yours in the Artemov thread
> >
> > On Tue, 23 Apr 2019, Michael Detlefsen wrote:
> > > If all you’re saying is that application of (*) gives us good
> > > inductive evidence for the finitary unprovability of CON(PA), then I
> > > don't disagree.
> > >
> > > We had quite a bit of inductive evidence for this even before the
> > > proof of Gödel’s incompleteness theorems. (This is what we got from
> > > the many failed attempts to finitarily prove the consistency of
> > > arithmetic (analysis). Bernays and Kreisel have both emphasized this.)
> > >
> > > Does G2 in combination with (*) give us something more than good
> > > inductive support for the failure of Hilbert’s Program?
> > >
> > > If so, what?
> >
> > I would draw an analogy with computability and the Church-Turing thesis.
> >
> > Let's take something like Hilbert's Tenth Problem.  Wikipedia offers the
> > following statement:
> >
> >    Given a Diophantine equation with any number of unknown quantities
> >    and with rational integral numerical coefficients: To devise a
> >    process according to which it can be determined in a finite number of
> >    operations whether the equation is solvable in rational integers.
> >
> > This predates the definition of a Turing machine, demonstrating that
> > people already had a pretty good intuitive feeling for what a
> > satisfactory "process" would look like, long before Turing.
> >
> > Of course, today, thanks to the work of Davis, Putnam, Robinson, and
> > Matiyasevich, we know that there is no Turing machine algorithm for
> > solving an arbitrary Diophantine equation.  This is widely regarded as
> > resolving Hilbert's Tenth Problem in the negative.
> >
> > However, one can contest this conclusion, by rejecting the Church-Turing
> > thesis and maintaining that we might one day discover a "process" that
> > we all agree solves Hilbert's Tenth Problem in the affirmative.  The
> > process would just not be translatable into a Turing machine algorithm.
> >
> > I accept this objection.  Nevertheless, I would say that the work of
> > DPRM did more than "merely" give us "good inductive support" for the
> > unsolvability of Hilbert's Tenth Problem.  "Good inductive support" is
> > what I would use to describe repeated failures to come up with an
> > algorithm.  What the Church-Turing thesis plus DPRM did was to greatly
> > clarify our understanding of what a "process" or "algorithm" means, and
> > to show that with a certain carefully defined notion of "algorithm," it
> > can be mathematically proved that an algorithm for Diophantine equations
> > does not exist.
> >
> > Similarly, I take (*) plus G2 to give us comparable support for the
> > claim that Hilbert's program of finding a finitary proof of the
> > consistency of PA is dead. My claim (*), when generalized to arbitrary
> > statements of number theory, is analogous to the Church-Turing thesis,
> > and has a comparable amount of empirical support.  G2 is analogous to
> > the DPRM theorem.
> >
> > Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom