Model theory question with finiteness

Question

It should be pretty elementary, but I can't really see it.. Cheers to anyone who can help me

Let $\Psi$ be a transitive set that is a model of $ZF$. Then, $a$ is finite if and only if $\Psi \models (\underline{a}\ \text{is finite})$.

Answer 1

[Edit: I address first the original version of the question, where the requirement that $\Psi$ is transitive was not stated. The last paragraph addresses this case.]

As stated, this is false, and it requires too many wrinkles to fix appropriately:

(Assume that) $\mathsf{ZF}$ is consistent, and that $\Psi$ is a model of $\mathsf{ZF}+\lnot\mathrm{Con}(\mathsf{ZF})$. Define $a$ to be the set of natural numbers that code proofs in $\mathsf{ZF}$ of the inconsistency of $\mathsf{ZF}$. It is then the case that (in the true universe of sets) $a$ is the empty set, so it is finite. However, in $\Psi$, the object $\underline{a}$ corresponding to $a$ not only is non-empty, it is in fact infinite, because by assumption $\Psi$ sees a proof of the inconsistency of $\mathsf{ZF}$, and any such proof can be "padded" by adding as many irrelevant deductions as wanted before its conclusion.

On the other hand, any (standard) hereditarily finite set $a$ has a (parameter free) definition that, provably in $\mathsf{ZF}$, is satisfied by a unique set, and that set is hereditarily finite, and we can pick these definitions so they decode correctly in all models $\Psi$ of $\mathsf{ZF}$, in the following sense: Letting $\underline{t}$ denote the unique element of $\Psi$ that satisfies the definition of $t$, we can recursively prove that for any such $a$, say $a=\{b_1,\dots,b_n\}$, where the $b_i$ are pairwise distinct, we have $\Psi\models\underline{a}=\{\underline{b_1},\dots\underline{b_n}\}$, and the $\underline{b_i}$ are distinct in $\Psi$, and $\underline{n}$ is in $\Psi$ the $n$-th natural number and, in $\Psi$, $\underline{a}$ is finite and has size $\underline{n}$.

(The previous paragraph can be further generalized as well. And there are appropriate versions for other theories. For example, any model $\Lambda$ of $\mathsf{PA}$ has an initial segment isomorphic to the true $\mathbb N$, and any $n\in\mathbb N$ has a canonical $\underline{n}$ corresponding to it in $\Lambda$, and all true identities $n+m=k$, $n\times m=p$, etc, hold in $\Lambda$ of these interpretations.)

This being said, in practice there is a very usual case where we can prove the result you mentioned, without needing to assume that $a$ is in any way definable: If $\Psi$ is transitive, and the membership relation of $\Psi$ is the restriction to $\Psi$ of the usual membership relation, then finiteness is absolute between the universe $V$ and $\Psi$. You can indeed prove by induction on $n$ that if $a\in\Psi$, then $|a|=n$ iff $\Psi\models|a|=n$. Note that for this to even make sense one first needs to verify that, among other things, $\omega\subset\Psi$ and that each $n\in\omega$ is in $\Psi$ the $n$-th natural number.