[FOM] re re re Harvey on "a very exciting claim."

[Gabriel Stolzenberg]

   Harvey, I have to take this slowly to make sure I understand.
It's possible that the issues I raise below are irrelevant but,
if they are, I'd like to see why.

> So Corollary 7 can be proved constructively (under normal accounts), but
> any proof must be grotesque - in that it must use at least 2^[1000]
> symbols.

   What I first would like to know about is your proof that it can
be proved constructively.  Your "So" suggests that you believe you
have explained this already.  But, if you did, I didn't follow it.
Could you please go over this crucial point again?

   Also, do you agree that *if* your proof that it can be proved
constructively albeit grotesquely is itself constructive but not
grotesque, then that's it?  I.e., in that case, it would be like
almost every theorem that one proves in constructive mathematics.

   E.g., if Bishop claims to construct of a rational number with
a certain property, we don't expect to see something of the form,
m/n, in his proof.  We assume that all he has done is to define
(perhaps only implicitly) a program that if executed will yield
such an m/n.  But the printout of the computation, if thought of
as a proof, will almost surely be grotesque.


   Gabriel Stolzenberg