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)