Variables for use in terms may be declared globally, locally, or with explicit quantification. Globally or locally declared variables are implicitly universally quantified in subsequent axioms of the enclosing basic specification. Variables are not included in the declared signature.
Note that universal quantification over a variable that does not occur free in an axiom is semantically irrelevant, due to the assumption that all carriers are non-empty.