Why is Gödel's second incompleteness theorem interpreted as "a theory cannot prove its own consistency"?

Question

I'm reading the book Mathematical Logic by Cori and Lascar, in which Gödel's second incompleteness theorem is stated as follows:

Let $T$ be a consistent, recursive theory that extends $\mathcal{P}$. Then $Con(T)$ is not derivable in $T$.

Why is this theorem interpreted as "a theory cannot prove its own consistency"? Since $Con(T)$ is not exactly the same as the consistency of $T$. They are the same notion for $\mathbb{N}$, but not for some non-standard models of $\mathcal{P}$.

Edit: So is the theorem still worth the existential crisis?

Answer 1

I don't agree with the general idea that $\mathrm{Con}(T)$ isn't meaningful in non-$\omega$-models of theories like $\mathsf{PA}$ and $\mathsf{ZFC}$. This is alluded to in some of the discussion of Artemov's paper on FOM, but I think it's worth an answer here, specifically to your question, 'Why is this theorem interpreted as "a theory cannot prove its own consistency"?' The short answer is that $M \models \mathrm{Con}(T)$ really does mean that $T$ is consistent 'internally' inside $M$.

The way in which $\mathrm{Con}(T)$ is meaningful is easier to see in the context of $\mathsf{ZFC}$, but a version of this is true in $\mathsf{PA}$ as well. A really important result in mathematical logic is Gödel's completeness theorem which says that a first-order theory has a model if and only if it is consistent in the sense of a syntactic proof calculus. This fact is of course provable in $\mathsf{ZFC}$, that is to say that $\mathsf{ZFC}$ proves $$\forall T (\mathsf{Con}(T) \leftrightarrow \exists M \models T).$$ What's important here is that any model $M$ of $\mathsf{ZFC}$ is correct about satisfying individual formulas. That is to say, if $A$ is some structure in $M\models \mathsf{ZFC}$, the for any standard formula $\varphi(\bar{x})$ and any $\bar{a} \in A$, $M$ 'thinks' $A \models \varphi(\bar{a})$ if and only if $A \models \varphi(\bar{a})$. For infinite theories the issue of course is that there are now non-standard formulas, but you still get one direction, specifically, if $M \models \mathsf{ZFC}$ thinks that $A$ is a model of a computably enumerable theory $T$, then $A$ is actually a model of that theory.

$\mathsf{PA}$ and $\mathsf{ZFC}$ have the special property that they non-uniformly prove the consistency of any finite fragment of themselves. By a slightly tricky argument, this implies that every model of $\mathsf{ZFC}$ contains what is externally a model of $\mathsf{ZFC}$. In a model of $\mathsf{ZFC}+\neg\mathrm{Con}(\mathsf{ZFC})$, though, there is no way to definably separate these models from models of arbitrarily large finite fragments of $\mathsf{ZFC}$.

With finitely axiomatizable set theories like $\mathsf{NBG}$ or $\mathsf{NFU}$, Gödel's second incompleteness theorem has a far more striking implication. There are, for instance, models of $\mathsf{NFU}$ which contain no models of $\mathsf{NFU}$. $\mathsf{ZFC}$ has a similar phenomenon, which is that there are models of $\mathsf{ZFC}$ which contain no transitive models of $\mathsf{ZFC}$.

The analogous phenomenon with $\mathsf{PA}$ involves the fact that a certain form of the completeness theorem is provable in $\mathsf{PA}$: If a model $N$ of $\mathsf{PA}$ satisfies $\mathrm{Con}(T)$, then $N$ actually interprets the full elementary diagram of a model of $T$. The converse is true as well, so this means that a model $N$ of $\mathsf{PA} + \neg \mathrm{Con}(\mathsf{PA})$ does not interpret the full elementary diagram of a model of $\mathsf{PA}$.

Answer 2

To expand on my comment a bit, and address your edit...

No, it does not justify an existential crisis. Even as typically read, it mainly requires you to adjust your expectations about what can be accomplished with formal system. And it's not clear that the expectations that are dashed really made sense to begin with (like, if a formal system proves its own consistency, is that really a basis for trusting it?).

But, it's also a good example of where un-emphasized assumptions can make an important difference. There is a similar theorem in programming languages, where languages with guaranteed-terminating programs cannot represent their own interpreter. The proof is very similar to the second incompleteness theorem.

However, then this paper was published. Like the Artemov paper, the key point is that the internal representation of program expressions is not collected in a single type, but a family of types given by a schema. Then, the interpreter is schematic as well (see edit). The assumption of a single type of all expressions is not emphasized in the impossibility proof, but it turns out to be essential.

I can't really answer the 'why' of people giving the overly broad interpretations. That is probably more of a psychology and sociology question. Most people teach and learn the prevailing historical narrative on the incompleteness theorems, and aren't interested in how that narrative may not be precisely supported by the formal theorem. It's (relatively) easy to get to the point of understanding why the theorem seems to mean the typical interpretation. To uncover the problem with that interpretation, you have to be further motivated to do so. And as mentioned above, the typical interpretation isn't really a problem, so that alone would be unlikely to motivate someone to dig deeper.

There are other examples where you have to be careful like this. For instance, SAT is an NP complete problem, which people will generally tell you means it's "difficult." However, practical SAT solvers are all the rage these days. Just because the whole problem space is intractable doesn't mean that there can't be techniques for efficiently solving most instances that people actually want. But if you just read the theorem as saying, "this problem can't be solved efficiently," you might not even try.

Edit: I skimmed the Brown-Palsberg paper again, and realized that the interpreter is actually not schematic. The quotation process is schematic, and the type of the quotation of a term will depend on the type of the term. However, there is a single uniform interpreter that can be instantiated to work on any quotation. I think it is also possible to give a type that classifies (an analogue of) every quoted value, as well, but an abstraction theorem would imply that they can no longer be interpreted within the language, basically because the result type of the interpreter would need to depend on the value.