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.
Best Answer
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:
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.