Why do models of ZF which are not $\omega$-models have non-standard formulas whose length is "infinitely large natural numbers"?

For every natural $n$, $\phi_n$ is a sentence, where $\phi_0$ is $\forall x\,(x=x)$ and $\phi_{n+1}$ is $(\phi_n\land\phi_n)$. By recursion, there is a sentence in the theory that codes this claim and so, for any model, for any $n$ that, from the point of view of the model, is a natural number, there is an object of the model that the model interprets as the sentence $\phi_n$. This holds even if $n$ is nonstandard.

Of course, if $n$ is nonstandard, this object $\phi_n$ is not really a formula, but the model cannot see that.


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.