Let $\mathcal{G} = (G,\in)$ be some $\mathfrak{L}$ = {$\in$} structure (for this question a model of ZFC). Let $M$ be some definable class (using Jech's term) and $E$ some class-relation on M. Let $\mathcal{M} = (M, E)$. $\varphi$ be a formula and let $\varphi^{\mathcal{M}}$ be the relativization of $\varphi$. $\mathcal{M} \models \varphi$ is defined to be $\mathcal{G} \models \varphi^{\mathcal{M}}$.

In the Constructible Herierachy, for each ordinal $\alpha$, $L_{\alpha + 1}$ is the "collection" of all subset of $L_\alpha$ that is definable over $L_\alpha$.

Is each $L_\alpha$ a set - an element in the original structure $\mathcal{G}$? To prove this I think one should use the separation schema. However, how does one prove that there is a formula that asserts $x$ is a definable subset (with respect to the structure $L_\alpha$) over $L_\alpha$, where the model relation for $L_\alpha$ is defined by the relativization with respect to $\mathcal{G}$.

Assuming $L_\alpha$ is a set. I think I would need a formula like

$L_{\alpha + 1}$ = {$x \in \mathscr{P}(L_\alpha)$ : $(\exists (\ulcorner \varphi\urcorner) \in Form)(\exists a_1, ..., a_n \in L_\alpha)(\forall y \in x)(\varphi^{L_\alpha}(y, a_1, ..., a_n))$}

(where I think $n$,$a_1, ..., a_n$ can be encoded or that part can be written in some way using parameter so that portion is an actual {$\in$}-formula.)

However is there a formula $\psi$ such that for $\mathcal{G} \models \psi(\ulcorner\varphi\urcorner(\bar{a}))$ if and only if $\mathcal{G} \models \varphi^{L_\alpha}(\bar{a})$.

I am uncertain about whether such a formula exists since in $\textit{Set Theory}$ by Jech (pg 162; newest edition), he writes

"When using relativization $\varphi^{M,E}(x1,...,xn)$ it is implicitly assumed that the variables x1, ..., xn range over M. We shall often write (M,E) $\models$ φ(x1,...,xn) instead of (12.14) and say that the model (M,E) satisfies φ. We point out however that while this is a legitimate statement in every particular case of φ, the general satisfaction relation is formally undefinable in ZF."

and also the next paragraph

"If M is a set and E is a binary relationon M and if $a_1$,...,$a_n$ are elements of M, then

(12.16) φ^{M,E}(a1,...,an) ↔ (M,E) $\models$ $\ulcorner\varphi\urcorner$[a1,...,an]

as can easily be verified. Thus in the case when M is a set and φ a particular (metamathematical) formula, we shall not make a distinction between the two meanings of the symbol $\models$. We note however that the left-hand side of (12.16) (relativization) is not defined for φ ∈ Form, and the right-hand side (satisfaction) is not defined if M is a proper class."

I hope the question was coherent. Thanks for any clarifications about whether $L_\alpha$ is a set or not, or the excerpt from Jech.