The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Freek,

Thanks for this question. It make me understand a bit better what is at stake here. Let me try to follow the implications. 

To answer your question: the constructive proof does not give directly an extra but it implies that it can obviously be done in another theory T’ where only constructive proofs are allowed.

But IIUC the (same) encoding of S in T’ may not correspond to the same theory (= set of provable formulas) than in T. So here we have a difficulty: define S in a sufficiently precise way to know how to define the same S in T and T’. 

So we are back to defining what exactly is provable in peano arithmetic.

Now I feel a bit less lost in this discussion :-)

Pierre

Le mer. 2 mai 2018 à 22:56, Freek Wiedijk <freek AT cs.ru.nl> a écrit :

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?

Freek