On unification: Equational theories are not bounded (Q1094131)

We are interested in first-order unification problems and, more specifically, in the hierarchy of equational theories based on the cardinality of the set of most general unifiers. The following result is established in this paper: if T is a suitable first-order equational theory that is not unitary, then T is not bounded; that is, there is no integer \(n>1\) such that for every unification problem \(<s=t>_ T\), the cardinality of the set of most general unifiers for \(<s=t>_ T\) is at most n. Hence, the class of (non-unitary) finitary theories cannot be decomposed into a hierarchy obtained by uniformly bounding the cardinalities of the sets of most general unifiers.