This is based on a related question. I did some further reading to understand the problem. I'm just posting this question to check whether I have correctly understood the solution.
Let's say we are using ZFC as our meta-language (in standard first order logic). We have proven that a theory is consistent iff it has at least one model, and we have defined the satisfaction relation $\models$.
Now we wish to show that some formal theory $\Gamma$ is consistent. To do this, formally speaking, we would need to:
Define the constant, relation and function symbols as sets. Prove each definition describes a unique and existing object (using axioms of ZFC). Define another set $\Gamma$ containing the required axioms of our formal theory.
Also, by doing this, we have extended ZFC with definitions that makes $\mathcal{L}(\Gamma)$ a sub-language of extended-ZFC. This is required for the following.
Derive the axioms of $\Gamma$ as properties of the defined sets. The proof would be in the language of FOL and would be limited to the axioms of extended-ZFC.
Construct a tuple $\mathfrak{M} = \langle \ldots \rangle$ listing the constructed sets. This is a $\Gamma$-structure.
Using the definition of the satisfaction relation, prove that $\mathfrak{M} \models \Gamma$. The proof would again be in the language of FOL and would be limited to the axioms of extended-ZFC.
Thus, there exists a model of $\Gamma$. Therefore, it is consistent.
Am I right in thinking this is all we need to do, formally speaking? I know in practice we only need to do steps 1 and 2.
One important thing I learned is that, in this situation, we must pick a meta-language that allows us to talk about both $\Gamma$ and its model $\mathfrak{M}$.
Note: I am only looking to check my intuition. There may be better ways of proving consistency, but I am wondering whether my naive understanding could also work, and if not, what the problem is.
Update: I realized that one could regard ZFC as our theory instead, and simply define $\Gamma$-symbols in it. Then steps 1 and 2 are sufficient. But in doing so, ZFC is no longer a meta-theory, and so this solution addresses a different problem.