# 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?

-
Have you tried to open a book? Wikipedia is a good place to get an overview about things, but not to study. This site is not a supplement for trying to figure things on your own after working through the first part of Jech's Set Theory, for example. – Asaf Karagila Sep 18 '12 at 9:24

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: