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.

### Like this:

Like Loading...

*Related*

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.

countV’s behaviour is defined by the following axioms.

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)