Question about a proof that there is no formula $fin(x)$ Consider the following passage in Just/Weese:

where $fin(x) \equiv $ "$x$ is a finite set".
I'd like to confirm the following with you : requiring "ZFC $\vdash fin(n)$ if $n \in \omega$" is weaker than requiring that "$fin(x) \iff$ $x$ is a finite set", right? There could be a model $M$ of ZFC in which we have an infinite set $x$, that is, there is an injection $\omega \to x$ in real life but $M \models fin(x)$. Is that correct?
And I'd also like to double check my understanding: The problem with question 20 above is that elements in $M$ might be finite sets representing infinite set and the other way around, we can have $\mathbb R \in M$ but in $M$, $\mathbb R$ might stand for the set $n$. So neither $\implies$ nor $\Longleftarrow$ hold in question 20. Correct?
Thanks for your help.
 A: In answer to the question in the first paragraph, you are correct, though it is irrelevant.  Yes, a model $\langle M , E \rangle$ of ZFC could have the property that its version $\varnothing^M$ of the emptyset is actually an infinite set, but what we know for certain is that $$\{ b \in M : b \mathrel{E} \varnothing^M \} = \varnothing,$$ since the emptyset is defined by having the property that $( \forall y ) ( y \notin \varnothing )$.  This Question is really talking about these subsets of $M$ represented by elements of $M$ (as in previous questions).
In regards to your second question, this Question has (virtually) nothing to do with whether an element $a \in M$ that $M$ thinks is finite is actually an infinite set in real life.  It is saying that there is no formula $\phi (x)$ in the language of set theory such that whenever $\langle M , E \rangle$ is a model of ZFC and $a$ is an element of $M$ then 
$$ M \models \phi [ a ] \quad \Longleftrightarrow \quad \{ b \in M : b \mathrel{E} a \} \text{ is finite}$$  (and by "is finite" on the right-hand-side we mean is really finite in the real world).
It appears to me that Just-Weese will be showing that a particular theory extending ZFC will be consistent where there following are new axioms:


*

*$c_k \neq c_\ell$ for distinct $k , \ell$;

*$c_k \in c_0$ for all $k \neq 0$; and

*$\mathrm{fin} (c_0)$.


Then a model $\langle M , E , c_0 , c_1 , \ldots \rangle$ of this theory will also be  a model of ZFC, and $M \models \mathrm{fin} [ c_0 ]$ however the set $$\{ b \in M : b \mathrel{E} c_0 \} \supseteq \{ c_k : k \neq 0 \}$$ is infinite.  (This will be similar to an idea I sketched out in a previous answer.)
