In the presence of Godel's Completeness Theorem, the 2nd Incompleteness Theorem has the following strictly model theoretic interpretation: if there exists any model at all of (say) ZFC, there also exists a model M of ZFC such that M contains no (internal) model of ZFC. That is the direct model-theoretic translation of: if ZFC is consistent, then ZFC + (ZFC is inconsistent) is consistent.

My question(s): Either 1) Does this model theoretic statement possibly enjoy a "purely" model-theoretic proof? or 2) Is there a good reason not to expect a purely model-theoretic proof of this statement?

Since category theory affords a rich context for studying internalization, perhaps I should substitute "category-theoretic" for "model-theoretic."

[As a graduate student years ago I wondered whether "every model of ZFC contains an internal model of ZFC" would simply run *directly* afoul of the Axiom of Foundation until someone refined my understanding of "internal model" and convinced me that the story couldn't be that simple.]