[FOM] Michael Detlefsen

[Timothy Y. Chow]

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.

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