By adding a large cardinal axiom to ZFC, one can prove statements of arithmetic that wasn't provable from ZFC alone. I need a little help understanding exactly how that works.

Here is what I (think I) understand: If LCA is some large cardinal axiom, then any model of ZFC+LCA contains a set which is a model of ZFC, and the existence of such a model implies the consistency of ZFC. Also, there is a Gödel number $a$ for the "conjunction" of all the axioms of ZFC+LCA and a Gödel number $b$ for the statement that ZFC is consistent, and there is an arithmetical relation $R$ that represents "... implies ...", and $aRb$ is provable.

So far so good, but here is what I don't understand: How does $aRb$ and the assumption of LCA interact to produce a new arithmetical theorem? $a$ is a number and thus cannot follow from LCA; nor can $aRb$ be used for modus ponens. In other words: while I understand how there can be provable arithmetical statements that some axioms imply something else, I don't understand how it makes any difference to arithmetic whether those axioms are *actually* adopted.

How does this work? What have I misunderstood?

The way large cardinals provide consistency strength is by producing *models*.

ZFC (in fact, much less) proves the *soundness theorem*: If $T$ has a model, then $T$ is consistent. So consistency statements can be proved in ZFC (or expansions of ZFC) by proving *the existence of models*.

Large cardinals provide one way of doing ths. For instance, reasoning in ZFC+"There is an inaccessible," let $\kappa$ be the first inaccessible. Then $V_\kappa$ is a set, and it's easy to check that it satisfies ZFC. So ZFC+"There is an inaccessible" proves "There is a model of ZFC." This is *not* an arithmetic assertion, but ZFC also proves the soundness theorem, which lets us pass from such an assertion to an arithmetic one.

Similarly, we can show e.g. that if $\kappa$ is the second inaccessible, then $V_\kappa$ satisfies ZFC+"There is an inaccessible" - so ZFC+"There are at least two inaccessibles" proves the consistency of ZFC+"There is at least one inaccessible."

So arithmetic and set-theoretic principles only come into contact directly in the soundness theorem; everything else in this context is purely on the set-theoretic side, building models of the relevant theories, and then we apply soundness at the end.

This is not very different from how working in $\sf ZFC$ we can prove arithmetic statements which we could not prove in $\sf PA$ alone.

For example, "$\sf PA$ is consistent" is an arithmetic statement (in fact $\Pi_1$) which is not provable from $\sf PA$, but easily provable from $\sf ZFC$. This goes even further, since $\sf ZFC$ proves far stronger theories are consistent.

Similarly, $\sf ZFC$ augmented with stronger axioms can prove that even stronger theories are consistent. The obvious example being $\sf ZFC$ itself.

Of course, adding large cardinal axioms (or any axiom) to an inconsistent theory will not make it consistent. But if $\sf PA$ is inconsistent, then working in $\sf ZFC$ will not make it consistent, it will only mean that $\sf ZFC$ itself is inconsistent. But as long as we cannot prove that $\sf ZFC$ is inconsistent, there is a lot of evidence to the contrary, which means that adding axioms is something of interest.

(The interesting thing would to find "natural arithmetically-looking statements" which have large cardinals implications, like if the negation of the twin-primes conjecture imply the consistency of $\sf ZFC$, or something like that (although that sounds a bit extreme).)