Is Gödels second incompleteness theorem provable within peano arithmetic?

Question

All following notation and assumptions follow Gödel's Theorems and Zermelo's Axioms by Halbeisen and Krapf.

Exercise 11.4 c) states "Conclude that the Second Incompleteness Theorem is provable within PA."

As the Second Incompleteness Theorem is stated as $\text{PA} \not\vdash \neg \text{prv}(\lceil 0=1 \rceil)$, I interpret the stated conclusion as the statment $\text{PA} \vdash \neg \text{prv}(\lceil{\neg \text{prv} (\lceil{0=1}\rceil)\rceil}).$

I could not find a proof of this fact. However, I think I managed to prove the opposite. But since this directly contradicts the authors, I am not sure if I am correct.

My solution:

Amongst others, recall the following from the book:

• The axiom scheme $(L1)$: $\varphi\rightarrow(\psi\rightarrow \varphi)$
• The tautology (G): $\vdash(\varphi\rightarrow \psi)\leftrightarrow(\neg\psi\rightarrow \neg\varphi)$.
• Löb's Theorem states that if $\varphi$ is an $L_{\text{PA}}$-sentence, then $\text{PA}\vdash \text{prv}(\lceil \varphi \rceil) \rightarrow \varphi$ implies $\text{PA} \vdash \varphi$.

We assume by contradiction that $\text{PA} \vdash \neg \text{prv}(\lceil{\neg \text{prv} (\lceil{0=1}\rceil)}\rceil)$. Then by (L1) and Modus Ponens we can derive $$\text{PA} \vdash \text{prv}(\lceil{0=1}\rceil) \rightarrow \neg \text{prv}(\lceil{\neg \text{prv} (\lceil{0=1}\rceil)}\rceil)$$ or equivalently (by (G)) $$\text{PA} \vdash \text{prv}(\lceil{\neg \text{prv} (\lceil{0=1}\rceil)}\rceil) \rightarrow \neg \text{prv}(\lceil{0=1}\rceil).$$ But by Löb's Theorem we then obtain $\text{PA} \vdash \neg \text{prv}(\lceil{0=1}\rceil)$ which contradicts the Second Incompleteness Theorem. Therefore, $\text{PA} \not\vdash \neg \text{prv}(\lceil{\neg \text{prv} (\lceil{0=1}\rceil)}\rceil)$, i.e. the Second Incompleteness Theorem is not provable within $\text{PA}$

Do you know of a way to prove the original statement (i.e. solve the exercise)? Do you see any mistake in my proof? Do you agree with me? Any insight is appreciated.

Answer 1

This is a common confusion, and in particular Halbeisen/Krapf messed it up here (either Exercise 11.4(c) or Theorem 11.1 needs to be rephrased). The same confusion happens around the first incompleteness theorem G1IT; since it's a little easier to state, I'll treat it first.

---

The general-and-conditional statement of G1IT is as follows:

$(\star)\quad$ If $T$ is a consistent r.e. theory interpreting $\mathsf{Q}$ then $T$ is incomplete.

This is almost always what logicians mean when we refer to "the first incompleteness theorem." This is provable in $\mathsf{PA}$. On the other hand, the statement

$(\dagger)\quad$ $\mathsf{PA}$ is incomplete

is not provable in $\mathsf{PA}$ (unless $\mathsf{PA}$ is inconsistent of course). The point is that $(\dagger)$ is not actually an instance of $(\star)$; rather, it is an instance of $(\star)$ together with a further hypothesis, namely $\mathit{Con}(\mathsf{PA})$.

---

The same issue happens with G2IT. While the "general" second incompleteness theorem takes a bit more care to state (see e.g. Willard's self-verifying theories), the following moderately-general version is provable in $\mathsf{PA}$:

$(\star\star)\quad$ If $T$ is a consistent r.e. extension of $\mathsf{PA}$, then $T\not\vdash\mathit{Con}(T)$.

As above, the following is not provable in $\mathsf{PA}$:

$(\dagger\dagger)\quad$ $\mathsf{PA}\not\vdash\mathit{Con}(\mathsf{PA})$.

But this is - again - not a contradiction, since the latter only follows from the former in the further presence of a hypothesis which $\mathsf{PA}$ (hopefully!) doesn't prove.

---

Tl;dr, when people say "The incompleteness theorems are provable in $\mathsf{PA}$" they're referring to the conditional-and-general versions, not the specific incompletenesses about $\mathsf{PA}$ itself. Getting back to the H/K book in question, the right exercise is to show $$\mathsf{PA}\vdash [{\color{red}{\mathit{Con}(\mathsf{PA})\rightarrow}} \mathsf{PA}\not\vdash\mathit{Con}(\mathsf{PA})]$$

(or "$\mathsf{PA}\vdash\mathit{Con}(\mathsf{PA})\rightarrow\neg\mathsf{prov}_{\mathsf{PA}}(\mathit{Con}(\mathsf{PA}))$" if we want to be a bit more careful about distinguishing $\vdash$ from its formalization within $\mathsf{PA}$).