Incompleteness for Extensions of P A

Generalized Gödel Incompleteness Theorem

If $T$ is a sound primitive recursive axiomatized theory containing $PA$, then there will be a true ${\Pi }_1$-sentence $G_T$ such that $T/⊢G_T$ and $T/⊢\neg G_T$.

Here sound is defined with respective to standard arithmetic model $\mathfrak{A}$.

$\omega$-consistent

Specifically, $T$ is $\omega$-consistent if $T⊢\psi (m)\text{ for all }m\in \mathbb{N}⟹T⊬\neg \forall m\psi (m).$

There is a version of the Incompleteness Theorem which does not involve truth in $\mathfrak{N}$ but requires that $T$ be $\omega$-consistent.

Generalized Gödel Incompleteness Theorem

If $T$ is a $\omega$-consistent primitive recursive axiomatized theory containing $PA$, then there will be a true ${\Pi }_1$-sentence $G_T$ such that $T/⊢G_T$ and $T/⊢\neg G_T$.

There is a version of the sentence $G$ due to Rosser that does not require $\omega$-consistency to establish its independence from $PA$.

Generalized Gödel Incompleteness Theorem (Gödel–Rosser)

If $T$ is a consistent primitive recursive axiomatized theory containing $PA$, then there will be a ${\Pi }_1$-sentence $G_T$ such that $T⊬G_T$ and $T⊬\neg G_T$.

It is possible to formalise the proof of the first half of the Incompleteness Theorem as a proof in $PA$ to obtain $PA⊢\neg Prov(\perp )\to G,\text{written}PA⊢Con(PA)\to G$ Here $\perp$ is an “absurdity” such as $0=1$ or $\phi \wedge \neg \phi$ for some sentence $\phi$. $Prov$ is the provability formula. $G$ is the Gödel sentence. $Con(PA):=\neg Prov(\perp )$ is a sentence interpreted as consistency of $PA$.

This is far from straightforward, see (Smith, 2020, Chapters 20,21). It follows that $PA⊬Con(PA)$ since if $PA⊢Con(PA)$ then $PA⊢G$, contradicting $PA⊬G$ by Gödel’s first theorem. Restating this, for an arbitrary theory $T$, by essentially the same argument:

Second Gödel Incompleteness Theorem

If $T$ is a consistent primitive recursive axiomatized theory containing $PA$, then $T⊬Con(T).$ That is, $T$ is not strong enough to prove its own consistency! Note this also applies to any axioms for set theory!