Clearing misconceptions: Defining "is a model of ZFC" in ZFC There is often a lot of confusion surrounding the differences between relativizing individual formulas to models and the expression of "is a model of" through coding the satisfaction relation with Gödel operations.  I think part of this can be attributed to the common preference for using formulas over codings.  For example, a standard proof showing that $V_{\kappa} \models ZFC$ for $\kappa$ inaccessible will appeal to the fact that all of the ZFC axioms relativized to $V_{\kappa}$ are true.  But then one learns about the Lévy Reflection Theorem scheme which allows every (finite) conjunction of formulas to be reflected to some $V_{\alpha}$.  Perhaps this knowledge is followed by a question of whether the Compactness theorem can be used to contradict Gödel's Second Incompleteness Theorem.
Specifically, consider the following erroneous proof that ZFC + CON(ZFC) proves its own consistency:  
Introduce a new constant $M$ into the language of set theory and add to the axioms of ZFC all of its axioms $\varphi_n$ relativized to $M$, denoted $\varphi_n^M$.  Provided that ZFC is consistent, every finite collection of this theory is consistent by the Lévy Reflection Theorem whereby the Compactness Theorem tells us that the entire theory ZFC + "$M \models ZFC$" will be consistent.  Consequently, this theory has a (ZFC) model $N$ so in this model, there exists a model $M$ of ZFC.  To summarize then, arguing in ZFC + CON(ZFC), we've seemingly proven that we have a ZFC model $N$ modeling the consistency of ZFC by virtue of it having the model $M$ (i.e., seemingly $N \models ZFC + CON(ZFC)$ so we would have a proof of CON(ZFC + CON(ZFC)).
The misstep in this proof is of course a misuse of the conclusion of the Compactness theorem, mainly the assumption that such an $N$ will think that $M$ is a ZFC model.  With some enumeration of the formulas of the axioms $\{\varphi_n| n \in \mathbb{N}\}$ of ZFC, it is clear that $N$ will certainly think that $M \models \varphi_n$ for any particular $n \in \mathbb{N}$ analogous to how a nonstandard model of Peano arithmetic has an element $c$ satisfying $c > n$ for any particular $n \in \mathbb{N}$.  The problem of course in the case of $N$ is that there may be formulas with nonstandard indices not accounted for just as there will definitely be nonstandard numbers greater than $c$ in the PA example.
If one were to carry out the same proof with the more tedious arithmetization of syntax, then this link may be more apparent.
To a lesser extent, there may also be confusion with the fact that $0^{\sharp}$ provides us with a proper class of $L(\alpha) \preceq L$.  This may lead to the question of whether $L$ has its own truth predicate, contradicting Tarski's Theorem.  But of course $L$ will only realize that each of these $\varphi^{L(\alpha)}$ is true for any ZFC axiom $\varphi$, and if one attempts to appeal to the arithmetization of syntax, one can begin to see the problem that these $\alpha$ may not (and of course will not) be definable (without parameters) in the constructible universe L.
Since these types of misconceptions can be common among logicians and non-logicians alike, I thought I would ask the highly intelligent mathematicians who have worked through such problems or helped illuminate them to others if they would do so here as well.  I think compiling a collection of tidbits of wisdom in this area from the collective perspectives of the MO Community can be illuminating to all.  As such, my question is as follows:

What insights can you share regarding the questions of formalizing "is a model of ZFC" in ZFC and the various "paradoxes" that arise?

