The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

This entire discussion is fascinating.

I've never studied this stuff properly; what's a recommended undergrad textbook on this subject? (I assume the subject is proof theory? I've read some model theory but I've never bumped into many of the things namedropped here, so I feel it is not model theory. Ofc, I could be wrong.)

Thanks 

Siddharth

On Thu 3 May, 2018, 04:22 , <roconnor AT theorem.ca> wrote:

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.''

--

Sending this from my phone, please excuse any typos!