On the completeness theorem of many-sorted equational logic and the equivalence between Hall algebras and Bénabou theories. (English) Zbl 1096.03031

Summary: The completeness theorem of equational logic of Birkhoff asserts the coincidence of the model-theoretic and proof-theoretic consequence relations. Goguen and Meseguer, giving a sound and adequate system of inference rules for many-sorted deduction, founded ultimately on the congruences on Hall algebras, generalized the completeness theorem of Birkhoff to the completeness theorem of many-sorted equational logic [J. Goguen and J. Meseguer, Houston J. Math. 11, 307–334 (1985; Zbl 0602.08004)]. In this paper, after simplifying the specification of Hall algebras as given by Goguen-Meseguer, we obtain another many-sorted equational calculus from which we prove that the inference rules of abstraction and concretion due to Goguen-Meseguer are derived rules. Finally, after defining the Bénabou algebras for a set of sorts \(S\), we prove that the category of Bénabou algebras for \(S\) is equivalent to the category of Hall algebras for \(S\) and isomorphic to the category of Bénabou theories for \(S\), i.e., the many-sorted counterpart of the category of Lawvere theories, hence that Hall algebras and Bénabou theories are equivalent.


03C05 Equational classes, universal algebra in model theory
18C10 Theories (e.g., algebraic theories), structure, and semantics
08B05 Equational logic, Mal’tsev conditions


Zbl 0602.08004