In a finite linear order, the rank of an element is the number of elements strictly below it, so that the elements are numbered $0, \dots, n - 1$. The number of bit positions of the order is $\lceil \log_2 n \rceil$, enough to write every rank in binary. The predicate BIT$(i, x)$ holds when the bit of weight $2^{r}$ is set in the binary expansion of the rank of $x$, where $r$ is the rank of $i$: an element names a position by its rank.

A quantifier prefix over $m$ variables is given by a polarity per variable, existential or universal; it holds of a property of $m$-tuples when the variables, quantified in order with the first outermost, make the property true.