Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 11, Issue 4, pp. 623-653: Abstract.

On the Soundness and Completeness of Equational Predicate Logics

George Tourlakis

Department of Computer Science, York University, Toronto, M3J 1P3 Ontario, Canada. E-mail: gt@cs.yorku.ca

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

  Full-Text PDF  (287 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.