Return to Answer

(Although I think it flows better to say "Assuming ZFC + Con(ZFC_ is consistent, ZFC cannot prove "If ZFC is consistent then ZFC+an inaccessible is consistent.")

(Although I think it flows better to say "Assuming ZFC + Con(ZFC) is consistent, ZFC cannot prove "If ZFC is consistent then ZFC+an inaccessible is consistent.")

EDIT: another important takeaway, relating to your comment below (and I think worth incorporating into this answer for completeness), is:

$$\mbox{Forcing is not the only tool for producing models.}$$

If $T$ is a consistent theory extending ZFC, there is no reason to believe that models of $T$ can always be produced from arbitrary models of ZFC by forcing. While forcing is a powerful tool (indeed, one of the very few we have) for proving relative consistency results, the inability of forcing to produce a model of a given theory from an arbitrary model of ZFC is in no way evidence that that theory is inconsistent.

Yet we can have "forcibly measurable" cardinals which are not measurable. So this shows that it's not enough to simply observe that a large cardinal assumption has high consistency strength in order to be certain it can't be forced.

From now on I'll sweep the usual meta-commitments like "ZFC + Con(ZFC) is consistent" under the rug.

Yet we can have "forcibly measurable" cardinals which are not measurable. So this shows that it's not enough to simply observe that a large cardinal assumption has high consistency strength in order to be certain it can't be forced.