Iterating definability An odd -- probably basic -- question about model theory:
For $\mathcal{M}$ a structure in a (first-order) signature $\Sigma$, let $\mathcal{M}'$ be the structure in signature $\Sigma\sqcup\lbrace U\rbrace$ -- with $U$ a unary relation -- whose reduct to $\Sigma$ is $\mathcal{M}$, and interprets $U$ as $$ U^{\mathcal{M}'}=\lbrace a: a\text{ is definable in $\mathcal{M}$}.\rbrace$$
Up to the choice of unary relation symbol $U$, this is well defined; moreover, we can iterate this through the ordinals: $$ \mathcal{M}^{(0)}=\mathcal{M}, \quad \mathcal{M}^{(\alpha+1)}=(\mathcal{M}^{(\alpha)})', \quad \mathcal{M}^{(\lambda)}=\bigcup_{\beta<\lambda}\mathcal{M}^{(\beta)} \,\,(\lambda \text{ limit}).$$ (The union notation is technically inappropriate, but its meaning is clear.) Now, for any $\mathcal{M}$, let $$ D(\mathcal{M}, \alpha)=\lbrace a\in\mathcal{M}: a\text{ is definable in $\mathcal{M}^{(\alpha)}$}\rbrace$$ be the set of elements of $\mathcal{M}$ definable after stage $\alpha$. Let $D(\mathcal{M}, \infty)=\bigcup_{\alpha\in ON} D(\mathcal{M}, \alpha)$ be the set of all eventually definable elements, and for $a\in D(\mathcal{M}, \infty)$ let the age of $a$, $age_\mathcal{M}(a)$, be the least $\beta$ such that $a\in D(\mathcal{M}, \beta)$. Clearly for each $\mathcal{M}$ there is a least upper bound, $m_\mathcal{M}$, on the ages of elements of $D(\mathcal{M}, \infty)$.
Some very easy observations:


*

*If $\mathcal{M}=(M, <)$ is a well-ordering, then $D(\mathcal{M}, \infty)=M$, since the $\alpha$th element of $\mathcal{M}$ is definable by stage $\alpha$ at the latest.

*Even if $\mathcal{M}$ is strongly minimal, $\mathcal{M}'$ need not be: consider $\mathcal{M}=\mathbb{N}+\mathbb{Z}$ as a linear order. Presumably other niceness properties such as stability are also not preserved, but I don't have examples yet.
My question is, what is known about the set $D(\mathcal{M}, \infty)$, the age function $age_\mathcal{M}$, or the invariant $m_\mathcal{M}$? I've been playing around with this idea for a bit, but my model theory is not very strong; I'm sure this has been treated before, but I haven't been able to find a reference. 
(In case anyone is interested, I initially thought that there would be connections with notions of rank, as long as $\mathcal{M}$ is sufficiently nice; in fact, I came up with this question after using some dubious analogies to try to explain forking and rank to a friend. As far as I can tell, this initial hope is in fact bogus, but that's where this came from.)

There are two other questions about this that I'm especially interested in. First, what if we augment first-order logic by adding a logical unary relation $D$ whose interpretation is stipulated to always be $D(\mathcal{M}, \infty)$ -- the resulting model theory seems wild (compactness and Lowenheim-Skolem fail extremely badly), but this logic "comes from" first-order logic in a natural way; is there anything nice we can say about it? Second, this time closer to computability theory: what if we replace "definable" with $\Sigma_1$-definable? Does $m_\mathcal{M}$ now have a recursion-theoretic interpretation? I consider these as just curiosities, compared to the main question (which, though more vague, I hope is still appropriate), but if anyone has anything to say on either count I'd be extremely interested.
 A: Your construction has a family resemblence with the iterative
theories of truth, due originally to Tarski and discussed at
length in the philosophical logic literature, by Kripke, Putnam
and many others.
Rather than adding a predicate for definability, the idea in these
theories, acknowledging Tarski's nondefinability theorem that one
cannot have a full classical theory of truth in the language with
that truth predicate, is that nevertheless one may build an
increasingly robust theory of truth, in a transfinite progression,
by successively adding truth predicates over the expanded
structure that has been defined so far. One starts with an initial
structure $\mathcal{M}$, and then add a predicate for
true-in-$\mathcal{M}$, and then a predicate for truth in that
structure, and so on transfinitely.
To be precise, if $\mathcal{M}^{(0)}$ is a structure that interprets
arithmetic, so one can refer to formulas via Gödel coding,
then we define the truth predicate $T^{(0)}$ for this model, where
 $T^{(0)}(\varphi,\vec a)$ holds if and only if
$\mathcal{M}^{(0)}\models\varphi[\vec a]$, where $\varphi$ is any
formula in the language of $\mathcal{M}^{(0)}$. Adjoining this new
predicate, we form the next structure $\mathcal{M}^{(1)}=\langle
M,\ldots,T^{(0)}\rangle$, and then continue the construction just
as you did. At stage $\alpha$, we have the $\alpha^{\rm th}$
structure $\mathcal{M}^{(\alpha)}$, and then form the truth
predicate $T^{(\alpha)}$ for satisfaction in this structure. In
particular, the predicate $T^{(\alpha)}$ concerns formulas
$\varphi$ in the language in which earlier truth predicates
$T^{(\beta)}$ appear as formal predicates.
The closely related revision theories of truth (see the book The revision theory of truth by
Gupta and Belnap) have a different tack, following ideas of
Kripke, trying to unify the theory of truth into one increasingly
stable (but partial) truth predicate. In this theory, one can
refer to things like "eventually true" or stabilized truth, and so
on. There would seem to be an analogue of this approach also in
your context.
