So... you want $M$ to be hereditarily finite in some larger (non-standard) extension?

@AsafKaragila I don't think that's quite it. The elements of $M$ can still be infinite in the extension, but they will all be in $H$, a finite set. So $H$ will not be hereditary finite either.

Uh, no. The inclusion will be an injective map from any $S\in M$ into $H$, so it will be finite.

@AlexKruckman looks good.

@AsafKaragila But the infinite elements of $M$ will also be bigger in the extension, I think. For example, if a set whose elements are $\mathbb N$ is in $M$, then in $M'$ that set will also contain nonstandard integers. Also, since it is an elementary extension, whether or not a given set is finite will have the same answer in both models.

You want to extend the model in a way that there is a finite set that contains every set from the original model. In particular, every set in that model is a subset of the finite set. You're confusing intension and extension.

@AsafKaragila Well, if $M$ says one of it elements are infinite, $M'$ will also say its infinite. Whether or not this is true outside the models, I do not know.

No, it won't. Or the theory you describe is inconsistent. Those are the options.

@AsafKaragila I think PyRulez is right here - maybe you've misunderstood what $M'$ and $Z_M(H)$ are supposed to be. Let $M$ be a model of ZFC. Then there is a partial type $p(x)$ with parameters from $M$ (PyRulez calls this type $Z_M(H)$) given by $\{"x \text{ is finite}"\}\cup \{m\in x\mid m\in M\}$. This type is consistent by compactness, since any (meta) finitely many elements of $M$ are contained in an element of $M$ that $M$ thinks is finite. So it is realized by a set $H$ in an elementary extension $M\preceq M'$. Since this is an elementary extension, $\omega^{M'} = \omega^{M}\in H$.

@AsafKaragila The theory is definitely not inconsistent since it is modeled by a bunch of theories. Models can not model inconsistent theories. The reason that the infinite elements of $M$ will not be subsets of $H$ in $M'$ is that in $M'$ they will contain nonstandard elements. These nonstandard elements will not be in $H$.

@Alex: But also $\omega^M\subset H$, since for every element of it, it will be in $H$. So if $H$ is finite, it means what?

