How do you formally state the axiom of constructibility? The Axiom of Constructibility states every set is constructible.
My question is, how would one formally state this, since it seems to involve quite a bit of metamathematics? In particular, if one wanted to add this as an axiom to, say, ZFC, how would you state it?
 A: Recall that $x\in L$ if and only if there is some $\alpha$ such that $x\in L_\alpha$. And that is exactly the content of the axiom $V=L$:

For every $x$, there exists an ordinal $\alpha$ such that $x\in L_\alpha$.

But wait, what is $L_\alpha$ anyway? Ah, well, luckily, it is the unique set $X$ such that there exists a function $f$ with domain $\alpha+1$, that $f(0)=\varnothing$, $f(\gamma+1)$ is the definable subsets of $f(\gamma)$, if $\gamma$ is a limit ordinal then $f(\gamma)=\bigcup\{f(\beta)\mid\beta<\gamma\}$, and $X=f(\alpha)$.
Note that "definable subsets" is an internal notion, which requires a very long definition, which essentially establishes a large chunk of first-order logic as internalized by $\sf ZF$. But it is certainly the internal version of "definable" we are talking about here, and this is important.
So what would a complete write up of this axiom include? A rudimentary definition of first-order logic and what it means for a set to be definable; then the definition of the function $\alpha\mapsto L_\alpha$; then the statement that for every $x$, there is some $\alpha$ such that $x\in L_\alpha$. We leave writing something like this in full as an exercise to the masochistic reader.
