A formula that defines constructible universe 
\begin{multline}
\mathrm{Def}(X) := 
\Bigl\{ \{y \mid y\in X \text{ and } \Phi(y,z_1,\ldots,z_n) \text{ is true in }(X,\in) \} \mid \\
\Phi \text{ is a first order formula and } z_1,\ldots,z_n\in X\Bigr\}.
\end{multline}
(Constructible Universe, Wikipedia)

I saw somewhere at stackexchange that $\Phi$ can be defined, but was not able to find it. So, is there anyway to define what such $\Phi$ would be?
 A: Note that given a (first-order) formula $\Phi$ of set theory (with free variables among $u, v_1 , \ldots , v_n$) and $a_1 , \ldots , a_n \in X$ we can define the set $\{ y \in X : ( X , \in ) \models \Phi [ y, a_1 , \ldots , a_n ] \}$.  The family $\mathrm{Def}(X)$ of all sets "definable" over $X$ is then the collection of all such sets as $\Phi$ varies over all formulas and $a_1 , \ldots , a_n$ vary over all elements of $X$.
There is a formula $\psi (x)$ such that a set $a$ is constructible iff $\psi[a]$ holds (and so $\mathbf{L} = \{ x : \psi[x] \}$).  A common abbreviation for this formula is $( \exists \alpha \in \mathbf{Ord}) ( x \in L_\alpha )$, and I understand if this is not too helpful.  For more detail please consult some of the following references:


*

*Jech, Set Theory: Third Millennium Edition, pp.175-188.

*Drake, Set Theory: An Introduction to Large Cardinals, pp.127-134.

*Kunen, Set Theory: An Introduction to Independence Proofs, pp.165-173.



For some (minimal) details.
You can fix to a Gödel numbering of the formulas of set theory, and say that a set $Y$ is "definable" over $X$ iff for some $n \in \omega$ and parameters $a_1 , \ldots , a_n \in X$ (where $n$ is determined by $n$) $Y$ is the set of all $y \in X$ such that the structure $( X , \in )$ "thinks" that the $n$th formula with the parameters $y, a_1 , \ldots , a_n$ is true. This step is definable, though perhaps tedious to set up.
Another option is to go via so-called Gödel operations, and show that for a transitive $X$, $\operatorname{Def}(X)$ is just the closure of $X \cup \{ X \}$ under these operations (restricted to the power set of $X$). Each of these operations is definable (recursive, even), and from there it is pretty straightforward to define the closure (by recusion up to $\omega$).
