How to prove $\text{Con}(PA + \text{Con}(PA))$ in $ZFC$?

Question

How to prove $\text{Con}(PA + \text{Con}(PA))$ in $ZFC$?

I found an example of this claim here but I'm looking for a more detailed explanation.

An equivalent statement is: there is no proof in $PA$ that $PA$ is inconsistent.

If $PA$ could prove that $PA$ is inconsistent, then $ZFC$ could also prove it, so $ZFC$ would be inconsistent (because $ZFC$ also proves that $PA$ is consistent). But that's not a contradiction since we can't prove that $ZFC$ is consistent anyway (in $ZFC$).

Is there a theory $T$ intermediate in consistency strength, so that $ZFC$ proves that $T$ is consistent and $T$ proves that $PA$ is consistent? That would solve the problem with the above approach (since $PA$ proving its own inconsistency would make $T$ inconsistent which would make a contradiction in $ZFC$).

Answer 1

Well, in ZFC there is a model of PA + Con(PA), namely the natural numbers. Also the soundness theorem (if a theory has a model, it is consistent) is a theorem in ZFC so it is also a theorem of ZFC that the above is consistent.

Edit: I think I understand your approach now. But I don't think it could lead to anything. The problem is that PA+Con(PA) is already a somehow minimal form of such a theory T you are looking for (of course there are way weaker theories that would do it but I don't think they would make anything easier).

Answer 2

The completeness theorem for first-order logic tells us that a theory $T$ is consistent if and only it has a model. Moreover, since $\sf ZFC$ proves the completeness theorem, in order to show that $\sf PA+\operatorname{Con}(PA)$ is consistent, we just need to show it has a model.

But this is not quite what you are asking for. Since $\sf\operatorname{Con}(PA+\operatorname{Con}(PA))$ is a statement about arithmetic, we need to code these things into the natural numbers first.

Luckily, all the usual coding schemes work just fine. So that means that for a theory $T$ with Godel coding, $\sf ZFC$ proves that $\operatorname{Con}(T)$ holds in the natural numbers, if and only if $T$ has a model.

Now, since $\sf PA$ is true in $\omega$, we get that $\sf PA$ is consistent and therefore $\operatorname{Con}\sf (PA)$ is true in $\omega$, and therefore $\sf PA+\operatorname{Con}(PA)$ is true there. So we found a model for our theory, and therefore $\sf\operatorname{Con}(PA+\operatorname{Con}(PA))$ is provable from $\sf ZFC$.