On the soundness and completeness of Equational Predicate Logics

We present two dierent formalizations of Equational Predicate Logic, that is, rst order logic that uses Leibniz’s substitution of \equals for equals " as a primary rule of inference. We prove that both versions are sound and complete. A by-product of this study is an alternative proof to that contained in [GS3], that the \full " Leibniz rule is strictly stronger than the \no-capture " Leibniz rule, this result obtained 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. Introduction. Equational Logic, as proposed by Dijkstra and Scholten [DSc], and propounded in the recent text and papers by Gries and Schneider [GS1, GS2, GS3], is nding its way in Computer Science curricula towards satisfying the \Discrete Math" requirements therein