[proofplan] We define a canonical order by following the construction of $L$ stage by stage. A set first appearing at stage $L_{\alpha+1}$ is represented by the least formula, and then the least tuple of parameters from $L_\alpha$, which defines it over $L_\alpha$. The order compares first by stage of first appearance, then by formula code, and finally by the already constructed order of the parameter tuple. Because definitions at stage $\alpha+1$ use only parameters from $L_\alpha$, the recursion is well-founded and gives a unique global well-order. [/proofplan]

[step:Fix canonical codes for formulas and finite tuples] Fix once and for all a primitive recursive coding of first-order formulas in the language $\{\in\}$ by natural numbers. For a code $e \in \omega$, write $\theta_e(v_0,\dots,v_m)$ for the formula coded by $e$, when $e$ codes such a formula; codes that do not code formulas are ignored. Also fix the usual set-theoretic coding of finite tuples by sets. If $a$ is a coded finite tuple, write $\ell(a) \in \omega$ for its length and $a_i$ for its $i$-th coordinate, for $i < \ell(a)$. For a binary relation $R$ on a set $A$, define the induced lexicographic order $R^{<\omega}_{\mathrm{lex}}$ on finite tuples from $A$ as follows: $a \, R^{<\omega}_{\mathrm{lex}} \, b$ iff either $\ell(a) < \ell(b)$, or $\ell(a)=\ell(b)$ and, letting $i<\ell(a)$ be the least coordinate with $a_i \ne b_i$, one has $a_i \, R \, b_i$. The coding relations just described are first-order definable in the language of set theory, since finite sequences, natural numbers, and primitive recursive relations on $\omega$ are first-order definable over set theory. [/step]

[step:Define the local construction rule at one successor stage] Let $\alpha$ be an ordinal, and suppose that $R_\alpha$ is already a well-order of $L_\alpha$. For each $x \in L_{\alpha+1}\setminus L_\alpha$, define its canonical definition datum over $L_\alpha$ to be the least pair $(e,a)$ in the lexicographic order on $\omega \times L_\alpha^{<\omega}$ such that $e$ codes a formula $\theta_e(v_0,\dots,v_m)$, the tuple $a$ has length $m$, and \begin{align*} x &= \{z \in L_\alpha : L_\alpha \models \theta_e(z,a_0,\dots,a_{m-1})\}. \end{align*} Here $\omega$ is ordered by the usual order, and $L_\alpha^{<\omega}$ is ordered by $R_{\alpha,\mathrm{lex}}^{<\omega}$. This least datum exists because, by definition of $L_{\alpha+1}$, every element of $L_{\alpha+1}\setminus L_\alpha$ is definable over $L_\alpha$ with finitely many parameters from $L_\alpha$, and $\omega \times L_\alpha^{<\omega}$ is well-ordered by the stated lexicographic order. Extend $R_\alpha$ to a relation $R_{\alpha+1}$ on $L_{\alpha+1}$ by declaring: \begin{align*} x \, R_{\alpha+1} \, y \end{align*} iff one of the following mutually exclusive alternatives holds: \begin{align*} x,y &\in L_\alpha \text{ and } x \, R_\alpha \, y; \end{align*} \begin{align*} x &\in L_\alpha \text{ and } y \in L_{\alpha+1}\setminus L_\alpha; \end{align*} \begin{align*} x,y &\in L_{\alpha+1}\setminus L_\alpha \end{align*} and the canonical definition datum of $x$ over $L_\alpha$ is lexicographically smaller than the canonical definition datum of $y$ over $L_\alpha$. Thus every old element precedes every new element, and new elements are ordered by their least defining formula and least defining parameter tuple. [/step]

