Question

We have numerous statements that are invariant by set forcing, but which are independent of ZFC and even of ZFC + large cardinals. Thus, I dispute the premise of your question. Examples include:

• Eventual GCH. This is the assertion that the GCH holds for all sufficiently large cardinals. This is forcing invariant, by set forcing (see remarks below), since any given forcing notion can affect the continuum function only for cardinals of size less than the size of the forcing. But it is independent of ZFC, since it is implied by GCH and it is easy to use class forcing to produce models with unbounded violations of GCH.

• Eventual non-GCH, or eventual some-other-GCH-pattern. Similarly, we can arrange other GCH patterns just as easily, and as long as the statement is only that the pattern holds eventually, then it will again be independent of ZFC for the same reason.

• The previous examples are also independent of ZFC+ large cardinals, since we can control the GCH pattern while preserving most of the standard large cardinal notions.

• Any kind of eventual statement, about a feature that can be controlled locally by forcing. For example, assertions about the eventual pattern of the existence of $\kappa$-Souslin trees or $\Diamond_\kappa^*$ and so on. These can be controlled by forcing in a class iteration to achieve unbounded patterns, but set forcing can only affect things locally. So the statement that the eventual pattern is such-and-such will be invariant by set-forcing.

• Assertions that there are a proper class of such-and-such large cardinals. These are forcing invariant, because by the Levy-Solovay theorem, the large cardinals above the size of any forcing will be preserved. Thus, the assertion that there is a proper class of inaccessible cardinals, or Woodin cardinals or supercompact cardinals, etc. are all forcing invariant, but we cannot hope to settle these assertions in ZFC, or even with ZFC + very strong large cardinal axioms not of this particular form. For example, it is consistent (from a suitable hypothesis) with a supercompact cardinal (or any other standard large cardinal notion) that there is not a proper class of inaccessible cardinals. It is consistent with an almost huge cardinal that there is a proper class of supercomapct cardinals, and also that there is not (assuming a suitable LC hypothesis).

• The failure of the Ground Axiom. The Ground Axiom, which I introduced with Jonas Reitz, is the assertion that the universe is not a set-forcing extension of any inner model. Despite its second-order nature, it is actually first-order expressible. GA is true in L and forceable over any model of ZFC by class forcing, but once it fails, then of course it remains false in any set forcing extension. So $\neg GA$ is upwards forcing invariant by set forcing. And again, we get the independence here not just over ZFC, but over ZFC + large cardinals.

• There are other similar examples concerning the existence of bedrock models, that is, ground models of the universe that are not themselves forcing extensions of any inner model.

All of these statements are forcing-invariant in the sense you mention, but none of them are settled either way by large cardinal axioms.

Set forcing vs. class forcing. It is important in your example and all my examples above that we are speaking of forcing invariance by set forcing, that is, when the partial order is a set, rather than a proper class. Your example theorem, for example, is true for set forcing, but not for class forcing. In particular, the statement that there is a proper class of Woodin cardinals is itself destroyable by class forcing: one can perform the coding-the-universe forcing that obtains $V[G]=L[x]$ for a real $x$, and there are no Woodin cardinals in $L[x]$.

So you are only talking about forcing invariance for set forcing to begin with. Furthermore, the assertion that "$\varphi$ is set forcing invariant" is first-order expressible for set forcing, but not for class forcing. Thus, it is difficult to formalize or even express any general theory about forcing invariance by class forcing, although one can adopt ad hoc methods for particular statements.