We study an extension of FO^2[<], first-order logic interpreted in finite words in which only two variables are used. We adjoin to this language two-variable atomic formulas that say, 'the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables.

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 also give an effective algebraic characterization of the properties expressible in this logic. This enables us to prove, among many other things, that our new logic has strictly less expressive power than full first-order logic FO[<].

This is joint work with Andreas Krebs, Kamal Lodaya, and Paritosh Pandya, and will be presented at LICS2016.