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 we prove a completeness theorem for it. This theorem is obtained as a consequence of the completeness theorem of predicate logic, by encoding this logic back into predicate logic using de Bruijn indices and explicit substitutions (Joint work with The're`se Hardin and Claude Kirchner).