[FOM] About Harvey Friedman's "Classical/Constructive Arithmetic"

[Gabriel Stolzenberg]

   In this message, I make a few comments about Harvey Friedman's
"Classical/Constructive Arithmetic" of March 18.

>   Examples where the known proof is nonconstructive, and where one
> can give a constructive proof, but all known constructive proofs are
> grotesque (e.g., extremely long, or extremely unpleasant, etc.).

   I don't understand.  Suppose a muddlehead makes a constructive
proof that reflects his muddleheadedness.  (Or three muddleheads
make three such proofs.)  What does this tell you?

>  Examples where the known proof is nonconstructive, and where one
> can give a constructive proof, but it is known that all constructive
> proofs are grotesque (e.g., extremely long, or extremely unpleasant,
etc.).

    What counts as a proof here?  Does everything have to be spelled
out from first principles?  Or are you concerned only with a "normal"
proof (one with things like "By lemma 2.7") that is long or grotesque?

   More important, according to what you say above, for a case of
this kind, you actually have a constructive proof that is extremely
long or extremely unpleasant.  But if it's extremely long, how did
you manage to make it?  It must have taken forever.  Also, how can
you be confident that it is correct?  Who is going to check this
monster?  Please explain.

> Apparently there are quite a number of famous AEA theorems of
> mathematics which people would like to prove constructively, but
> can't.  Nobody knows if they can be proved constructively.

   Also, who are these people, what are some of these classical
theorems and why do these folks want constructive proofs?  Is it
just a game?  A challenge?  The fascination of "I've proved that
a sign change exists but I don't know how to get a bound for it"?
(An eminent number-theorist once said this to me re a certain
phenomenon, adding "It's so fascinating!"  But I don't think it
took more than five minutes to convince him that he already had a
bound.  End of fascination.)

   Finally, the fact that something is a famous theorem of classical
math says nothing about its significance for constructive math.  And
this is true even if we have a constructive proof of it!  Hence, I
find the adjective "famous" a bit misleading.


   Gabriel Stolzenberg