Completeness of many-sorted equational logic. (English) Zbl 0602.08004

The abstract of this interesting paper best summarizes what it is all about. ”Assuming that many-sorted equational logic ’goes just as for the one-sorted case’ has led to incorrect statements of results in many- sorted universal algebra; in fact, the one-sorted rules are not sound for many-sorted deduction. [The authors provide simple examples of this. Reviewer] This paper gives sound and complete rules, and characterizes when the one-sorted rules can still be used safely; it also characterizes the related question of when many-sorted algebras can be represented as one-sorted algebras. The paper contains a detailed introduction to [P]. Hall’s theory of clones (later developed into ’algebraic theories’ by Lawvere and Benabou); this allows a full algebraization of many-sorted equational deduction that is not possible with the usual fully invariant congruences on the free algebra on countably many generators.”
Reviewer’s comment: The problems that arise in the naive approach stem from the possibility of empty sorts. How logicians might get around this is to add unary predicates; but that avenue is not available in universal algebra.
Reviewer: P.Bankston


08B05 Equational logic, Mal’tsev conditions
03C05 Equational classes, universal algebra in model theory
03B50 Many-valued logic