The Coq mailing list

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

Hi,
Adam means that Coq itself understand second order logic at its heart.
You don't need to develop a library for that, you can just formalize
your problems directly,

For example: "forall (R:nat ->nat -> Prop), forall n, R n n \/ R n 0"
is a formula that coq understands perfectly (although it is not
provable).

The typical situation where you need to formalize formulas by a
concrete type is if you want to prove meta-properties about second
order formulas themselves (like correctness or completeness of some
proof system).

Maybe a more precise description of the problems you want to formalise
and the kind of theorems you would like to prove about them would
help.

Best regards,
Pierre

2017-03-23 1:21 GMT+01:00 Caitlin McGregor 
<caitlin.mcgregor AT anu.edu.au>:
> Thanks for your response. (Apologies for the first order part of the
> question - that was silly!)
>
>
> The context is that if I wish to formalise some problem that involves second
> order formulas, I would like a library that defines such a type and proves a
> collection of lemmas that are in some sense "obvious" to the mathematician
> and require no explanation.
>
>
> One idea is to define the type myself and then define functions between my
> own second order formulas and some set theoretic notions, and then prove
> inside set theory. But I was wondering if there was a library that was
> explicitly working with second order formulas.
>
>
> Please bear with any misunderstandings that I have. Any help that you could
> provide would be greatly appreciated.
>
>
> Kind regards,
> Caitlin
>
>
> ________________________________
> From: 
> coq-club-request AT inria.fr
>  
> <coq-club-request AT inria.fr>
>  on behalf of
> Adam Chlipala 
> <adamc AT csail.mit.edu>
> Sent: Thursday, 23 March 2017 11:06:44 AM
> To: 
> coq-club AT inria.fr
> Subject: Re: [Coq-Club] Second order logic library?
>
> What exactly would be in such a library, considering that, in a reasonable
> sense, second-order logic is a subset of Coq's full logic?
>
> On 03/22/2017 08:03 PM, Caitlin McGregor wrote:
>
> Hi all,
>
>
> I am looking for a second order logic library in Coq, or even a first order
> library. Does anyone know if these are available?
>
>
> Thanks in advance,
>
> Caitlin
>
>