Many interesting properties of words can be described in a first-order language with variables (x, y, ...) for positions and two basic properties: x < y (meaning that x is to the left of y) and Qax (meaning that letter a is at position x). For example, in this language, there are at least two occurrences of a to the left of the first occurrence of b. In this language, too, there are two different ways to describe the complexity of statements: by the number of variables and by their quantifier complexity, that is, by the number of alternating blocks of universal and existential quantifiers. Hierarchy by the number of variables is not very complex; it has been proven that any formula can be reformulated by using at most three variables.
This paper analyzes the two-variable fragment. Within this fragment, we can classify formulas by their quantifier complexity. The authors show that for two-variable formulas, the quantifier complexity--which at first glance may seem to be a purely syntactic property--can actually be reformulated in purely algebraic, syntax-free terms. This algebraic reformulation enables the authors to come up with an algorithm that, given a two-variable formula, computes its quantifier complexity.
