Binding logic

Gilles Dowek, Thérèse Hardin and Claude Kirchner, from LPAIR 2002, long version available at Gilles Dowek’s website:

We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and
completeness theorem there.

2 Responses to “Binding logic”


  1. 1 Samuel Gélineau October 7, 2009 at 6:04 am

    Hmm! What would the language corresponding to that logic look like?

    For now, let’s focus on implementing a function counting variable occurrences. Assume the predicate symbol “=” of arity , with the usual equality axioms. Also assume the following (function_symbol : arity) pairs.

    zero : 
    suc  : 
    
    app : 
    lam : 
    
    countV : 
    

    countV’s behaviour is defined by the following axioms.

    countV(x x) = 1
    countV(x y) = 0
    countV(x app S T) = countV(x S) + countV(x T)
    countV(x lam(y S)) = countV(x S)
    
  2. 2 Samuel Gélineau October 7, 2009 at 6:08 am

    Hmm! What would the language corresponding to that logic look like?

    For now, let’s focus on implementing a function counting variable occurrences. Assume the predicate symbol “=” of arity ⟨0, 0⟩, with the usual equality axioms. Also assume the following (function_symbol : arity) pairs.

    zero : ⟨⟩
    suc : ⟨0⟩

    app : ⟨0, 0⟩
    lam : ⟨1⟩

    countV : ⟨1⟩

    countV’s behaviour is defined by the following axioms.

    countV(x x) = 1
    countV(x y) = 0
    countV(x app S T) = countV(x S) + countV(x T)
    countV(x lam(y S)) = countV(x S)


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: