Is $V=L$ a single first-order sentence? Is $V=L$, the axiom of constructibility, a single first-order sentence?
Since $V=L$ really stands for $(\forall x)(\exists \alpha)[\alpha \in \mathrm{On} \wedge x \in L_\alpha]$, so my question might as well be "is $x \in L_\alpha$ a single first-order formula?".
I was confused about this since prima facie the definition of $L$ involves arbitrary first-order formulas and a satisfaction predicate for them.  Of course one can appeal to the recursive definition by using Goedel's operations, but I am still unsure whether all the details work out.
 A: Yes, it is a first-order statement.
Recall that the definition of $L_\alpha$ is an inductive definition. $L_0=\varnothing$, $L_{\alpha+1}=\operatorname{Def}(L_\alpha,\in)$ and for limit ordinals $L_\alpha=\bigcup_{\gamma<\alpha}L_\gamma$.
It might seem that the successor definition is not "internal", but in fact it is. It uses the internal definition of truth,1 so it is again another definition using complicated inductions.
Finally, remember that the replacement schema allows us to take an inductive definition, over all the ordinals, and replace it with a single first-order statement. Much like how induction is internalized in Peano arithmetic.



*

*Remember that the way we define first-order logic related concepts is really by induction. We have notions of strings, and when a string is a term, etc.; and a notion of a structure, and an assignment function, and then a truth value (after assigning the free variables values, of course). 
But since this is really just a long long long list of inductions, and the core concept of "strings" is already easy to formalize internally (simply finite sequences from a fixed alphabet), we can write a definition for what the universe "thinks" is the set of strings, and formulas and so on.
So all this collapses to a very complicated, very long, very uninteresting formula that we know that we can write.
A: There are 15 very simple functions that generate $L$. See Schindler Set Theory textbook for more details. 
Examples of these function are the pairing function, set difference function, cartesian product, etc. 
Define a function $S$ which takes a set $x$ to it closure under these 15 functions. 
Define 
$S_0 = \emptyset$
$S_{\alpha + 1} = S (S_\alpha)$
For limits $\lambda$, let
$S_\lambda = \bigcup_{\alpha < \lambda} S_\alpha$
Then it can be shown that $L = \bigcup_{\alpha \in \text{ON}} S_\alpha$.
Since $S$ is the closure of a finite list of function, it may be more clear that $\alpha \rightarrow S_\alpha$ is definable using the usual transfinite recursion. 
This is similar to Godel and Jensen approach to constructibility. 
