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

[Gabriel Stolzenberg]

   Here I want to have a second try at commenting on a statement in
Harvey Friedman's "Classical/Constructive Arithmetic." (Mar 18)  My
first try was in "About Harvey Friedman's 'Classical/Constructive
Arithmetic'" (Mar 28).

   In a list of five "questions" on which he proposes to concentrate,
Harvey writes:

> > 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 see how the quality of proofs of a certain statement that
some people happen to have made can be revelant to fom.  (By contrast,
Harvey's examples in which "all known" is replaced by "it is known
that all" seem to this layman to be of great interest for fom.)

   Also, fairly or not, mention of cases of this kind concerning "all
known constructive proofs" brings to mind the widespread perception
that constructive proofs are typically (more or less) grotesque compared
with classical ones.  But why is there this perception?  Is it a fact
about constructive math?  Is it a fact about the folks who are seen
doing it?  Or is it an artifact of seeing constructive math only in a
classical mindset?  Who is in a position to say?

   Gabriel Stolzenberg