How does Gödel's second incompleteness apply to any theory containing arithmetic?

Question

If I understand correctly, there are two facts proven by Gödel's second incompleteness theorem, for a formal theory containing arithmetic

1) It is possible to express the consistency of the theory with a formula Con by arithmetizing the syntax

2) If the theory is consistent, then it does not prove Con.

What I don't understand is how it can be generalized to the fact that such a theory cannot prove its own consistency. Maybe there are other ways of expressing the consistency of the theory with another formula, which does not require to arithmetize the syntax !

For instance, I don't see why Gödel's theorem implies that ZFC cannot prove that there exists a set which satisfies ZFC (which would imply the consistency of ZFC).

As far as I understand, the key to the second incompleteness theorem is the diagonal lemma, but this assumes an encoding of the formulae into objects of the theory and I don't understand clearly why such an encoding is fundamentally necessary in order to be able to express the consistency.

Answer 1

There are indeed some loopholes in the area of deciding what it should mean for a theory to prove its own consistency. I'm not aware of any that are based on avoiding arithmetization, but how about this fairly blatant cheat:

Define an enumeration of the axioms of ZFC as $\{\varphi_1,\varphi_2,\varphi_3,\ldots\}$. Then ZFC proves the following

Theorem. The theory $$ T = \{ \varphi_n \mid \{\varphi_1,\ldots,\varphi_n\}\text{ is consistent}\} $$ is consistent.

Now, if we believe in ZFC, then the $T$ this theorem speaks about consists of exactly all the axioms of ZFC itself, so arguably ZFC has just proved its own consistency.

If you buff this up with a sufficient amount of smoke and mirrors, it can be made to look quite convincing at first look. But really, it is not much of a "proof" in the sense of "something that convinces a skeptical reader ZFC is actually consistent" -- namely, in order to decode that ZFC is actually the theory $T$ that the theorem speaks about we need to already believe ZFC is consistent. That's just begging the question, though at an interpretative rather than a formal level.

What the Second Incompleteness Theorem really proves is that the theory under consideration cannot prove "the theory whose axioms are enumerated by such-and-such computable function" to be consistent, when "such-and-such computable function" happens to describe the theory itself. If the same set of axioms are specified in some different way, the situation may well be different.

(Note that the problem is not that the theory $T$ as defined above is not recursively axiomatizable -- no matter whether ZFC is consistent, $T$ is either finite or equals ZFC, and in each of those cases the set of axioms is decidable. The problem is just that the theorem's description of the set is not in terms of a decision procedure).

Answer 2

The bulk of your question is unclear: what does it mean to express the consistency of a theory? For example, "$0=0$" is clearly (:P) equivalent to "$PA$ is consistent", in that they're both true statements; but obviously this is silly. So if you want to talk about different ways of expressing consistency, you need to define what such a thing is. (By the way, we can indeed consider different ways to express consistency, and there are interesting differences - especially in weak theories of arithmetic.)

Here's one approach: given a (true recursive) theory $A$ of arithmetic (or set theory, but let's stick with arithmetic for now), we can fix a reasonable ( = recursive and conservative over $A$) theory $T$ describing natural numbers, formulas of arithmetic (as objects in their own right - that is, un-arithmetized), and proofs from $A$ (ditto). We could then say that a sentence $p$ in the language of arithmetic (which is a proper sublanguage of the language of $T$) is a consistency statement if $T$ proves "$p$ iff there is no proof of $0=1$." Of course, this depends on exactly how we build $T$ . . .

---

As to the example of ZFC: Well, first of all, note that it's not at all easy to say "$A$ satisfies ZFC" in the language of ZFC - we need arithmetization! So it's not at all weird that there's a connnection. But moving on. The key is to show, in ZFC, that - if there is a model of ZFC - then the usual arithmetized sentence "$Con(ZFC)$" is true. This is a bit tedious, but not hard at all.

The point is: if we take "ZFC has a model" to be a consistency statement for ZFC, then it actually implies the usual "arithmetized" one.