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?
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).)