### 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. 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. 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)