In preceding sections, we dealt with implicit variables declarations by means import commands, bounded quantifiers, etc. In this section, we introduce explicit variable declarations.
An explicit atomic variable declaration is an expression ``Var v ranges over U '', where v is a variable and U a universe name. The universe U is the range (or type) of the variable v . A explicit variable declaration D is a sequence of explicit atomic variable declarations, and Var(D) is the collection of variables in D . For brevity, the adjective explicit is often omitted.
Intuitively, D is a set of explicit atomic declarations, but we do not
forbid re-declarations of the same variable. The range of a variable
v Var(D)
is the range in the last declaration of v in D . In other
words, later declarations of a variable override the earlier ones. One may
use more concise explicit variable declarations, like ``Var
range over U ''.
A variable declaration D covers a syntactic object s if Var(D) contains all free (that is undeclared) variables of s.
As in 3.2.3, we use auxiliary vocabularies of the form , where
is a genuine
vocabulary, V a finite set of variables and each
v
V
is treated as a nullary function, except it cannot be the subject
of an update instruction. We say that a state S of an auxiliary
vocabulary is appropriate for a syntactical object s if all
function names and all free variables of s occur in
Fun(S)
.