  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.
