Finite-variable logic ($L^k$)

The fragment $L^k$ permits at most $k$ distinct variable names, but allows bound names to be reused. It can contain formulas of arbitrarily large quantifier depth. On a linear order, alternating two variable names can express an increasing chain of any prescribed finite length.

On a finite linearly ordered structure with an equivalence relation, the formula $\forall y(y<x\to \neg E(y,x))$ selects exactly the least element of each equivalence class. Variable-recycling counting therefore expresses any prescribed lower bound on the number of classes. The order and equivalence-relation axioms use three variable names. Finiteness matters: densely interleaved infinite classes need not have least elements.

For a formula $\varphi (x)$ in $L^k$, $k\ge 2$, with only $x$ free, define $C_1^x=\varphi (x)$ and $C_{m+1}^x=\varphi (x)\wedge \exists y(x<y\wedge C_m^y)$. Obtain the superscript-$y$ formula by globally interchanging the two variable names in the superscript-$x$ version. Then $\exists x{C}_m^x$ counts at least $m$ distinct satisfying elements without introducing any further variable names. The recursion works on finite and infinite linear orders.