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.