@AsafKaragila I don't know how to make sense of the statement $\omega^M\subset H$, since they live in different models. What's true is that $(\omega^{M'}\cap M)\subseteq H$, but $\omega^{M'}\not\subset H$. From the point of view of $M'$, $H$ is finite, but not hereditarily finite.

@Alex: You literally told me that $\omega^M=\omega^{M'}$, so I don't know what to make of this new comment of yours...

@Asaf: Sorry, let me try again. We have $M\preceq M'$. As elements of these models, $\omega^M = \omega^{M'}$. But of course there are new elements $n\in M'\setminus M$ such that $M'\models n\in \omega^{M'}$. When you write $\omega^M\subset H$, I'm not sure whether to interpret this as "every element of $\omega^M$ in $M$ is in $H$" (which is true) or "every element of $\omega^M = \omega^{M'}$ in $M'$ is in $H$" (which is false).

@AsafKaragila It is also impossible to prove that infinite elements of $M$ are subsets of $H$ in $M'$, since that would require invoking an infinite number of axioms (since each element of $H$ is given its own axiom).

@Asaf Maybe we're talking past each other, if so I apologize. I guess my point comes down to (1) $M$ is an (external) subset of $M'$, not an internal subset, (2) there are elements of $M$ which $M'$ believes are infinite, like $\omega$. So it doesn't make sense to say "$M$ is hereditarily finite in $M'$". What is true is that there's an element $H$ which $M'$ believes is finite, and such that every element of $M$ is an element of $H$. So $M$ is a (non-definable) subclass of a finite set in $M'$.

@AlexKruckman I think the source of the miscommunication is that even though the elements of $M$ are also in $M'$, $\in_M$ is not the same as $\in_{M'}$.

@Alex, PyRulez: Let me understand it, then. $\omega^M=\omega^{M'}$, and for every $x\in M$, including all those $x\in\omega^M$, $x\in H$ and $H$ is finite. So $\omega\subseteq H$. But $H$ is finite. Yes?

@Asaf Maybe we're using the notation $\omega^M$ differently? To me, the statement $\omega^M = \omega^{M'}$ means that the set called $\omega$ in $M$ is equal to the set called $\omega$ in $M'$ (which follows immediately from the fact that $M'$ is an elementary extension). But also $M'$ must have new natural numbers that aren't in $M$ (otherwise we would have $\omega^{M'}\subseteq H$ and $H$ finite, which really would be a contradiction). These two statements are not contradictory, since $M$ is not a transitive submodel of $M'$.

The sequence of symbols $\omega\subseteq H$ means $\forall x\, (x\in \omega\rightarrow x\in H)$. This formula is false in $M'$, because $H$ is finite. But it is true that for each natural number $n$ in $\omega\cap M$, we have $n\in H$, and we even have $\omega\in H$ and much more. There must be enough new natural numbers in $M'$ to accomodate this and still allow $H$ to be finite. (All these assertions are just me unwinding the definition of what it means for $H$ to realize that consistent type $p(x)$ in an elementary extension $M'$...)

@AsafKaragila it may help if you label which sub set relation you are talking about: the meta one, the one in $M$, or the one in $M'$.

@PyRulez: Of course, the one in $M$ or $M'$ (which doesn't matter if it's the same thing in the two modesl).

@AsafKaragila This comments section is getting very long. It's probably better to continue the discussion in chat, if you're interested in doing so (but I haven't used chat very much, so I'm not exactly sure how to do that).

@Alex: It's better to finish this discussion over beer, perhaps someday.

@AsafKaragila in general, all three will different.

@AsafKaragila I'll happily take you up on that.

@PyRulez: You can't in a single breath claim that $\omega$ is not changed, and then claim that it is. If $\omega$ is the same object, in the same that it is the same set, with the same elements, then $\in^M\restriction\omega^M=\in^{M'}\restriction\omega^{M'}$. Other than this, I have nothing more to add.

@AsafKaragila it's the same object, but it has different elements in M and M' since they have different $\in$ relations.

Then in what sense it's the same object????

@AsafKaragila You have to remember that $M$ and $M'$ don't necessarily represent their elements using corresponding sets from the meta theory. For example, let's say that $M$ has an element $\{1,2,3\}$, which it proves to be $\mathbb N$. This is not a contradiction because the claim is made using $\in_M$, not $\in$. There would still exist infinitely many elements $x$ of $M$ such that $x \in_M \{1,2,3\}$, despite $x \notin \{1,2,3\}$. And there might be elements such that $x \notin_M \{1,2,3\}$ but $x \in_{M'} \{1,2,3\}$. The actual elements of $\{1,2,3\}$ don't matter at all.

@AsafKaragila In particular, $M$ and $M'$ probably are not standard models. If they were, you'd be absolutely correct.

@PyRulez: This has nothing to do with being standard or not. This can be $\varnothing$ for all I care. There are $E$ and $E'$. And when you tell me that $\omega^M=\omega^{M'}$, then you are effectively telling me not only that it's essentially the same object, but that the inclusion map (or whatever canonical embedding you want to think of in this case) is witnessing that they are the same.

@AsafKaragila They are represented by the same object in the meta theory, but are treated differently in the two models. For example, if $x \in_{M'} Y$, but $x$ is not an element of $M$, then obviously you can not have $x \in_M Y$, because $x$ is not even in the "domain" of $\in_M$, so to speak.

@PyRulez The last point in your question isn't right: $H$ can't be closed under the successor function, because ZFC proves that any set containing $0$ and closed under successor is infinite. $H$ will contain all of the natural numbers in $M$, but there will be a greatest natural number in $M'$ which is an element of $H$ (because it is finite).

What's true is that $H$ will have a sub-class (namely $M$) which is closed under all definable functions. This sub-class is necessarily not a set in $M'$.

@AlexKruckman oh, whoops. I'll edit it out then (unless someone else does).

@AsafKaragila Since $M$ is an elementary submodel of $M'$, the definition "the first infinite ordinal" will denote the same element in $M$ and in $M'$. Call this element $\omega$. Furthermore, again by elementarity, for any $x\in M$, we'll have that $x\in_M\omega$ iff $x\in_{M'}\omega$. But that's only for $x\in M$; there are lots of $x\in M'-M$ that are $\in_{M'}\omega$ but it doesn't even make sense to ask whether they're $\in_M\omega$. So it's not true that $\omega$ has the same elements in $M'$ as in $M$.

@PyRulez Does my answer resolve your question?