[FOM] Re Harvey's "nonconstructive proofs."

[Gabriel Stolzenberg]

   On November 11, 2007, Harvey Friedman posted a very short message,
"nonconstructive proofs."  I am not sure what he meant to say in it,
but, on a reading I find attractive (though very possibly not what
he meant), I find it remarkable.

   On this reading, Harvey's posting is, at least in part, a response
to my own message, "the power of nonconstructive reasoning," of Nov 6,
wherein I discuss a fairly popular example of the alleged power of
nonconstructive reasoning and show that it (this particular example)
is an illusion.  (The illusion is that a constructive proof of the
same statement, if there is one, would be less elegant and much more
complicated than the classical one.  The statement is that there are
two irrational numbers, x and y, such that x^y is rational.)

   So far as I can make out, the content of Harvey's posting is that,
for Kruskal's theorem and two related ones, (1) the usual proofs are
"highly nonconstructive" and (2) there are also constructive proofs
(in reasonable senses of "constructive"), but, unlike the ones in the
simple example I considered, they appear to be "more involved."

   To me, this is a good observation.  Harvey describes the situation
without trying to draw any unwarranted conclusion from it.  By itself,
the fact that the existing constructive proofs are more involved means
very little.

   E.g., it could be that the authors of these proofs were merely
trying to "constructivize" a classical proof, instead of working
"naturally" constructively (as if classical mathematics didn't exist).
Such constructivizations are frequently messier than the classical
proofs they copy.  (The standard, embarrassingly lame, excuse for this
is, sure, it's more complicated, but this is because it's a stronger
result.  This is the flip side of the equally lame, "a classical proof
is a good first step toward getting a constructive one.")

   Or these "more involved" constructive proofs might simply have
been first tries.  The first proof of a theorem or theory (even
a published one) is often, in effect, a first draft, which is then
reworked (and reworked and reworked and...), usually by others.

   Speaking only for myself, if it could be shown convincingly that
every constructive proof of Kruskal et al has to be messier/more
complicated than the nicest classical proof, that would be fantastically
interesting---even more so, if there was a satisfying explanation of
why this is so.  (E.g., does it have to do with the impredicativity that
Harvey has shown every proof of Kruskal requires?)

   Finally, based on past experience, I would find it nice but much
less exciting to have a constructive proof of Kruskal that is at least
as nice as the nicest classical one.  In the several test cases that I
tried for other assertions, some of which took several years to complete
(it is not just a matter of making a proof but of creating a theory
from which it emerges in a natural way), this is indeed how it worked
out.

   As for Kruskal itself, in around 1990, I helped to rework what, so
far as I knew, was the first constructive proof of Kruskal.  Though,
as it stood, much of it seemed to have been done by brute force, it
seemed to be a promising candidate for being transformed (by a series
of reworkings) into a very nice proof of Kruskal.  But the author
dropped the project and, so far as I know, that was the end of it.

   Gabriel Stolzenberg