[step:Pass through limit stages by union] Let $\lambda$ be a limit ordinal, and suppose that $R_\beta$ has been constructed on $L_\beta$ for every $\beta<\lambda$, with the coherence property \begin{align*} R_\gamma &= R_\beta \cap (L_\gamma \times L_\gamma) \end{align*} whenever $\gamma<\beta<\lambda$. Define \begin{align*} R_\lambda &= \bigcup_{\beta<\lambda} R_\beta. \end{align*} This is a relation on $L_\lambda = \bigcup_{\beta<\lambda} L_\beta$. The coherence condition implies that $R_\lambda$ is well-defined, linear, and restricts to $R_\beta$ on each $L_\beta$. Every nonempty subset $A \subseteq L_\lambda$ has an $R_\lambda$-least element: choose the least ordinal $\beta<\lambda$ such that $A\cap L_{\beta+1}\ne\varnothing$. Then $A\cap L_{\beta+1}$ has an $R_{\beta+1}$-least element, and every element of $A$ appearing at a later stage is placed after all elements of $L_{\beta+1}$. Hence that element is also least in $A$ under $R_\lambda$. [/step]

[step:Verify the recursion gives a coherent well-order at every level] By the [Transfinite Recursion Theorem](/page/Transfinite%20Recursion) applied to the class rule just described, the preceding successor and limit rules determine a unique relation $R_\alpha$ on each $L_\alpha$. We prove by induction on $\alpha$ that $R_\alpha$ is a well-order of $L_\alpha$ and that the family is coherent. The case $\alpha=0$ is immediate, since $L_0=\varnothing$. The successor step follows from the construction: $R_{\alpha+1}$ is obtained by putting the well-ordered set $L_\alpha$ first, then well-ordering the new part $L_{\alpha+1}\setminus L_\alpha$ by the well-order of canonical definition data. A [lexicographic product of well-orders](/theorems/4805) is a well-order, so the new part is well-ordered. Placing one well-order after another again gives a well-order. The limit step was verified in the preceding step. Coherence is built into both clauses: at successors the old relation is preserved exactly, and at limits the relation is the union of earlier coherent relations. Therefore each $R_\alpha$ is a well-order of $L_\alpha$, and $R_\gamma$ is the restriction of $R_\beta$ whenever $\gamma<\beta$. [/step]

[step:Define the global relation and prove it well-orders $L$]Define a class relation $<_L$ on $L$ by \begin{align*} x &<_L y \end{align*} iff there exists an ordinal $\alpha$ such that $x,y\in L_\alpha$ and $x \, R_\alpha \, y$. This definition is independent of the chosen $\alpha$. Indeed, if $x,y\in L_\alpha\cap L_\beta$, then for any ordinal $\delta$ with $\alpha,\beta\leq\delta$, coherence gives \begin{align*} R_\delta\cap(L_\alpha\times L_\alpha)&=R_\alpha \end{align*} and \begin{align*} R_\delta\cap(L_\beta\times L_\beta)&=R_\beta. \end{align*} Thus the truth value of $x \, R_\alpha \, y$ agrees with that of $x \, R_\beta \, y$. The field of $<_L$ is exactly $L$, since every constructible set belongs to some level $L_\alpha$. The relation is linear because any two elements of $L$ lie together in some $L_\alpha$, where $R_\alpha$ is linear. Finally, let $A$ be a nonempty subclass of $L$. Choose $x\in A$, and let $\alpha$ be an ordinal with $x\in L_\alpha$. The class \begin{align*} B&=\{\beta\in\operatorname{Ord}: A\cap L_{\beta+1}\ne\varnothing\} \end{align*} is nonempty, since $\alpha\in B$ or some earlier ordinal is in $B$. Although $B$ may be a proper class, it is a nonempty subclass of $\operatorname{Ord}$, so it has a least element $\beta$ by the class well-ordering of the ordinals. Since $R_{\beta+1}$ well-orders $L_{\beta+1}$, the set $A\cap L_{\beta+1}$ has an $R_{\beta+1}$-least element $a$. By minimality of $\beta$, no element of $A$ appears before stage $\beta+1$, and by construction all elements appearing at later stages are placed after elements of $L_{\beta+1}$. Hence $a$ is the $<_L$-least element of $A$. Therefore $<_L$ is a well-order of $L$.[/step]

