[FOM] a very exciting claim

[Gabriel Stolzenberg]

   Andrej Bauer (March 20) quotes Harvey Friedman (March 18)
saying:

> > 4. 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.).

   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.

   Also, almost always what matters is not a theorem but a theory
of which it is a part.  When, say, by a tour de force, some
impressive result is attained, it's usually not a pretty sight.
(Until a theory is created in which it has a natural home, in the
course of which the proof is reworked and reworked and reworked.)

   Finally, some things are shorter and nicer in a constructive
mindset yet disturb the classical mind.  E.g., the definition of
|x|.  Constructively: x if x is at least 0, -x if x is at most 0.
Period.

   But a classical mathematical can't stop there.  He feels a need
to say that |x| is defined for all x.  On the other hand, in a
constructive mindset, one does not feel such a need.  Nothing is
missing.

   Classically, there is a tendency to assume that more is always
better---if you carry around more assumptions, it can only help,
without taking into account the effect of being loaded down with
the stuff.


   Gabriel Stolzenberg