TR07-008 Authors: Philipp Weis, Neil Immerman

Publication: 18th January 2007 19:47

Downloads: 1593

Keywords:

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