# How to prove a generalized version of Gödel's Second Incompleteness Theorem?

Let's start from Gödel's Second Incompleteness Theorem (GST) in the following form:

If $$\mathcal{T}$$ is a consistent, recursively axiomatizable first order theory that contains $$\mathsf{PA}$$ as a subtheory, then $$\not \vdash_\mathcal{T} \mathsf{Con}_\mathcal{T}$$, where $$\mathsf{Con}_\mathcal{T}$$ is some sentence in the formal language of $$\mathcal{T}$$ that states the consistency of $$\mathcal{T}$$.

I suspect that there holds a more general version of this, let's call it GGST:

If $$\mathcal{T}$$ is a consistent, recursively axiomatizable first order theory that can relatively interpret $$\mathsf{PA}$$, then $$\not \vdash_\mathcal{T} \mathsf{Con}_\mathcal{T}$$, where $$\mathsf{Con}_\mathcal{T}$$ is some sentence in the formal language of $$\mathcal{T}$$ that states the consistency of $$\mathcal{T}$$.

Here, I used roughly the following chain of definitions (see e.g. Mendelson, Introduction to Mathematical Logic, Exercises 3.61 - 3.63).

• A theory $$\mathcal{T}$$ can interpret a theory $$\mathcal{T'}$$ iff there is a definitorial extension of $$\mathcal{T}$$ that contains $$\mathcal{T'}$$ as a subtheory.

• Let $$\mathcal{S}$$ be a theory, $$\mathscr{A}$$ a formula in the formal language of $$\mathcal{S}$$ and $$\mathsf{R}$$ a unary function letter not contained in the alphabet of $$\mathcal{S}$$. Then the $$\mathsf{R}$$-relativisation $$\mathscr{A}^\mathsf{R}$$ of $$\mathscr{A}$$ is obtained by "relativising" all quantifications with respect to $$\mathsf{R}$$, i.e. by replacing, in all subformulas of $$\mathscr{A}$$ from the inside out, $$\forall x \mathscr{B}(x)$$ by $$\forall x (\mathsf{R}(x) \Rightarrow \mathscr{B}(x))$$ and $$\exists x \mathscr{B}(x)$$ by $$\exists x (\mathsf{R}(x) \wedge \mathscr{B}(x))$$.

• A theory $$\mathcal{S}^\mathsf{R}$$ is called a relativisation of a theory $$\mathcal{S}$$ iff the theory axioms of $$\mathcal{S}$$ are exactly the $$\mathsf{R}$$-relativised theory axioms of $$\mathcal{S}$$, plus the axiom $$\exists x \mathsf{R}(x)$$, plus the axioms $$\mathsf{R}(\mathsf{c}_i)$$ for all constants $$\mathsf{c}_i$$ of $$\mathcal{S}$$, plus the axioms $$(\mathsf{R}(x_1) \wedge \ldots \wedge \mathsf{R}(x_n)) \Rightarrow \mathsf{R}(\mathsf{f}(x_1,\ldots,x_n))$$ for all $$n$$-ary function letters $$\mathsf{f}_i$$ of $$\mathcal{S}$$.

• A theory $$\mathcal{T}$$ can relatively interpret a theory $$\mathcal{S}$$ iff it can interpret a relativisation of $$\mathcal{S}$$.

In practice, of course, we will have in mind the case where $$\mathcal{S}$$ is $$\mathsf{PA}$$ and $$\mathcal{T}$$ some set theory of our choice, like $$\mathsf{ZF}$$ or $$\mathsf{ZFC}$$, and the relativisation predicate will be given by something like $$\mathsf{R}(x) :\Leftrightarrow x \in \omega$$, where the ordinal $$\omega$$ represents the set of natural numbers.

So my questions are:

• Is GGST true?

• If yes, how can one prove it, given that I accept GST?

• If the proof is to complicated to be sketched here, is there some good reference in the literature I could consult?

