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.

翻译：我们定义了一种谓词逻辑的扩展，称为绑定逻辑，其中变量可以在项和命题中被绑定。我们为该逻辑引入了模型的概念，并证明了其可靠性与完备性定理。该定理通过将这种逻辑编码回谓词逻辑，并利用经典谓词逻辑的可靠性与完备性定理来获得。