in classical logic, atomic propositions (in propositional logic) are either true or false and constants (in first-order logic) take fixed values, assigned once and for all by the interpretation. In modal (and in particular, temporal) logic, the interpretations of these symbols are different from one "world" (state, in the temporal interpretation) to another. In a first-order setting, one still uses ordinary ("rigid") variables so that one can compare values of variables at different states. 
In order to interpret a formula of temporal logic, you have to know which symbols are flexible (assigned values by states) and which are rigid (assigned values by the underlying first-order interpretation, independently of states). That's why in TLA+ you declare every parameter to be either a CONSTANT or a VARIABLE.
If this bothers you, you are not alone, but people seem to prefer writing, say,
(x > 0)
where x is a state variable rather than
\A t \in Nat : x(t) > 0
as you would have to do if you expressed temporal properties in a purely first-order language.
As for quantification, many modal logics only have quantification over rigid variables, such that you can write, for example,
\A n \in Nat : <>(x = n)
but in TLA there is also quantification over state variables (\AA and \EE), used in particular in connection with refinement. In quantifier contexts, the kind of the bound symbol is indicated by the quantifier.
 In theory, rigid variables can be avoided in TLA+: if all variables are assumed to be flexible, one can express that a particular variable x is rigid by writing [FALSE]_x. However, including such a formula in every statement would be exceedingly clumsy.