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").
(1995-02-21)