[guided]We must be slightly careful because $A$ is allowed to be a proper subclass of $L$, not merely a set. Since $A$ is nonempty, choose $x\in A$. By the definition of $L$, there is an ordinal $\alpha$ with $x\in L_\alpha$, and therefore $A\cap L_{\alpha+1}\ne\varnothing$. Hence the class \begin{align*} B&=\{\beta\in\operatorname{Ord}: A\cap L_{\beta+1}\ne\varnothing\} \end{align*} is nonempty. The point of passing to $B$ is to locate the first constructible level at which $A$ appears. The class $B$ may be proper, but this causes no problem: $B$ is a nonempty subclass of $\operatorname{Ord}$, and the ordinals are class well-ordered by $\in$. Thus $B$ has a least element $\beta$. Now $A\cap L_{\beta+1}$ is a set, because $L_{\beta+1}$ is a set. Since $R_{\beta+1}$ is a well-order of $L_{\beta+1}$, the set $A\cap L_{\beta+1}$ has an $R_{\beta+1}$-least element $a$. Minimality of $\beta$ says that no element of $A$ lies in any earlier level $L_{\gamma+1}$ with $\gamma<\beta$. The construction of the relations places all later-stage elements after all elements already present at stage $L_{\beta+1}$. Therefore every element of $A$ distinct from $a$ is either in $L_{\beta+1}$ and follows $a$ by $R_{\beta+1}$, or appears at a later stage and is placed after $a$. Hence $a$ is the $<_L$-least element of $A$, so $<_L$ well-orders $L$.[/guided]

[step:Show the global well-order is first-order definable without parameters]It remains to check definability. Let $\operatorname{Ord}$ denote the class of ordinals. For any set $M$, let $\operatorname{Def}(M)$ denote the set of all subsets of $M$ that are first-order definable over the structure $(M,\in)$ with finitely many parameters from $M$. By the standard uniform definition of the [constructible hierarchy](/page/Constructible%20Universe), the relation “$z=L_\alpha$” is first-order definable uniformly in $\alpha$ from the recursive clauses \begin{align*} L_0&=\varnothing,\qquad L_{\alpha+1}=\operatorname{Def}(L_\alpha),\qquad L_\lambda=\bigcup_{\beta<\lambda}L_\beta \end{align*} for limit ordinals $\lambda$. The [satisfaction relation](/page/Satisfaction%20Relation) for set-sized structures is first-order definable in the ambient universe by recursion on formula codes. More explicitly, for a set $M$, a formula code $e$, and a finite tuple $b$ from $M$, the assertion \begin{align*} (M,\in)\models \theta_e[b] \end{align*} is defined by induction on the syntactic complexity of $e$: atomic formulas are evaluated directly from membership and equality in $M$, Boolean connectives are handled by the corresponding Boolean operations, and quantifiers are bounded to elements of the set $M$. Since this recursion is over the set of subformulas of the coded formula, it is first-order expressible in the ambient universe. Consequently, the assertion that a pair $(e,a)$ is the least definition datum for $x$ over $L_\alpha$ is first-order expressible from $\alpha$, $x$, and the already constructed relation on $L_\alpha$: it says that $e$ is a formula code, $a\in L_\alpha^{<\omega}$ has the right length, $x$ is exactly the subset of $L_\alpha$ satisfying that formula with parameters $a$, and no lexicographically smaller pair has the same property. Now say that a set $S$ is a construction history up to $\alpha$ if $S$ is a function with domain $\alpha+1$, each $S(\beta)$ is a binary relation on $L_\beta$, and $S$ satisfies the successor and limit clauses described above at every stage $\beta\leq\alpha$. This condition is first-order expressible because all quantifiers over stages are bounded by the set $\alpha+1$, all relations $S(\beta)$ are set-sized, and the successor clause can be written using the definable satisfaction predicate for $L_\beta$, formula codes, finite tuple coding, and lexicographic comparison. The limit clause says, in first-order form, that for every limit $\lambda\leq\alpha$ and all $x,y\in L_\lambda$, one has $x\,S(\lambda)\,y$ iff there is some $\beta<\lambda$ with $x,y\in L_\beta$ and $x\,S(\beta)\,y$. By uniqueness in the [Transfinite Recursion Theorem](/page/Transfinite%20Recursion), any two construction histories up to the same stage agree. Therefore the formula \begin{align*} \varphi(x,y) \quad\Longleftrightarrow\quad \exists \alpha\,\exists S\,\bigl(S \text{ is a construction history up to } \alpha,\ x,y\in L_\alpha,\text{ and } x\,S(\alpha)\,y\bigr) \end{align*} defines exactly the relation $<_L$. This formula has no parameters. Hence $<_L$ is a parameter-free first-order definable class well-order of $L$, as required.[/step]

