Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR07-008 | 27th November 2006 00:00

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



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].

ISSN 1433-8092 | Imprint