The purpose of this chapter is twofold. On the one hand, it introduces basic notions from universal algebra (such as terms, substitutions, and identities) on a syntactic level that does not require (or give) much mathematical background. On the other hand, it presents the semantic counterparts of these syntactic notions (such as algebras, homomorphisms, and equational classes), and proves some elementary results on their connections. Most of the definitions and results presented in subsequent chapters can be understood knowing only the syntactic level introduced in Section 3.1. In order to obtain a deeper understanding of the meaning of these results, and of the context in which they are of interest, a study of the other sections in this chapter is recommended, however. For more information on universal algebra see, for example, [100, 55, 173].

Terms, substitutions, and identities

Terms will be built from function symbols and variables in the usual way. For example, if f is a binary function symbol, and x, y are variables, then f(x,y) is a term. To make clear which function symbols are available in a certain context, and which arity they have, one introduces signatures.

Definition 3.1.1 A signature Σ is a set of function symbols, where each f ∈ Σ is associated with a non-negative integer n, the arity of f. For n ≥ 0, we denote the set of all n-ary elements of Σ by Σ(n). The elements of Σ(0) are also called constant symbols.