For some context: I'm currently taking a course of Formal Methods and Logics and there's a passage where we show that the monadic second order ($\text{MSO}$) theory of (possibly labelled) linear orders is decidable. We introduced the question by saying what we intend for linear order, which can be seen as an interpretation of the language:
$$\{\le^{(2)},X_1^{(1)},...,X_n^{(1)}\}$$
But then we continued by saying that "we will show that for each formula $\phi \in \text{MSO}(\{\le\})$ with free monadic variables $X_1,...,X_n$ there exists a finite automaton that recognizes its language", etc.
Notice how the symbols $X_1,...,X_n$ are now interpreted not anymore as unary relational symbols of the language (i.e. the labels), but rather as free variables of the formula. I tagged this question with "predicate logic", too, because we could make the same parallel between first-order variables $x$ and constant symbols of the language.
My question is: under what circumstances can we "drop" the symbols from the language and treat them equivalently as free variables? As in:
$$(D^I,\le^I,X_1^I,...,X_n^I)\vDash\phi\quad\to\quad(D^I,\le^I),\,X_i\overset{\sigma}{\mapsto} X_i^I\vDash\phi(X_1,...,X_n)$$
where $I$ is the interpretation and $\sigma$ is its state. My guess is that we did it for convenience, since the proof of the above is by induction over the structural complexity of the formula, which is independent of the number of free variables, whereas we wish to maintain the same language. I hope the question is clear, since I myself am a bit confused. Thanks in advance.