| |
VOLUME 5, ISSUE 3, PAPER 4
|
Structure Theorem and Strict Alternation Hierarchy for FO2 on Words
|
©Philipp Weis, University of Massachusetts Amherst
©Neil Immerman, University of Massachusetts Amherst
|
Abstract
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 both the case with and without a successor
relation. 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. As another consequence of our
structural results, we show that satisfiability for first-order logic
with two variables without successor, which is NEXP-complete in
general, becomes NP-complete once we only consider alphabets of a
bounded size.
|
Publication date: August 4, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(3:4)2009
Hit Counts: 1407 |
 Creative Commons | |
