= Solution
Use only the variable names $x,y$. Define mutually renamed formulas by
$$
D_1^x(x)=(x=x),\qquad
D_{m+1}^x(x)=\exists y\,[x<y\land D_m^y(y)],
$$
where $D_m^y$ is obtained from $D_m^x$ by globally interchanging $x$ and $y$, including their bound occurrences. By induction, $D_m^x(a)$ means that an increasing chain of $m$ elements starts at $a$. Hence
$$
\boxed{\lambda_n=\exists x\,D_n^x(x)\in L^2}
$$
holds exactly when the <linear order> has at least $n$ elements. Inner quantifiers may bind the name $x$ again, but their scope is only the nested subformula; the comparison $x<y$ still refers to the preceding point. This <finite-variable logic> construction works on finite and infinite <linear orders>.
Back to article page