[guided]The definability issue is that the recursion defining $R_\alpha$ ranges through all ordinals, so we cannot use a single set as the completed recursive object. The standard way to express such class recursions first-order is to quantify over set-sized initial histories. First, the levels of $L$ are uniformly definable: by the standard definition of the [constructible hierarchy](/page/Constructible%20Universe), there is one first-order formula saying that a set $z$ is $L_\alpha$, using the clauses \begin{align*} L_0&=\varnothing,\qquad L_{\alpha+1}=\operatorname{Def}(L_\alpha),\qquad L_\lambda=\bigcup_{\beta<\lambda}L_\beta \end{align*} for limit ordinals $\lambda$. The successor clause is first-order because definability over a set-sized structure is handled by the [satisfaction relation](/page/Satisfaction%20Relation) for that structure. For set-sized structures, satisfaction is itself definable in the ambient universe by recursion on formula codes. If $M$ is a set, $e$ is a formula code, and $b$ is a finite tuple from $M$, the statement \begin{align*} (M,\in)\models \theta_e[b] \end{align*} is evaluated by a finite syntactic recursion: atomic formulas check equality and membership inside $M$, Boolean connectives reduce to their immediate subformulas, and quantifiers range only over elements of the set $M$. Thus the relation “$(e,a)$ defines $x$ over $L_\alpha$” is first-order expressible. The word “least” is also first-order expressible because the order on formula codes is the usual order on $\omega$, the order on parameter tuples is the already supplied relation $S(\alpha)$ extended lexicographically, and quantification over smaller candidate pairs is set-bounded. Now define a construction history up to $\alpha$ to be a set $S$ with domain $\alpha+1$ such that each $S(\beta)$ is a binary relation on $L_\beta$, and such that the successor and limit clauses are satisfied for every $\beta\leq\alpha$. This is first-order expressible: all stages being checked lie in the set $\alpha+1$, the values $S(\beta)$ are sets, the successor rule uses the just-described formula for least definition data, and the limit rule says that $S(\lambda)$ is the union of the earlier $S(\beta)$ for $\beta<\lambda$. By uniqueness in the [Transfinite Recursion Theorem](/page/Transfinite%20Recursion), two construction histories up to the same stage must agree at every earlier stage. Hence the formula \begin{align*} \varphi(x,y) \quad\Longleftrightarrow\quad \exists \alpha\,\exists S\,\bigl(S \text{ is a construction history up to } \alpha,\ x,y\in L_\alpha,\text{ and } x\,S(\alpha)\,y\bigr) \end{align*} is independent of the chosen history and stage, and it holds exactly when $x<_L y$. No parameter appears in this formula, so $<_L$ is a parameter-free first-order definable class well-order of $L$.[/guided]