Two-variable Logic with a Between Relation
Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, Howard Straubing · 2016
We study an extension of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. 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.