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?
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$:
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.