Two Variable Logic with a Betweenness Predicate
Paritosh Pandya ( Tata Institute of Fundamental Research, Mumbai )
The Unambiguous star-free regular languages (UL), originally defined by Shutzenberger, have many diverse and surprising characterizations.
These include the level Delta_2[<] within the quantifier alternation hierarchy of first-order definable languages, the two variable logic FO2[<], as well as the
unary temporal logic TL[F,P]. To these characterizations, we add several deterministic logics and show that these have efficient reductions between them and to
automata giving NP-complete satisfiability. Next, we consider the extension of FO2[<] with a predicate a(x,y) stating that letter a occurs between positions x and y. This is, in a sense, the simplest property that is not
expressible in FO2[<]. We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of
satisfiability for each of these formulations. We give effective conditions, in terms of the syntactic monoid of a regular language, for a property to be expressible in these logics.
This algebraic analysis allows us to prove, among other things, that our new logics have strictly less expressive power than the full first-order logic FO[<]. Finally, based on our logics,
we consider some new hierarchies within the FO[<] definable languages. (Joint work with Andreas Krebs, Kamal Lodaya and Howard Straubing)