A variable declaration VAR-DECL determines sorted variables for use in axioms; it does not contribute to the signature. Such a declaration of a variable as a BASIC-ITEM abbreviates adding a universal quantification on that variable to all axioms in the enclosing BASIC-SPEC. 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.VAR-DECL ::= var-decl VAR+ SORT VAR ::= SIMPLE-ID