The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 2 May 2018, Freek Wiedijk wrote:

> Hi Pierre,
>
> > But it is still just a matter of being careful right? You can
> > always reencode a logical system (say S) inside your preferred
> > one (say T, more expressive than S) as a regular first class
> > definition.
>
> 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'm being a little wishy-washy above, so some terms and conditions may 
apply.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''