Logic – PA and Consistency of PA with an Added Axiom

axiomsincompletenesslogicpeano-axioms

By Gödel's second incompleteness theorem, no sufficiently powerful formal system can prove its own consistency.

I was wondering what happens if one tries to manually append an axiom stating a formal system's own consistency to an existing formal system.

By the $2$nd incompleteness theorem (assuming the consistency of PA) we can append $\text{Con}(PA)$ to PA to get a consistent formal system which proves (trivially) the consistency of PA. Though this resulting system of course says nothing about itself.

What if instead, we append to $PA$ the following axiom T:

$T:\text{Con}(PA + T)$

The resulting system would seemingly trivially prove its own consistency, having it as an axiom. But also the effort to formally construct this system appears doomed to fail by the $2$nd incompleteness theorem, as it proves its own consistency (and I assume it remains a "sufficiently powerful" formal system as it still contains $PA$).

Where does this go wrong? I assume it is in the attempt to include a self-referencing axiom, though I'm not sure where the issue would lie since formal self-referencing statements aren't intrinsically wrong (as seen in the proof of the $1$st incompleteness theorem).

Best Answer

Actually, whipping up a self-referential axiom isn't difficult at all; the real issue is that doing so in the way you want just produces an inconsistent system.

We can indeed produce a sentence $\varphi$ with the property that, provably in $\mathsf{PA}$, we have $$\varphi\leftrightarrow Con(\mathsf{PA}+\varphi);$$ this is a direct consequence of the diagonal lemma. In particular, $\mathsf{PA}+\varphi\vdash Con(\mathsf{PA}+\varphi)$.

However, $\mathsf{PA}+\varphi$ also proves everything else, that is, $\mathsf{PA}+\varphi$ is inconsistent. This is exactly what the second incompleteness theorem tells us. Specifically, let $\rho$ be the Godel-Rosser sentence for this theory, i.e. "For every $\mathsf{PA}+\varphi$-proof of me there is a shorter $\mathsf{PA}+\varphi$-disproof of me." Reasoning within $\mathsf{PA}+\varphi$, since $\mathsf{PA}+\varphi$ is consistent (remember that $\mathsf{PA}+\varphi$ proves that!) we know that the Rosser sentence must not be provable in $\mathsf{PA}+\varphi$. But this constitutes a $\mathsf{PA}+\varphi$-proof of $\rho$ after all, and so we get a contradiction.