There is a large body of work studying ill-founded models of set theory. The goal is to provide a robust model theory for models of set theory, usually focussing on the countable models. Much of this theory grows out of the study of nonstandard models of arithmetic,
and many tools and theorems from models of arithmetic generalize to the study of models of ZFC.
Let me give a few examples. If M is a model of ZF, one can form the standard system of M by looking at the trace on the standard ω of all the reals of M. It is easy to see that Ssy(M) is a Boolean algebra, closed under Turing reducibility and if T is an infinite binary tree coded in Ssy(M), then there is a path through T coded in Ssy(M). Any set of reals with those three properties is called a Scott set, in honor of Dana Scott, who proved the following amazing characterization:
Theorem.(Scott) If ZFC is consistent, then every countable Scott set arises as the standard system of a model of ZFC.
Scott's theorem is usually stated for models of PA, but the proof for ZFC is identical. It remains a big open question whether Scott's theorem holds for all uncountable Scott sets. The answer is known for Scott sets of size ω1, and so under CH the problem is solved, but it remains open when CH fails.
A key definition is that a model M of ZFC is computably saturated if it realizes every finitely consistent computable type over M. All such models are ω-nonstandard. It turns out that M is computably saturated if and only if it is (isomorphic to) a model that is an element of an ω-nonstandard model of ZFC. Furthermore, these models have interesting closure properties.
Theorem. Any two countable computably saturated models of ZFC with the same standard system and same theory are isomorphic.
Theorem. Every countable computably saturated model M of ZFC is isomorphic to a rank initial segment Vα of itself.
Much of the analysis of models of PA, such as that in the book by Jim Schmerl (UConn) and Roman Kossak (CUNY) extends to models of ZFC. Ali Enayat has also done a lot of interesting work along these lines.
Here is another interesting theorem having to do with nonstandard ZFC models. Let ZFC* be any finite fragment of ZFC. If there is a (very small) large cardinal, then one can use full ZFC in this theorem (e.g. it suffices is there some uncountable θ with Lθ satisfying ZFC). The theorem is interesting in the case that there are nonconstructible reals.
Theorem. Every real x is an element of a model of ZFC*+V=L. Furtheremore, one can find such a model whose ordinals are well-founded at least to α, for any desired countable ordinal α.
Proof. First, the statement of the theorem is definitely true in L, since every real in L is in some large Lθ. Second, the complexity of the statement is Σ11 in x and a real coding α. Thus, by Shoenfield's Absoluteness theorem, it is true in V. QED
Thus, even when x is non-constructible, it can still exist in a model of V=L! This is quite remarkable. (This theorem was shown to me by Adrian Mathias, but I'm not sure to whom it is originally due.)
