Declarations of variables provide implicit universal quantification.Axioms in algebraic specifications are typically intended to be universally quantified over all the (sorted) variables that occur in them. Such quantifications may be given explicitly in CASL, with variables of particular sorts declared for use in individual formulae.
It is also possible in CASL to abbreviate universal quantifications that are common to different axioms, by giving variable declarations separately, as items of basic specifications. The effect of such a variable declaration is implicit universal quantification with that variable of all the axioms of the enclosing basic specification; but variable declarations do not contribute to the signature determined by the specification, so they do not affect other axioms.
Quantification over variables that do not occur (freely) in a formula is always semantically irrelevant in CASL, since models with empty carriers are not allowed. Thus one may also regard the implicit quantification as being limited to the freely-occurring variables.