From the Incompleteness theorems, if ZF is consistent, one knows there are models of ZF satisfying ¬Con(ZF). These models must be non-standard (in the sense of being models whose ordinals are not well-ordered), and so must be the proof of an inconsistency from the axioms of ZF in them.


Now, ¬Con(ZF) is a very special kind of arithmetical statement. My question is, are there other kinds of statements consistent with ZF known to require the existence of non-standard models to hold?


If there are any, how does one recognize them?



Statements that require the existence of non-standard models to hold
Here's another example. By a "computable well ordering" I will mean an index for a well-founded computable (total) linear order on $\omega$. Because ZFC is an effective theory, there must be some computable well ordering $\zeta$ that ZFC does not prove is a well ordering. This is because:


* The set of indices of computable well orderings is strictly $\Pi^1\_1$ but, because ZFC is an effective theory, the set of computable linear orderings that ZFC proves are well founded is $\Sigma^0\_1$. So it cannot be true that a computable linear ordering is well founded if and only if ZFC proves it is well founded.
* ZFC is a true theory, so if ZFC proves that a computable linear order $L$ is well founded then $L$ really is well founded.


Because ZFC does not prove that $\zeta$ is a well ordering, there is some model of ZFC in which $\zeta$ is either not a total linear ordering, or $\zeta$ is not well founded. Either of these can only happen in a non-well-founded model of ZFC, since by definition $\zeta$ really is a well ordering. 


Although this type of example is related to the type from the question, the proof method sketched here does not make use of consistency statements, so I feel this counts as an essentially different example of the same underlying phenomenon. 


