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.
Best Answer
(I overhauled my original answer to better tailor it to your question).
First off, although the general satisfaction relation (for both classes and sets) is not formalizable in ZFC, the satisfaction relation for set models is formalizable. That is, there is an $\mathcal{L}$-formula $\mathrm{Sat}$ such that $\mathrm{Sat}(M,E,\ulcorner \varphi \urcorner,x_1,\dots ,x_n) \leftrightarrow (M,E)\vDash \varphi (x_1, \dots , x_n)$. Just as you could unpack the definition of what it means for a real function to be continuous at a point and express it in ZFC, you can unpack the definition of what it means for a set model to satisfy a formula. That said, this would typically be quite tedious to write down, and so in particular you probably wouldn't want to prove the $L_{\alpha+1}$ exist by applying Separation to the power set of $L_{\alpha}$, although you could.
Rather, the typical approach is to find an alternative yet provably equivalent way of characterizing $\mathrm{Def}(L_{\alpha}) = L_{\alpha+1}$ in terms of something other than definable subsets, and then prove that the thing satisfying this other characterization exists. The approach you'll see in Jech uses the notion of Godel operations, cf. Corollary 13.8 and the preceding lemmas and theorems. Kunen also presents an alternative approach which also has to do with closing off under certain operations, and I feel his approach is better motivated, so I recommend checking out Chapter VI, Section 1 in Kunen's "Set Theory: An Introduction to Independence Proofs."
Let me add parenthetically that yes, you can deal with the $\exists a_1, \dots a_n \in L_{\alpha}$ so that you do get a formula of ZFC. One way is to say