The atoms of the bit-level logic over a vocabulary $L$ are $x \le y$, the addition of ranks $r(x) + r(y) = r(z)$, BIT$(i, x)$, and the atoms of $L$. A kernel is a Boolean combination of atoms, and a sentence is in prenex form: a quantifier prefix over finitely many variables followed by a kernel. It holds on a finite linearly ordered $L$-structure when the prefix holds of the kernel.

A decision problem $P$ over $L$ is bit-definable when some sentence holds, for every nonempty finite $L$-structure $A$ and every linear order on $A$, exactly when $A$ is a yes-instance of $P$. This is the logic FO($\le, +$, BIT), in prenex form.