Journal of Logic and Computation, Volume 11, Issue 4, pp. 623-653: Abstract.
On the Soundness and Completeness of Equational Predicate Logics
Department of Computer Science, York University, Toronto, M3J 1P3 Ontario, Canada. E-mail: email@example.com
This paper is about the elementary metatheory of equational predicate logic-that is, first-order logic that uses Leibniz's substitution of `equals for equals' as a primary rule of inference. We present here two different `faithful' formalizations of this logic and prove that both versions are sound and complete. A by-product of this study is a proof that the `full' Leibniz rule is strictly stronger than the `no-capture' Leibniz rule. We obtain this result here for a complete Logic. We also show that under some reasonable conditions, propositional Leibniz, no-capture Leibniz, and a full-capture version are all equivalent, provided that the latter is restricted to act on universally valid premises whenever capture is allowed.
Keywords: Logic, equational logic, calculational logic, soundness, completeness, Leibniz