= Variable-recycling count on a linear order
For a formula $\phi(x)$ in $L^k$, $k\ge2$, with only $x$ free, define $C_1^x=\phi(x)$ and $C_{m+1}^x=\phi(x)\land\exists y(x<y\land 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.
Back to article page
