The Coq mailing list

[Asya Bergal <abergal AT mit.edu>]

^ clarification, the file above was produced by me and ikdc AT mit.edu

On Thu, Mar 23, 2017 at 1:32 PM, Asya Bergal <abergal AT mit.edu> wrote:

It seems like you're looking for is known as a deep embedding of second-order logic in Coq. People are describing to you that you can use a shallow embedding inside of Coq instead, which is true but not useful to you (http://cstheory.stackexchange.com/questions/1370/shallow-versus-deep-embeddings).

I myself needed a deep-embedding of First Order logic for a former of project of mine, and failed to find an reasonable existing one. I've attached the very minimal formalization that I produced in case it's useful to you.

Good luck!

On Wed, Mar 22, 2017 at 10:21 PM, Caitlin McGregor <caitlin.mcgregor AT anu.edu.au> wrote:

Hi,

Ah I see where my lack of clarity is. Indeed, I do realise that Coq understands second order logic at its heart. I am working on proving meta-properties, in particular in correspondence theory. This shows certain correspondences between modal logic and first order logic, and in my case I go via second order logic.

Perhaps examples will help. Here is what I have already for the fragment of second order logic that I am working with:

(* Countably many unary predicates *)

Inductive predicate : Type :=

  Pred (n:nat) : predicate.

(* Countable many first order variables *)

Inductive FOvariable : Type :=

  Var (n:nat) : FOvariable.

(* The fragment of second order logic that I'm working with *)

Inductive SecOrder :=

    predSO : predicate -> FOvariable -> SecOrder

  | eqFO : FOvariable -> FOvariable -> SecOrder

  | allFO : FOvariable -> SecOrder -> SecOrder

  | exFO : FOvariable -> SecOrder -> SecOrder

  | negSO : SecOrder -> SecOrder 

  | conjSO : SecOrder -> SecOrder -> SecOrder 

  | disjSO : SecOrder -> SecOrder -> SecOrder 

  | implSO : SecOrder -> SecOrder -> SecOrder 

  | allSO : predicate -> SecOrder -> SecOrder

  | exSO : predicate -> SecOrder -> SecOrder.

 

Then, I define a satisfaction relation, SOturnst:

(* Iv = interpretation of FOvariables; 

   Ip = interpretation of unary predicates *)

Fixpoint SOturnst (D:Set) (Iv: FOvariable -> D) (Ip: predicate -> D -> Prop)  (alpha:SecOrder) : Prop :=

  match alpha with

    predSO (Pred n) (Var m) => (Ip (Pred n) (Iv (Var m)))

  | eqFO (Var n) (Var m) => (Iv (Var n)) = (Iv (Var m))

  | allFO (Var n) beta => forall d:D, SOturnst D (altered_Iv D Iv d (Var n)) Ip Ir beta

  | exFO (Var n) beta => (exists d:D, SOturnst D (altered_Iv D Iv d (Var n)) Ip Ir beta)

  | negSO beta => ~ SOturnst D Iv Ip Ir beta

  | conjSO beta_1 beta_2 => (SOturnst D Iv Ip Ir beta_1) /\ (SOturnst D Iv Ip Ir beta_2)

  | disjSO beta_1 beta_2 => (SOturnst D Iv Ip Ir beta_1) \/ (SOturnst D Iv Ip Ir beta_2)

  | implSO beta_1 beta_2 => (SOturnst D Iv Ip Ir beta_1) -> (SOturnst D Iv Ip Ir beta_2)

  | allSO (Pred n) beta => forall (pred_asgmt: D -> Prop), 

                               SOturnst D Iv (altered_Ip D Ip pred_asgmt (Pred n)) Ir beta

  | exSO (Pred n) beta => (exists (pred_asgmt: D -> Prop), 

                              (SOturnst D Iv (altered_Ip D Ip pred_asgmt (Pred n)) Ir beta))

  end.

 

(This definition uses two functions that I didn't give definitions to, but it's not important for our purposes.)

Then a small example of what I might want to be able to use might be:

Lemma lem : forall (D : Set) (Iv : FOvariable -> D) (Ip : predicate -> D -> Prop) (alpha : SecOrder) (P : predicate),

SOturnst D Iv Ip (allSO P (allSO P alpha)) ->

SOturnst D Iv Ip (allSO P alpha).

But ideally I don't want to have to prove things like this, if there so happens to be a library that does it for me. It's okay if there isn't; was just wondering if someone had already done something like this.

Is there any other information that would help you answer the questions? Thanks for your help.

Kind regards,
Caitlin

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Pierre Courtieu <pierre.courtieu AT gmail.com>
Sent: Thursday, 23 March 2017 11:41:52 AM
To: Coq Club

Subject: Re: [Coq-Club] Second order logic library?

 

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