Two Variable Logic with a Betweenness Predicate

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)