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 $\mathbb{N}$, 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?
On
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.
On
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.
On
You are right (in your comments) that "we know PA is consistent" is actually not because there is an absolute proof/justification of that claim. However, it is very misleading to think that PA's consistency is of the same kind of question as ZFC's consistency.
Firstly, numerous empirically verifiable statements about the natural numbers (via some encoding in physical medium) can be and have been proven using no more than PA, such as Fermat's little theorem, which implies the correctness of HTTPS encryption and decryption, which you are using right now to read this webpage. In this sense, there seems to be a rather concrete interpretation of PA in the real world, at least an approximate one (even if it fails beyond some huge size). So even if PA has no exact interpretation in the real world, we may never observe a failure of PA in the form of an explicit proof that $0=1$ (because there is no short proof of it). Thus in some sense consistency of PA can be justified empirically based on the real world.
On the other hand, ZFC does not enjoy similar ontological or empirical status, except for the fact that it can capture elegantly what mathematicians have been doing for centuries and no inconsistency has been found in ZFC (this is somewhat empirical). It seems there is no non-circular justification of ZFC as a whole. For example, if you use the cumulative hierarchy and take the powerset operation and iteration for granted, you still cannot justify full replacement (see here). If you treat the universe as open-ended, you may be able to obtain some replacement but then you would be unable to justify unbounded specification or unbounded replacement (because you cannot justify well-definedness of quantification over an unfinished universe).
Secondly, consistency is far from what mathematicians really want to have. ZFC+¬Con(ZFC) is consistent, and can prove everything that ZFC can, but everyone (rightly) rejects it, because it is unsound (and worse still proves itself inconsistent). Likewise, even if ZFC is consistent it may be unsound. Some logicians have doubts.
And there is another aspect to this soundness issue. There is no real hope of being able to define "soundness" itself non-circularly, unless we restrict to just "arithmetical soundness". The reason for this is, again, that the natural numbers suitably encoded appear to be the only concrete real-world collection of entities that we can make and test various predictions about. And we of course don't want to have a foundation for mathematics that proves false statements about them! If a first-order theory $S$ is consistent, $S$ does not prove any false $Π_1$ statement (arithmetical sentence with at most $1$ unbounded $\forall$-quantifier in Skolem normal form), but may still prove a false $Σ_1$ statement (with merely $1$ unbounded $\exists$-quantifier). (For example, ZFC+¬Con(ZFC) proves a false $Σ_1$ statement.) So once more we see that PA has a privileged role in the foundations of mathematics.
Thirdly, the fact that ZFC is elegant and virtually all mathematics can be expressed and proven in it does not imply that ZFC is 'more likely' to be 'correct' or even just arithmetically sound. This is because there are other incompatible foundational systems that can also express and prove virtually all mathematics. In other words, large parts of each powerful foundational system simply has no relevance to ordinary mathematics. Just for example, Dmitry Mirimanoff introduced well-foundedness and rank of sets, but never considered all sets to be well-founded, contrary to the regularity axiom in ZFC. And not only does mathematics outside of set theory never use regularity, it cannot be justified to be true of all collections (in any reasonable sense). Furthermore, logicians have investigated non-well-founded set theories as alternative foundations, such as Aczel's axiom and Quine's NF[U] set theory.
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. This is just like how we go outside of PA-formalizable mathematics to prove the consistency of PA (say, working in ZFC), except that PA-formalizable mathematics is a much smaller and relatively uncontroversial subset of mathematics. Thus it is a common view that the consistency of PA is a settled fact whereas the consistency of ZFC is conjectural. (As I mentioned in a comment, as a gross oversimplification, “settled mathematical truth (amongst mainstream classical mathematicians)” roughly corresponds to “provable in ZFC”... Con PA is whereas Con ZFC is not.)
As for proving the consistency of ZFC, 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. 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, and since you’ve made stronger assumptions, you’re at a higher “risk” of inconsistency.