Specificability and Characterization of Equational Classes

We have seen in chapters 2 and 3 that a specification SPEC defines the class Alg(SPEC) of algebras for that specification. We have been able to single out a specific isomorphism class of algebras, the initial algebras, which due to their properties of being generated and typical can serve as favorite candidates for semantics of specification. That we could do so, is intrinsically a property of equations which we used as axioms in specifications. One could think of axioms other than equations, and allow Horn-clauses or even arbitrary first order formulas. It is indeed not obvious that initial algebras exist as models of a specification, and it is even possible to show that with arbitrary first order formulas as axioms aninitial algebra in the defined class of models not always exists.