Variables (scopes, quantification,...)

[Jazzpirate]

Possible approach 1: Variable declarations

• \vardecl[name=N,type={\NaturalNumbers}]{varN}{N} (syntax analogous to \symdef, see Symbolic notations #3) introduces a macro \varN for the variable N, and behaves exactly like a semantic macro,
  i.e. in mathmode, $\varN$ simply yields "N" (its notation), in textmode it takes 0 {}-arguments and one optional []-argument:

=> \implication*[2]{\even{\varN[A \NaturalNumbers[natural number] $\varN$]}[ is even]}[, if]{\even{\natpow{\varN[its]}*{2}[ square]}[ is even]}

Possible approach 2: Scope environments
Can optionally declare variables, e.g. \varscope([name=name, type=t, notation=not, (universal|existential)])*{...} - with everything optional. If an occuring variable is not "declared in a \varscope, its scope is the most inner \varscope in which it occurs. A variable occurence is whatever LaTeXML's math parser considers a variable, or a \var{name} (for not explicitly declared variables in text, e.g. "its" in the example), or \name if a variable with name name is declared in the current \varscope, e.g.:

\varscope{\implication*[2]{\even{\var{N][A \NaturalNumbers[natural number] $N$]}[ is even]}[, if]{\even{\natpow{\var{N}[its]}*{2}[ square]}[ is even]}}

or

\varscope[name=varN, type=\NaturalNumbers, not=N]{\implication*[2]{\even{\varN[A \NaturalNumbers[natural number] $N$]}[ is even]}[, if]{\even{\natpow{\varN[its]}*{2}[ square]}[ is even]}}

Advantage: compatible with fewer explicit annotations, scope still has to be provided, though

Disadvantage: might require an additional \apply-operator for applications of (function) variables, but we probably can't avoid that anyway.