It is easy to overlook the fact that the existence of a given large cardinal provides us with a true arithmetical statement that would otherwise be false if the large cardinal notion were not consistent with ZFC (See On statements independent of ZFC + V=L ). The arithmetical statement that I'm referring to here is CON(ZFC + large cardinal notion). This is an example of where we use a fact that is *external* to the set of Natural numbers, the existence of the large cardinal, to prove a result that's *internal* to $\mathbb{N}$. If we want a less esoteric statement of looking externally (not using a large cardinal notion) to prove an internal result about the Natural numbers, we can consider Goodstein's Theorem. Goodstein's Theorem states that a certain infinite collection of sequences, almost all of which grow very quickly on some initial segment, eventually descend to 0. The amazing result is that while this fact is not provable in Peano arithmetic, we can give a very simple proof of it in ZFC. In this case, we consider sequences of infinite ordinals to prove a true arithmetical statement representable in PA.

Let me now switch gears a little to say something about large cardinals. Assuming increasingly strong large cardinal axioms opens up the possibility for increasingly complex transitive set models of ZFC and then increasingly complex definable inner models of ZFC. Nevertheless, even if we assume a sufficiently strong large cardinal hypothesis, say the existence of a weakly compact cardinal $\kappa$, the elementary embeddings that arise fix all "small" elements (hereditary size less than $\kappa$ in the domain). I would therefore like to consider nonstandard models of PA that will not be fixed by such embeddings in an effort to make use of the large cardinal assumptions in a meaningful way for revealing internal truth by external examination. In order to avoid asking a rather vague question, let me pose it as follows:

Has anyone considered models of PA of large cardinal size?

As an example of what I have in mind, assume that we have a nonstandard model $M$ of PA of size $\kappa$ containing an unbounded well-order ( See Uncountable nonstandard models of PA ) for $\kappa$ supercompact. Can we use the fact that $\kappa$ is supercompact to reveal any interesting number-theoretic properties true in $M$?