The Coq mailing list

[Freek Wiedijk <freek AT cs.ru.nl>]

Hi Russell,

>> To give this a little twist: is a classical proof that
>> a constructive proof exists just as good as having a
>> constructive proof?  Or does the latter give you something
>> extra?
>
>It is just as good.
>
>A classical proof that a constructive proof exists is a Sigma_1 sentence. By
>Goedel's Dialetical interpretation all Pi_2 (and hence Sigma_1) sentences
>provable classically are provable constructively.  So it we can mechanically
>transform it into a constructive proof that a constructive proof exists, from
>which one can extract said constructive proof.

I guess you're talking about HA versus PA here?

But what if my "classical proof" is from ZF?  Or from ZFC?
Or from a consistent extension of ZFC by throwing in some
large cardinal axioms?  Is that classical proof then still
just as good?

Freek