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?

-
Yes, that requirement is weaker. For example it does not exclude $fin(x)\equiv x=x$. – Hagen von Eitzen Nov 23 '12 at 12:49

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:

1. $c_k \neq c_\ell$ for distinct $k , \ell$;
2. $c_k \in c_0$ for all $k \neq 0$; and
3. $\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.)

-
Thank you! (I know that it is irrelevant but since it was the root of confusion of my two last questions I wanted to double-check that I now really understand.) – Rudy the Reindeer Nov 23 '12 at 11:39