FOM: Re: science and constructive mathematics

Harvey Friedman friedman at
Tue Jun 20 13:40:23 EDT 2000

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.

More information about the FOM mailing list