Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words

It is well-known that every first-order property on words is expressibleusing at most three variables. The subclass of properties expressible with onlytwo variables is also quite interesting and well-studied. We prove precisestructure theorems that characterize the exact expressive power of first-orderlogic with two variables on words. Our results apply to both the case with andwithout a successor relation. For both languages, our structure theorems showexactly what is expressible using a given quantifier depth, n, and using mblocks of alternating quantifiers, for any m \leq n. Using thesecharacterizations, we prove, among other results, that there is a stricthierarchy of alternating quantifiers for both languages. The question whetherthere was such a hierarchy had been completely open. As another consequence ofour structural results, we show that satisfiability for first-order logic withtwo variables without successor, which is NEXP-complete in general, becomesNP-complete once we only consider alphabets of a bounded size