Suppose $\kappa$ is a measurable cardinal and $U$ is a normal measure on $\kappa$. $M_1$ is the ultrapower of the universe $V$ constructed form $U$,$j_{01}$ is the induced elementary embedding, $M_2$ is the ultrapower of $M_1$ constructed from $j_{01}(U)$...We can iterate this process. We know $M_0,M_1,M_2,...$ and $j_{01},j_{02},j_{12},..$ are all classes of the universe, i.e. they are all definable. Also, they form a direct system, so we can define the direct limit $(M_{\omega},E_{\omega})$. $M_{\omega}$ and $E_{\omega}$ are both subset of the universe $V$, but my question is why they are definable subset of the universe?
1 Answer
There are in fact many different definable ways to represent the direct limit. One particularly concrete representation of the direct limit is to use maximal threads, that is, maximal sequences $\langle x_i \mid j\leq i\lt\omega\rangle$, where $x_{i+1}=j_{i,i+1}(x_i)$, where $j_{i,i+1}:M_i\to M_{i+1}$ is the ultrapower of $M_i$ by $U_i=j_{0,i}(U)$, a normal measure on $\kappa_i$, where $j_{i,j}:M_i\to M_j$ is the corresponding composition of these embeddings. One then defines the $\in$ relation in $M_\omega$ by consulting the common coordinates, and this is welldefined. Alternatively, one may take the disjoint union of the $M_i$, and declare that any two such points are equivalent when they map to the same point in some later $M_i$. And there are many other representations of the direct limit, and these may all be defined by defining the constituent elements of the system used to define the direct limit, often taking the quotient by an equivalence relation, which is definable from the system and the measure.
The point is that any of these concrete representations of the direct limit can be defined from the measure $U$. With $U$ as a parameter, one may define any of the classes $M_i$ and also the embeddings $j_{i,j}:M_i\to M_j$, and furthermore, we may do so uniformly in $i$ and $j$. Thus, the point is that not only are the various $M_i$ and embeddings $j_{i,j}$ definable individually, but uniformly in the parameters $i$, $j$, and this is what it takes to define the direct limit using any of the usual representations of the direct limit. In short, we use the fact that we can define the entire system of embeddings $j_{i,j}:M_i\to M_j$ uniformly in order to know that we can build a representation of the direct limit of that system.
But what is more, since the direct limit is wellfounded, there is in fact a canonical way to represent the direct limit: the Mostowski collapse of your favorite representation. This provides $\langle M_\omega,{\in}\rangle$ as a transitive model of set theory, using the actual $\in$ relation. And the result will be a proper transitive class $M_\omega\subset V$, definable from $U$ as a parameter, with definable class embeddings $j_{i,\omega}:M_i\to M_\omega$.

$\begingroup$ Thanks for your kind answer. If the entire system $<M_ii<\omega>$ and $<j_{i,j}i<j<\omega>$ are definable, then pick any representation of the direct limit, it is definable. But I still not well understand why the entire system is definable? $<M_ii<\omega>$ is a sequence of classes, in general, an infinite sequence of classes need not be definable. But I have a feeling this sequence $<M_ii<\omega>$ is similar to a sequence defined by induction, so whether "a sequence of classes defined by induction" is indeed definable? $\endgroup$– Song LiCommented Aug 3, 2012 at 4:16

1$\begingroup$ Yes, the classes and the system are definable by induction. One defines the relations $x\in M_i$ and $j_{i,k}(x)=y$, meaning that one defines the classes $\\{(x,i)\mid x\in M_i\\}$ and $\\{(i,k,x,y)\mid j_{i,k}(x)=y\\}$, so one needn't encounter problems from forming "sequences of classes". The point is that the definition of whether $x\in M_{i+1}$ depends only very locally on $M_i$; in general, one cannot legitimately define classes by induction: for example, there are serious isses with defining the classes $\text{HOD}^n$. See jdh.hamkins.org/generalizationsofkuneninconsistency $\endgroup$ Commented Aug 3, 2012 at 11:30

$\begingroup$ My previous comment seems to be missing the set braces { } around those two classes. $\endgroup$ Commented Aug 3, 2012 at 12:57

$\begingroup$ I just read the remark on iterated HOD classes in your paper. For the iterated ultrapower case, the graph is definable, but this does not happen in iterated HOD case. Thanks for your helpful answer again. $\endgroup$– Song LiCommented Aug 3, 2012 at 13:05

1$\begingroup$ Hi Joel. I didn't know of the Zadrozny paper, only of an earlier paper by Jech, "Forcing with trees and ordinal deﬁnability", Ann. Math. Logic 7, (1974/75), 387–409. Nice reference. $\endgroup$ Commented Aug 3, 2012 at 16:38