## 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.

### MSC:

 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