The Coq mailing list

[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