[FOM] Re Harvey Friedman's "Sigma01/optimal" 24 Mar (II)

[Gabriel Stolzenberg]

   This is a continuation of my previous message with the same title.

   More questions for Harvey.  In number 5, where I answer my own
questions, I am inviting Harvey to agree or disagree and explain
why.

   5. Consider next the more familiar situation in which a theorem
plays a central role in classical math but has no constructive proof.
(E.g., IVT.)  Is this of interest classically?  Not necessarily.  Is
it of interest constructively?  Not necessarily.

   Now suppose that the theorem has constructive proofs but they are
all grotesque.  Is this of interest classically?  Not necessarily.  Is
it of interest constructively?  Not necessarily.

   Nevertheless, in a classical mindset, one might think, "Thank God,
we're not working constructively or we'd be stuck with only grotesque
proofs," failing to take into account that a statement that plays a
central role classically need not be of any interest constructively.

   6.  Please explain why A-translation doesn't apply to your proof
of the proposition to yield a constructive proof not much longer than
the classical one.  Isn't it of the form, "There exists n, such that
P(n)," where P is a decidable predicate?

   7.  Why is it of interest, other than as a striking mathematical
phenomenon, to have a classical proof of some statement that is not
grotesque and either there are no constructive proofs of it or there
are some but they are all grotesque?

   I ask because when I first saw your statement quoted by Andrej
Bauer, I assumed, perhaps mistakenly, that it was supposed to be a
case in which classical math provides knowledge that constructive
math wants but cannot get for itself (if only because the proofs
are too long).  It was this idea that made it seem exciting.

   8. Finally, do impredicative definitions figure in any of this?
Are you assuming, as you should, that they are OK constructively?

   That's it.

   With best regards,

   Gabriel Stolzenberg