It is well-known that every first-order property on words is expressible
using at most three variables. The subclass of properties expressible with
only two variables is also quite interesting and well-studied. We prove
precise structure theorems that characterize the exact expressive power of
first-order logic with two variables on words. Our results apply to
FO^2[<] and FO^2[<,Suc], the latter of which includes the binary
successor relation in addition to the linear ordering on string positions.

For both languages, our structure theorems show exactly what is
expressible using a given quantifier depth, n, and using m blocks
of alternating quantifiers, for any m <= n. Using these
characterizations, we prove, among other results, that there is a
strict hierarchy of alternating quantifiers for both languages. The
question whether there was such a hierarchy had been completely open
since it was asked in [Etessami, Vardi, Wilke 1997].