How does large cardinal axioms make arithmetical statements provable?

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?

• "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." — That is only if ZFC+LCA is consistent. But if ZFC is inconsistent, I don't see how ZFC+LCA could be consistent anyway. – celtschk Mar 20 '17 at 9:43
• @celtschk: yes, epistemically speaking this is all very circular. But I'm just trying to understand this on a technical level. – Casper Mar 20 '17 at 9:46

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