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.

  • 4
    $\begingroup$ It's definitely not necessary to change your meta-language or make any sort of extension of the language of ZFC to carry out this sort of consistency proof. Rather, if our meta-language is ZFC, then we must have some encoding of everything we want to talk about as sets. In particular, the symbols and formulas in the language of $\Gamma$ are encoded as sets (and this "Gödel coding" is much easier to do in set theory than in arithmetic, by the way). $\endgroup$ – Alex Kruckman Feb 7 '17 at 14:38
  • $\begingroup$ @AlexKruckman Maybe I'm using "extension" incorrectly. What I meant is that you need to encode the symbols of $\Gamma$ as sets (that would amount to giving definitions right?) I was using "extension" in this sense, to mean we've defined some new symbols. I didn't know anything about Godel coding, so I read about it. This seems to be a different way proving consistency from what I wrote (no definitions, but numbering), right? Is this the easier way? Also, is what I wrote correct at least in principle? Thanks. $\endgroup$ – stranger Feb 7 '17 at 15:00

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

  • $\begingroup$ Thanks. This is much neater, and I now see why you don't need to extend ZFC, since you're existentially "quantifying away" any particular model. $\endgroup$ – stranger Feb 11 '17 at 12:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.