mjhjmtu

this might be a silly question, but I was wondering: PA cannot prove its consistency by the incompleteness theorems, but we can "step outside" and exhibit a model of it, namely $mathbbN$, so we know that PA is consistent.

Why can't we do this with ZFC? I have seen things like "if $kappa$ is [some large cardinal] then $V_kappa$ models ZFC", but these stem from an "if".

Is this a case of us not having been able to do this yet, or is there a good reason why it is simply not possible?

Using ZFC plus the axiom "Uncountable strong inaccessible cardinals exist" to give a model of ZFC is exactly the same kind of "stepping outside" as when you use ZF to make a model of PA.

The problem is that, unlike the case for PA, essentially all accepted mathematical reasoning can be formalized in ZFC. Any proof of the consistency of ZFC must come from a system that is stronger (at least in some ways), so we must go outside ZFC-formalizable mathematics, which is most of mathmatics. (Just like we go outside of PA-formalizable mathematics to prove the consistency of PA.)

For instance, as you mention, we could go to a stronger system where there is an axiom giving the existence of inaccessible cardinals. Working in Morse-Kelley is another possibility (though this is in a lot of ways pretty similar to positing inaccessible cardinals). In any case, you are in the same position with the stronger system as you were with ZFC: you cannot use it to prove its own consistency.

Of course we can. And we do just that.

To "step outside of $sf PA$" means that you assume the consistency of a far stronger theory, e.g. $sf ZFC$, which lets you construct $Bbb N$ as an object and prove it satisfies $sf PA$.

When you say "assume that $kappa$ is a cardinal such that $V_kappa$ is a model of $sf ZFC$" you effectively saying "We are stepping outside of $sf ZFC$ into a theory "$sf ZFC+varphi$ for a suitable axiom $varphi$, and there we can can find a model of $sf ZFC$.

In fact, when you assume something like $V_kappa$ is a model of $sf ZFC$, you can even find a fairly canonical model of $sf ZFC$: $L_alpha$ for the least $alpha$ satisfying $sf ZFC$, where $L_alpha$ is the $alpha$th step in the constructible hierarchy. As to why it exists, that's another question. But it is there.