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.
Best Answer
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
\begin{equation} \vdash_\mathcal{S} \mathscr{A} \quad \Rightarrow \quad \vdash_\mathcal{T} \mathscr{A}^\star. \end{equation}
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 \begin{equation} \mathscr{B}^+ :\equiv (\mathscr{B}^\mathsf{R})^\star \end{equation} 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 \begin{equation} \mathsf{Con}_X :\equiv \neg \exists x \, \mathsf{Prf}_X(x,\overline{\ulcorner \Lambda_X \urcorner} ), \end{equation} 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 \begin{equation} \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}), \end{equation} by existential generalization therefore \begin{equation} \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}), \end{equation} which is the same as \begin{equation} \vdash_\mathsf{PA} \neg \mathsf{Con}_\mathcal{U} \Rightarrow \neg \mathsf{Con}_\mathcal{T}. \end{equation} 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}$.