eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-04-23
1
22
10.4230/DagSemProc.06451.6
article
Structure Theorem and Strict Alternation Hierarchy for FOÃ‚Â² on Words
Weis, Philipp
Immerman, Neil
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 $mleq 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, and Wilke 1997].
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol06451/DagSemProc.06451.6/DagSemProc.06451.6.pdf
Descriptive complexity
finite model theory
alternation hierarchy
Ehrenfeucht-Fraisse games