In his popular book Set Theory: An Introduction to Independence Proofs, Kunen gives the following definitions on the bottom of page 145:
Let $\mathcal{A} = \lbrace A, E \rbrace$ be a structure for the language of set theory. Let also $\mathcal{A} \models ZF$. We call $\mathcal{A}$ an $\omega$-model iff there is no $a \in A$ such that $\mathcal{A} \models “a \in \omega”$ but $a \neq n^{\mathcal{A}}$ for each $n$.
He then proceeds with the following assertion:
If $\mathcal{A} \models ZF$, then for each formula $\phi$ in the metatheory, there is a corresponding $\phi^{\mathcal{A}} \in A$, where $\phi^{\mathcal{A}}$ is the interpretation of $\ulcorner\phi\urcorner$ in $\mathcal{A}$ (where $\ulcorner\phi\urcorner$ is a constant symbol—usually an element of $\omega^{< \omega}$—meant to represent $\phi$ in the language). If $\mathcal{A}$ is an $\omega$-model, then these are the only formulas of $\mathcal{A}$, but if $\mathcal{A}$ is not an $\omega$-model, then $\mathcal{A}$ has non-standard formulas whose lengths are infinitely large natural numbers.
Basically, I am trying to make sense of the statement in bold. First of all, is Kunen claiming that a non-$\omega$-model may contain non-standard formulas or that it will necessarily contain such formulas? If so, how can we reach that conclusion? It seems to me that even if $A$ has non-standard elements, we still have no way of knowing if $\phi^{\mathcal{A}}$ is or isn't a standard natural number of $A$, regardless of what formula $\phi$ we start with.
What am I missing? Some compactness argument perhaps?
Bonus question: What is "a length of size equal to an infinitely large natural number" in this context? I mean it's one think to talk about non-standard elements of a model, and a completely different one to associate these elements with "size" in the metatheory. How do these non-standard formulas look-like?
The whole "point", one might say, of an $\omega$-model is that its natural numbers only consist of the "standard" natural numbers. Since pretty much by definition, any model of ZFC must contain a set that it would "call" as "$\mathbb{N}$", we can inquire as to the contents of this set and whether or not they are only the "standard" natural numbers or, whether or not that they also include nonstandard numbers. $\omega$-models' "$\mathbb{N}$"s only include standard natural numbers.
So if we are not in an $\omega$-model, then that means that the model's "$\mathbb{N}$" must contain some non-standard numbers. Where that translates to non-standard formulas is that "formulas" are also an object we can formulate within the set theory and thus also can undergo "promotion" via the transfer principle. To see this, note that (as just one of an endless number of possible ways), we can encode a formula as a specific kind of function from a natural number to $\{ 0, 1 \}$ or better, in purely set-theoretic terms, to $\{\emptyset, \{\emptyset\}\}$, where the interpretation of such a function is that it indexes the bits of the formula when its graphic symbols are encoded in some kind of binary-based encoding, say, something like ASCII or UNICODE, and then taking that to be a string of binary bits (0 or 1).
But note now: because we have non-standard numbers, we can now have some formula-like objects which are functions with domain a nonstandard number. Such things are formulas of nonstandard length. Moreover, if it did not contain such formulas, that would mean it would have naturals, that it would recognize as such, and yet that would not be able to map out to $\{0, 1\}$ in ways that ZFC says can happen, and so such a model would fail to be a model of ZFC.
Finally, what does such a formula "look" like, as like a visualization? Well, imagine an infinitely long trail of logical symbols like you'd usually think, e.g.
$$\neg(A \vee [B \wedge C] \wedge \neg(\neg A) \vee \cdots$$
trailing off forever, but then also, somewhere "out there in the hazy mist of the foggy borderland between the definitively finite and definitively infinite", you can dream off to other strigns of symbols...
$$\cdots \vee A \vee A \vee A \vee [\neg A] \wedge B \wedge \cdots$$
where it continues now bidirectionally on both sides and, just as how a nonstandard natural looks, there's a dense linecloud-collection of these doubly-open-ended infinite chains. However, the model, just as it cannot see the nonstandard naturals are nonstandard, also can't see that this strange thing is not a formula. The symbols (or better, the bits in the encoding) will be indexed purely by nonstandard numbers, e.g. $\neg$ above will be located at, say, $(\mbox{some infinitely big 'root'}) - 6000^{\mathrm{googolplex}^\mathrm{moser}}$. And, of course, the formula must be generable by some procedure that could be carried out in ordinary ZFC, and extended to the nonstandard length.