If $\operatorname{Con}(\mathrm{PA})$, then $\operatorname{Con}(\mathrm{PA}+\operatorname{Con}(\mathrm{PA}))$?

Question

Assume $\newcommand\PA{\mathrm{PA}}\newcommand\Con{\operatorname{Con}}$ that $\PA$ is consistent.

Then we know that $\PA$ cannot prove $\Con(\PA)$. I was wondering. Can $\PA$ prove that $$\Con(\PA) \Rightarrow \Con(\PA + \Con(\PA))?$$

Answer 1

I assume that you mean can we prove from $\newcommand\PA{\mathsf{PA}}\newcommand\Con{\operatorname{Con}}\PA+\Con(\PA)$ the statement $\Con(\PA+\Con(\PA))$.

Th answer is no. We only added one axiom to $\PA$ so our theory is still recursively enumerable, so Gödel's theorem tells us it cannot prove its own consistency.

Note that $$\PA\vdash\Con(\PA)\rightarrow\Con(\PA+\Con(\PA))\iff\PA+\Con(\PA)\vdash\Con(\PA+\Con(\PA)),$$ so the above argument shows that indeed the implication is not provable in $\PA$.

Answer 2

We know from Godels second incompleteness theorem that PA does not prove Con(PA), and if Con(PA) then PA does not prove not(Con(PA)). Therefore Con(PA) is independent of PA so adjoining it leaves the theorey consistent.

Answer 3

$\newcommand\PA{\mathrm{PA}}\newcommand\Con{\operatorname{Con}}$As said above, $\PA \not\vdash \text{Con}(\PA) \rightarrow \text{Con}(\PA + \text{Con}(\PA))$, since by the deduction theorem, we'd get $\PA + \text{Con}(\PA) \vdash \text{Con}(\PA + \text{Con}(\PA))$, which would be bad since $\PA + \text{Con}(\PA)$ is (hopefully) not inconsistent.

However, strangely enough, assuming your proof predicate is a natural one, if $T \supseteq \PA$ is axiomatizable, then $\PA \vdash \Con(T) \rightarrow \Con(T + \neg\Con(T))$. This doesn't run into the same problem as before, since $\PA + \Con(\PA) \vdash \Con(\PA + \neg\Con(\PA))$ doesn't give you $\PA + \Con(\PA) \vdash \Con(\PA + \Con(\PA))$. And after some thought, this is as it should be; if a theory is consistent, then it can't prove its own consistency; so by the second incompleteness theorem, it plus the negation of its consistency should be consistent (and $\PA$ is strong enough to realize this).