[FOM] re Harvey on "a very exciting claim."

[Gabriel Stolzenberg]

   In "a very exciting claim" (Mar 21), I made the following comment
in response to part of a remark by Harvey Friedman that Andrej Bauer
quoted (Mar 20).

> >  All???  How can one know that all constructive proofs of some
> > statement are grotesque (in the sense described or any other)?
>
> >This is one of the most exciting claims I've ever heard.

   In what follows, I reply to part of Harvey's reply to this (Mar 22).

> Recall the famous Kruskal Theorem:

> I spoke to Bishop about this theorem, and sent him the simplest known
> proof, due to Nash-Williams. I think I sent it also to Stolzenberg,
> but I am not sure. In any case, Bishop (and Stolzenberg) confirmed
> that the proof is rather far from constructive.

   Harvey, I had the Nash-Williams proof of Kruskal's theorem in mind
when I made my remark.

   I'm not sure that you sent it to me.  (I recall something you wrote
with a copyright at the top.)  More important, I was introduced to all
this stuff by you, mainly in telephone conversations.  Starting, as I
recall, with Paris-Harrington.

   I have no recollection of ever thinking that the proof is "rather
far from constructive."  (But I see a deep issue here, which I'll
take up in a separate message.)  Indeed, about 15 years ago, I spent
a long time working with someone who constructed a (constructive)
argument along the general lines of Nash-Williams but, IMHO, more
beautiful.

   As for Bishop, you may be right but I have to wonder whether you
remember correctly.  (In the memorial volume for Bishop, Nerode
vividly remembered *exactly backwards* something Bishop said in a
lecture and even recalled discussing it with him during the question
period!)  It doesn't sound like Bishop to me.  Also, as I recall,
my contact with you about this was several years after Bishop had
died.  (I'll try to check.)  Do you recall having two discussions
about Kruskal and constructivity spaced this far apart?


> THEOREM 8. Corollary 7 can be proved in strictly finite mathematics.
> However, any such proof in Pi12-TI_0 must use at least 2^[1000]
> symbols.

>  Here 2^[1000] is an exponential stack of 2's of height 1000.

   Harvey, I don't understand what this has to do with my remark about
your claim.

   With best regards,

   Gabe Stolzenberg