Background: In Mendelson loc. cit. and some other logic textbooks I looked at I can only find a proof of GST or similar statements concerning theories of arithmetics; somehow the case where the theory in question is not some immediate extension of a theory of arithmetics (i.e. has a different formal language) tends to be ignored.

• Given an interpretation of the language of arithmetic in some theory $T$ (for example ZFC), let $U$ be the set of those sentences in the language of arithmetic whose interpretation is provable in $T$. If $T$ is consistent, then so is $U$; if $T$ is computably axiomatizable, then so is $U$ (via Craig's trick). PA can prove $\text{Con}_T\to\text{Con}_U$. So by applying Gödel's theorem to the theory $U$ (in the language of PA), you can get the theorem also for $T$. Commented Sep 16, 2018 at 21:12
• @AndreasBlass: But why do we know that PA can prove Con(T) → Con(U)? Commented Sep 17, 2018 at 19:00
• To prove in PA that $\text{Con}_T\to\text{Con}_U$, suppose we had a proof of a contradiction in $U$. Note that the assumptions from $U$ used in this proof become theorems of $T$ when we apply the interpretation (as that's how I defined $U$) and the contradiction at the end of the proof becomes a contradiction. So we'd have a proof of a contradiction from theorems of $T$. Insert the proofs from $T$ of those theorems and we'd have a proof of a contradiction in $T$. Commented Sep 17, 2018 at 21:01
• As far as I can see, these arguments show that we have (i) $\vdash_\text{PA} \text{Con}_T \rightarrow \text{Con}_U$ and (ii) $\not \vdash_\text{PA} \text{Con}_U$, and therefore $\not \vdash_\text{PA} \text{Con}_T$. But is this really the same as $\not \vdash_T \text{Con'}_T$? Commented Sep 18, 2018 at 19:44
• I would assume that "some analogous statement" would be equivalent (provably in $T$) to the interpretation in the language of $T$ of $\text{Con}_T$. Then if $T$ were to prove $\text{Con}'_T$, $U$ would prove $\text{Con}_T$ and therefore also $\text{Con}_U$ (since $U$ includes PA, which proves $\text{Con}_T\to\text{Con}_U$), contrary to Gödel's theorem applied to $U$. Commented Sep 18, 2018 at 21:56

Yes, GGST is true. The proof for this was basically given by @AndreasBlass, see his several very helpful comments above. Here, I give a fuller account of this proof, filling in some details.

First, some preliminaries. In what follows, if $$X$$ is a formal theory, then $$\mathcal{L}_X$$ denotes the formal language of this theory.

Let $$\mathcal{S}$$ be the definitorial extension of $$\mathcal{T}$$ that contains the $$\mathsf{R}$$-relativisation of $$\mathsf{PA}$$ as a subtheory. Any formula $$\mathscr{A} \in \mathcal{L}_\mathcal{S}$$ can be transformed into a certain formula $$\mathscr{A}^\star \in \mathcal{L}_\mathcal{T}$$ with

$$$$\vdash_\mathcal{S} \mathscr{A} \quad \Rightarrow \quad \vdash_\mathcal{T} \mathscr{A}^\star.$$$$

For an exact derivation of this see Mendelson loc.cit., Proposition 2.28(f). Furthermore, for any formula $$\mathscr{B} \in \mathcal{L}_\mathsf{PA}$$, define $$$$\mathscr{B}^+ :\equiv (\mathscr{B}^\mathsf{R})^\star$$$$ and call $$\mathscr{B}^+ \in \mathcal{L_T}$$ the interpretation of $$\mathscr{B}$$ in $$\mathcal{T}$$.

Now, the proof of GGST. Let $$\mathcal{U}$$ be the first order theory in the language of $$\mathsf{PA}$$ formed by exactly those formulae whose interpretations in $$\mathcal{T}$$ are provable in $$\mathcal{T}$$. Note that this theory knows potentially much more about arithmetics then $$\mathsf{PA}$$ does - namely, everything that our theory $$\mathcal{T}$$ can prove. For example, with $$\mathcal{T} = \mathsf{ZFC}$$, Goodstein's theorem would be part of $$\mathcal{U}$$, also it can't be proved in $$\mathsf{PA}$$. In any case, $$\mathsf{PA}$$ is a subtheory of $$\mathcal{U}$$ (since the interpretation of any $$\mathsf{PA}$$-theorem is provable in $$\mathsf{T}$$; remember that $$\mathcal{T}$$ can relatively interpret $$\mathsf{PA}$$).

To formalize the talk about consistency within these theories, we start from the number-theoretic provability relation $$Prf_X(x,y)$$. Here, $$X$$ can be any recursively axiomatizable first order theory, and $$Prf_X(x,y)$$ is defined to be satisfied iff $$x$$ is the Gödel number of a proof in $$X$$ of the formula with Gödel number $$y$$. Since $$X$$ is supposed to be recursively axiomatizable, this is a recursive relation and can hence be syntactically represented in $$\mathsf{PA}$$ by a certain formula $$\mathsf{Prf}_X(x,y)$$ in the language of $$\mathsf{PA}$$. Let $$\Lambda_X \in \mathcal{L}_X$$ be an arbitrary sentence whose negation can be proved in $$X$$ (like $$0 = \overline{1}$$ in $$\mathsf{PA}$$ , or $$\emptyset = \{ \emptyset \}$$ in $$\mathsf{ZFC}$$), and define $$$$\mathsf{Con}_X :\equiv \neg \exists x \, \mathsf{Prf}_X(x,\overline{\ulcorner \Lambda_X \urcorner} ),$$$$ where $$\overline{\ulcorner \Lambda_X \urcorner }$$ is the numeral corresponding to the Gödel number of $$\Lambda_X$$. This sentence is true (in the standard interpretation of $$\mathcal{L}_\mathsf{PA}$$, where the domain of the interpretation is given by the natural numbers) iff $$X$$ is consistent. So we are justified to say that $$\mathsf{Con}_X$$ codifies the consistency of $$X$$ in $$\mathcal{L}_\mathsf{PA}$$. Furthermore, for a theory $$X$$ not in the language of $$\mathsf{PA}$$, but able to relatively interpret $$\mathsf{PA}$$, we might say that the sentence $$\mathsf{Con}_X^+ \in \mathcal{L}_X$$ will codify the consistency of $$X$$ within $$X$$, since this sentence will also be true iff $$X$$ is consistent, at least in any interpretation of $$\mathcal{L}_X$$ where the predicate $$\mathsf{R}(x)$$ is interpreted as "$$x$$ is a natural number".

We will now prove the following three claims:

(1) $$\not \vdash_\mathcal{U} \mathsf{Con}_\mathcal{U}$$

(2) $$\vdash_\mathcal{U} \mathsf{Con}_\mathcal{T} \ \Rightarrow \ \mathsf{Con}_\mathcal{U}$$

(3) $$\vdash_\mathcal{T} \mathsf{Con}_\mathcal{T}^+ \ \Rightarrow \ \vdash_\mathcal{U} \mathsf{Con}_\mathcal{T}$$

Then one can argue as follows: Assume $$\mathcal{T}$$ could prove it's own consistency, i.e. $$\vdash_\mathcal{T} \mathsf{Con}_\mathcal{T}^+$$. With (3) this entails $$\vdash_\mathcal{U} \mathsf{Con}_\mathcal{T}$$, and this leads, with (2) and modus ponens, to $$\vdash_\mathcal{U} \mathsf{Con}_\mathcal{U}$$. But this contradicts (1), so our assumptions must be false and GGST is proved.

Proof for claim (1)

Since $$\mathcal{T}$$ is consistent, so is $$\mathcal{U}$$: By definition of $$\mathcal{U}$$ the proof of any inconsistency in $$\mathcal{U}$$, $$\vdash_\mathcal{U} \mathscr{B} \wedge \neg \mathscr{B}$$, would entail $$\vdash_\mathcal{T} (\mathscr{B} \wedge \neg \mathscr{B})^+$$ and this of course (by the formal definitions of the operators +, $$\mathsf{R}$$ and $$\star$$) means $$\vdash_\mathcal{T} \mathscr{B}^+ \wedge \neg \mathscr{B}^+$$, contradicting the consistency of $$\mathcal{T}$$.

Secondly, since $$\mathcal{T}$$ is recursively axiomatizable, so is $$\mathcal{U}$$. This is not so obvious, though. In fact, we have to employ Craig's theorem to show that: This theorem tells us that any theory whose theorems are recursively enumerable can be recursively axiomatized. And the theorems of $$\mathcal{U}$$ are recursively enumerable: Just make a list of all the theorems of $$\mathcal{T}$$ (that's possible since $$\mathcal{T}$$ is recursively axiomatizable) and check for every theorem in this list whether it is the interpretation of a $$\mathcal{L}_\mathsf{PA}$$-formula or not (this can also be done in a purely mechanical way). If so, add it to the list of $$\mathcal{U}$$-theorems.

So $$\mathcal{U}$$ is a consistent, recursively axiomatizable extension of $$\mathsf{PA}$$. By GST we therefore get $$\not \vdash_\mathcal{U} \mathsf{Con}_\mathcal{U}$$.

Proof for claim (2)

For every proof of a $$\mathcal{L}_\mathsf{PA}$$-sentence $$\mathscr{B}$$ there exists a corresponding proof in $$\mathcal{T}$$ of $$\mathscr{B}^+$$, the interpretation of $$\mathscr{B}$$ in $$\mathcal{T}$$, because that's how we defined $$\mathcal{U}$$. Furthermore, if $$\mathscr{B}$$ is a contradiction, i.e. of the form $$\mathscr{C} \wedge \neg \mathscr{C}$$, then so is $$\mathscr{B}^+$$ (see proof for claim (1)).

Now let $$c$$ be the Gödel number of some supposed proof for a certain contradiction $$\Lambda_\mathcal{U}$$ in $$\mathcal{U}$$, and $$d$$ the Gödel number of the proof of the corresponding contradiction $$\Lambda_T := \Lambda_\mathcal{U}^+$$ in $$\mathcal{T}$$. We then have $$Prf_\mathcal{U}(c,\ulcorner \Lambda_\mathcal{U} \urcorner) \Rightarrow Prf_\mathcal{T}(d,\ulcorner \Lambda_\mathcal{T} \urcorner)$$. Therefore, since $$Prf_X(x,y)$$ is syntactically represented in $$\mathsf{PA}$$ by $$\mathsf{Prf}(x,y)$$, we can conclude that in $$\mathsf{PA}$$ we must have the theorem $$$$\vdash_\mathsf{PA} \mathsf{Prf}_\mathcal{U}(\overline{c},\overline {\ulcorner \Lambda_\mathcal{U} \urcorner } ) \ \Rightarrow \ \mathsf{Prf}_\mathcal{T}(\overline{d},\overline{\ulcorner \Lambda_\mathcal{T} \urcorner}),$$$$ by existential generalization therefore $$$$\vdash_\mathsf{PA} \exists x \, \mathsf{Prf}_\mathcal{U}(x,\overline {\ulcorner \Lambda_\mathcal{U} \urcorner } ) \ \Rightarrow \ \exists y \, \mathsf{Prf}_\mathcal{T}(y,\overline{\ulcorner \Lambda_\mathcal{T} \urcorner}),$$$$ which is the same as $$$$\vdash_\mathsf{PA} \neg \mathsf{Con}_\mathcal{U} \Rightarrow \neg \mathsf{Con}_\mathcal{T}.$$$$ From this, we get claim (2) by contraposition (and using the fact that $$\mathsf{PA}$$ is a subtheory of $$\mathcal{U}$$).

Proof for claim (3)

Since $$\mathsf{Con}_\mathcal{T}^+$$ is the interpretation of $$\mathsf{Con}_\mathcal{T}$$ in $$\mathcal{T}$$, this follows immediately from the definition of $$\mathcal{U}$$.