Soundness and completeness of the Birkhoff equational calculus for many-sorted algebras with possibly empty carrier sets (Q1185017): Difference between revisions

This is a useful paper for those interested in many-sorted equational logic. It is well-known that the standard (Birkhoff) rules of equational deduction are not sound in the setting of many-sorted algebras when some carrier sets are allowed to be empty. In fact, even to state the meaning of an equation in such an algebra, the notion of an interpretation must be modified to allow partial maps of the many-sorted set of terms into the algebra \({\mathfrak A}\). Indeed, if the carrier of sort \(s\), \(A_ s\) say, in \({\mathfrak A}\) is empty, there can be no total mapping of the variables of sort \(s\) to \(A_ s\). Thus, the authors consider partial valuations \(\pi: V\to A\), which are allowed to be undefined on a variable of sort \(s\) iff \(A_ s\) is empty. Partial valuations extend in the usual way to partial homomorphisms from the set of terms to the algebra \({\mathfrak A}\). One says that \({\mathfrak A}\) weakly satisfies an equation \(t\equiv t'\) if under each partial valuation both \(t\) and \(t'\) are undefined in \({\mathfrak A}\) or they are both defined and equal. Write \(E\models_ w t\equiv t'\) if whenever \({\mathfrak A}\) weakly satisfies all equations in \(E\), then \({\mathfrak A}\) weakly satisfies \(t\equiv t'\). If we write \(E\vdash_ B t\equiv t'\) to abbreviate the statement that the equation \(t\equiv t'\) is provable from \(E\) using the standard Birkhoff equational logic, then the equivalence \(E\models_ w t\equiv t'\Leftrightarrow E\vdash_ B t\equiv t'\) fails. \textit{J. A. Goguen} and \textit{J. Meseguer} [Houston J. Math. 11, 307-334 (1985; Zbl 0602.08004)] have introduced a different system of equational deduction \((\vdash_{GM})\) in which equations are triples \((X,t,t')\), where \(X\) is a set of variables containing at least \(Var(t_ 1,t_ 2)\), the set of the variables occurring in \(t\) or \(t'\). \textit{G. Huet} and \textit{D. C. Oppen} [Formal language theory: perspective and open problems, Proc. Symp. Santa Barbara/CA 1979, 349-405 (1980; Zbl 0545.68065)] have defined a different notion of satisfiability: \({\mathfrak A}\models_{HO} t\equiv t'\) if for every valuation \(\pi: Var(t_ 1,t_ 2)\to {\mathfrak A}\), the equality \(\pi(t)=\pi(t')\) holds. The present paper considers the relationship among these and other notions of both provability and satisfiability. The authors show, for example, that the following is true: \(E\models_ s t\equiv t'\Leftrightarrow E\vdash_ B t\equiv t'\), where \(\models_ s\) strong satisfiability: an algebra strongly satisfies an equation \(t\equiv t'\) if for all endomorphisms \(\tau\) of the algebra of terms, the algebra weakly satisfies \(\tau(t)\equiv \tau(t')\). There are other results which depend on the nature of the many-sorted signature. The paper is clearly presented, and most proofs are short. However, unless I missed something, there is nothing said about an equational notion of provability equivalent to weak satisfiability.