Soundness and completeness of the Birkhoff equational calculus for many-sorted algebras with possibly empty carrier sets

Since the many-sorted extension of the Birkhoff equational calculus is unsound when algebras with empty carrier sets are admitted, Goguen and Meseguer proposed a new sound and complete many-sorted equational calculus. This paper presents another approach, alternative to that proposed by Goguen and Meseguer that makes sound and complete the many-sorted extension of the Birkhoff equational calculus. The possibility of maintaining the classical rules is obtained by introducing a new notion of satisfiability, called strong satisfiability. An easier notion of satisfiability called weak satisfiability is also studied, and sufficient and necessary conditions are developed in order to reduce the strong satisfiability to the weak one. In fact, strongly sensible signatures, which generalize sensible signatures introduced by Huet and Oppen, guarantee the equivalence between strong, weak and other usual satisfiabilities. Finally, general conditions for the equivalence of the Birkhoff calculus to the Goguen-Meseguer calculus are established. © 1992