[FOM] re Harvey on "a very exciting claim."
gstolzen at math.bu.edu
Sun Mar 26 13:17:43 EST 2006
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
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^
> Here 2^ is an exponential stack of 2's of height 1000.
Harvey, I don't understand what this has to do with my remark about
With best regards,
More information about the FOM