Completeness of many-sorted equational logic.

*(English)*Zbl 0602.08004The 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’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

##### MSC:

08B05 | Equational logic, Mal’tsev conditions |

03C05 | Equational classes, universal algebra in model theory |

03B50 | Many-valued logic |