FOM: Re: science and constructive mathematics

[Harvey Friedman]

Tennant wrote 6/19/00 4:21PM:

>Better to put it another way: using classical methods (e.g. proving P by
>refuting not-P) often gives us much shorter proofs than any known
>constructive proof of the same result.

In the standard contexts and interpretations I am thinking of, this is not
true. What examples do you have in mind?

E.g., my proof that PA is conservative over HA for Pi-0-2 sentences gives a
very modest blowup in the size of the proof.