logic First-order equational logic consists of

quantifier-free terms of ordinary first-order logic, with

equality as the only predicate symbol. The model theory

of this logic was developed into Universal algebra by

Birkhoff et al. [Birkhoff, Gratzer, Cohn]. It was later made

into a branch of category theory by Lawvere ("algebraic

theories").