Formally proving the consistency of a formal theory

Question

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:

1. 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.

2. 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.

3. Construct a tuple $\mathfrak{M} = \langle \ldots \rangle$ listing the constructed sets. This is a $\Gamma$-structure.

4. 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.

5. 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.

Answer 1

As Alex Kruckman writes in a comment, it is not necessary to change the language of ZFC. We do not need to prove $\Gamma$ in ZFC, and we do not need to specifically define the model $M$, we only need to prove that it exists.

So, working in ZFC, what we need to do is:

1. Write a formula $\phi(N,T)$ of ZFC which expresses "the set $N$ is a model of the theory $T$."

2. Prove that there is a set $M$ which is a model of our particular theory $\Gamma$. In other words, prove $(\exists M)\phi(M,\Gamma)$ for the $\phi$ in step 1. Note that we do not need to "define" $M$ or show that it is unique, we only need to prove that it exists. We do not need to extend the language of ZFC.

3. Prove that the model $M$ from step 2 cannot satisfy any contradictory sentence.

4. Show that if $\Gamma$ was inconsistent then the model $M$ from step 2 would need to satisfy some contradictory sentence.

Parts (1), (3), and (4) are standard results, which do not rely on $\Gamma$ in any special way. These are covered in any reasonable logic textbook, and I would just call them "formalizing first-order logic in ZFC". Only step (2) has to be adjusted to the particular theory $\Gamma$.