First-order equational logic consists of quantifier-free terms of ordinarYfirst-order logic, with equalitY as the onlYpredicate 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)