For example, maybe you can show a related seemingly paradoxical problem and resolve it, or simply share your thoughts on how to avoid such traps of logic.
 A: I suspect these sorts of problems arise in two ways: ignoring wrongness (e.g. Skolem's paradox, that there are countable models of set theory which believe in uncountable sets) and ignoring first-orderness: First-order theories with infinite models have models of every larger size; but in any universe there is exactly one isomorphism class of complete ordered field --- being a complete ordered field is NOT a first-order property of the field, but a first-order statement about a thing in some universe.
Contrapositivewise, teaching clearly about these two sorts of phenomena ought to help us keep clear of trouble.  Unless, of course, ZFC proves itself consistent...
A: Here is a result along the lines you are requesting, which
I find beautifully paradoxical.
Theorem. Every model of ZFC has an element that is a
model of ZFC. That is, every $M\models ZFC$ has an element
$m$, which $M$ thinks is a structure in the language of set
theory, a set $m$ and a binary relation $e$ on $m$, such
that if we consider externally the set of objects $\bar
m=\{\ a\ |\ M\models a\in m\ \}$ with the relation $a\mathrel{\bar e}
b\leftrightarrow M\models a\mathrel{e} b$, then $\langle
\bar m,\bar e\rangle\models ZFC$.
Many logicians instinctively object to the theorem, on the
grounds of the Incompleteness theorem, since we know that
$M$ might model $ZFC+\neg\text{Con}(ZFC)$. And it is true
that this kind of $M$ can have no model that $M$ thinks is
a ZFC model. The paradox is resolved, however, by the kind
of issues mentioned in your question and the other answers,
that the theorem does not claim that $M$ agrees that $m$ is
a model of the ZFC of $M$, but only that it externally is a
model of the (actual) ZFC. After all, when $M$ is
nonstandard, it may be that $M$ does not agree that $m$
satisfies ZFC, even though $m$ actually is a model of ZFC,
since $M$ may have many non-standard axioms that it insists
upon.
Proof of theorem. Suppose that $M$ is a model of ZFC. Thus,
in particular, ZFC is consistent. If it happens that $M$ is
$\omega$-standard, meaning that it has only the standard
natural numbers, then $M$ has all the same proofs and
axioms in ZFC that we do in the meta-theory, and so $M$
agrees that ZFC is consistent. In this case, by the
Completeness theorem applied in $M$, it follows that there
is a model $m$ which $M$ thinks satisfies ZFC, and so it
really does.
The remaining case occurs when $M$ is not
$\omega$-standard. In this case, let $M$ enumerate the
axioms of what it thinks of as ZFC in the order of their Goedel numbers. An initial segment of
this ordering consists of the standard axioms of ZFC. Every
finite collection of those axioms is true in some
$(V_\alpha)^M$ by an instance of the Reflection theorem.
Thus, since $M$ cannot identify the standard cut of its
natural numbers, it follows (by overspill) that there is
some nonstandard initial segment of this enumeration that
$M$ thinks is true in some $m=(V_\alpha)^M$. Since this
initial segment includes all actual instances of the ZFC
axioms, it follows that $m$ really is a model of ZFC, even
if $M$ does not agree, since it may think that some
nonstandard axioms might fail in $M$. $\Box$
I first learned of this theorem from Brice Halimi, who was visiting in New York in 2011, and who subsequently published his argument in:


Halimi, Brice, Models as universes, Notre Dame J. Formal Logic 58, No. 1, 47-78 (2017). ZBL06686417.


Note that in the case that $M$ is $\omega$-nonstandard, then we actually get that a rank initial segment $(V_\alpha)^M$ is a model of ZFC. This is a very nice transitive set from $M$'s perspective. 
There are other paradoxical situations that occur with countable computably saturated models of ZFC. First, every such M contains rank initial segment $(V_\alpha)^M$, such that externally, $M$ is isomorphic to $(V_\alpha)^M$. Second, every such $M$ contains an element $m$ which $M$ thinks is an $\omega$-nonstandard model of a fragment of set theory, but externally, we can see that $M\cong m$. Switching perspectives, every such $M$ can be placed into another model $N$, to which it is isomorphic, but which thinks $M$ is nonstandard. 
A: Most of the confusion usually comes from the fact that there is a difference between 
what a model of ZFC believes to be a formula, i.e., an object in the model that satisfies the
definition of a formula applied in the model, and a real world formula.
While every real world formula can be translated into an object in the model, 
not everything that the model believes to be a formula has an analog in the real world.
In particular, not everything that satisfies the definition of being an axiom of ZFC in the model corresponds to a real ZFC axiom.
But this type of problem only arises in non-standard models (with a non-wellfounded set of natural numbers).  However, the completeness theorem and the compactness theorem usually produce non-standard models.
Another source of confusion is the fact that there can be a model of ZFC without there being
any transitive model (or equivalently, any well-founded model)  of ZFC.
The point here is that even though ZFC contains the axiom of regularity which says the 
$\in$-relation is wellfounded, a model of set theory can believe that it is wellfounded while it really is not.  This is due to the fact that from we outside we might see infinite decreasing $\in$-sequences, but the model contains none of them (only the individual elements of such a sequence, but not the sequence itself).
