Variables vs. Constants, how are they defined in ZFC, and how they differ? The other day I was thinking that whenever I'm presented in Uni with constants my teachers use letters like $c$, $k$, $n$, $a$, $b$, etc, and when encountered with variables they use letters like $x$, $y$, $z$, $w$, etc. However, these are only labels, there's nothing stopping me from using $c$ as a variable, or $x$ a constant; this led me to ask myself how are constants vs. variables formally defined.
So far, I have only come up with the definition of a constant in a set by reading "Introduction to Set" Theory by Jech and Hrbáček:

According what they say, given a set $A$ and a $0$-ary operation $R$ on $A$, $(∅,a)$, such that $(∅,a)\in R$ and $a\in A$, is a constant and we can call it just $a$.
Nonetheless, I haven't found anything on the book about the formal definition of a variable.
Is my understanding of the definition of a constant correct? Do you know what's the definition of a variable? (if so, could you share it with me?)
Thanks in advance.
 A: "The" language of first-order logic, which ZFC is based on, is a family of languages.

*

*All languages share the same logical symbols:

*

*individual variables: $x_n$ for each $n \in \mathbb{N}$

*connectives: $\neg, \land, \lor, \to$

*quantifiers: $\exists, \forall$



*and auxiliary symbols:

*

*parentheses: $), ($

*comma: $,$



*Different languages differ in their inventory of non-logical symbols:

*

*individual constants

*function symbols

*predicate symbols



One defines a formal language by listing all members of each category.
For the language of ZFC, it is sufficient to limit oneself to:

*

*individual constants: none

*function symbols: none

*predicate symbols: $\in$
One can add some useful additional symbols, e.g. *

*

*individual constants: $\emptyset$

*function symbols: $\cap, \cup, \wp$

*predicate symbols: $\subset, \subseteq$
Variables and constants are thus defined extensionally by specifying which elements they encompass in a given language; but there is no formal definition of the underlying concept of variables and constants. Remember that variables and constants themselves are just symbols, not mathematical objects; and there are no global regulations on what these symbols need to look like. Though it makes sense in practice to stick to conventions, such as using $x, y, z$ (possibly with indices) for variables and $a, b, c, \ldots$ for constants.
Your understanding of a constant is not entirely correct, though the way it is presented in the text also makes it kind of difficult: We have constant/function/predicate symbols which are interpreted as elements/functions/relations on the domain. The object $a \in A$ would be the interpretation of a constant symbol such as $c$.
Which constants there exist is fixed by specifying the formal language; how they are interpreted is fixed by specifying a structure consisting of a domain of objects and an interpretation function which maps the constant/function/predicate symbols to elements/functions/relations on that domain. This interpretation again has to be defined by explicitly listing which formal symbols map to which object: $\mathcal{I}(c) = a$. A constant is a symbol which by itself is meaningless; its meaning is given by fixing an interpretation which maps it to an element of the domain.
The meaning of variables is given by an assignment function which maps each variable to an element of the domain; again, this assignment needs to be explicitly specified.
The difference between variables and constants is that a variable can undergo different assignments and thus take different values in the same structure under which the formula is evaluated, whereas the meaning of a constant is fixed within a structure.

* though typically these would not be treated as elementary symbols of the formal language whose interpretation needs to be specified in a structure, but rather as abbreviations for some complex expression, e.g. $y = \wp(x)$ is taken as shorthand for $\forall z (z \in y \leftrightarrow \forall u \in z (z \in x)))$ (meaning that the elements of $\wp(x)$ are exactly those sets all of whose members are elements of $x$).
