In model theory, you often add different symbols to the language you're interested in, to prove a result and then go back to the original language to have the theorem you wanted.

To be more precise, here's an example : suppose you want to show that a theory $T$ in a language $L$ with arbitrarily large finite models has infinite models of arbitrarily large cardinality.

You pick a cardinal $\kappa$, add $\kappa$-many new symbols $c_\alpha$ for $\alpha<\kappa$ to the language $L$ to get $L'$. Then you notice that $T\cup\{c_\alpha\neq c_\beta \mid \alpha\neq \beta \in \kappa\}$ is finitely consistent by hypothesis; and so by compactness it is consistent.

Take a model $M$ of $T'$ and consider its $L$-reduct $\tilde{M}$. This is a model of $T$ and it has cardinality $\geq \kappa$ : we added stuff to $L$ to get what we wanted, then removed it to have a theorem about $L$.