How many variables in formal logic?

Remark: I assume the equality symbol „$=$“ with its standard semantics to always be included in first-order logic.

Suppose we want to formalize some first-order theory. For our first-order language, we need to fix some set of variables and some set of contstants, e.g. one constant in group theory and Peano arithmetic, no constant at all in ZFC. The choice of a set of constants is most often done quite canonical.

Also, the cardinality of the set of constants can have a direct influence on semantics. For if the set of constants has cardinality $\kappa$ and we add for any two distinct constants $c,d$ the axiom $c\neq d$, each model must have at least cardinality $\kappa$.

What consequences does the choice of the set of variables have?

I can think of these two cases:

• One usually takes an at least infinite set of variables to be able to nest arbitrary many quantifiers. Example: Let $P$ be a 1-ary predicate and $F$ be a 2-ary function, then the formula $$ \forall x_1 \forall x_2 \forall x_3 \dots \forall x_n : P(F(x_1,F(x_2,F(x_3, \dots ,F(x_{n-1},x_n)))))$$ does only make sense, if one has at least $n$ distinct variables.
• If one has at least $n$ distinct variables, one can add axioms like $$ \exists^{\ge n} x : P(x) \qquad \text{or} \qquad \exists^{\le n} x : P(x)$$ which imply each model to contain at least $n$ or at most $n$ elements.
• If one wants to enumerate the set of all strings and do some gödelian reasoning, one must only take a countable set of variables.

Do you know any more cases, where the cardinality of the set of variables does matter? Does it, as long as it is infinite, affect the class of models for our formal theory?

from Hot Weekly Questions - Mathematics Stack Exchange